Polar SAT and related graphs

We introduce polar SAT and show that a general SAT can be reduced to it in polynomial time. A set of clauses C is called polar   if there exists a partition Cp∪Cn=CCp∪Cn=C, called a polar partition  , such that each clause in CpCp involves only positive   (i.e., non-complemented) variables, while each clause in CnCn contains only negative   (i.e., complemented) variables. A polar set of clauses C=(Cp,Cn)C=(Cp,Cn) is called (p,n)(p,n)-polar  , where p⩾1p⩾1 and n⩾1n⩾1, if each clause in CpCp (respectively, in CnCn) contains exactly p (respectively, exactly n  ) literals. We classify all (p,n)(p,n)-polar SAT Problems according to their complexity. Specifically, a (p,n)(p,n)-Polar SAT problem is NP-complete if either p>n⩾2p>n⩾2 or n>p⩾2n>p⩾2. Otherwise it can be solved in polynomial time. We introduce two new hereditary classes of graphs, namely polar satgraphs and polar (3,2)(3,2)-satgraphs, and we characterize them in terms of forbidden induced subgraphs. Both characterization involve an infinite number of minimal forbidden induced subgraphs. As are result, we obtain two narrow hereditary subclasses of weakly chordal graphs where Independent Domination is an NP-complete problem.