Polynomial-time satisfiability for a special case of Positive$\wedge$Negative

Abstract

A Boolean function in CNF format is of type Positive$\wedge$Negative} if each clause C is either positive (i.e. all literals of C are positive) or negative (i.e. all literals of C are negative). As is well known, deciding the satisfiability of such CNFs is NP-complete. We say that a CNF is of type DisjointPositive if its clauses are positive and mutually disjoint. Dually define DisjointNegative. It is shown that the satisfiability of CNFs of type DisjointPositive$\wedge$DisjointNegative can be decided in quadratic time. Moreover, the modelset can be output in polynomial total time. This is relevant since it affects not only the modelsets of CNFs of type Positive$\wedge$Negative, but more generally of type Horn$\wedge$AntiHorn. As to the latter CNFs, they e.g. occur in connection with the fixpoints of a Monotone Boolean Network. In another vein, the unsatisfiability of a Horn$\wedge$AntiHorn CNF can be demonstrated by means wholly different to the often used method of clausal proofs.

arXiv comment37 pages, 4 figures