Polynomial-time satisfiability for a special case of Positive$\wedge$Negative
This provides a polynomial-time solvable subclass for a known NP-complete problem, with implications for Horn∧AntiHorn formulas and monotone Boolean networks.
The paper shows that satisfiability of CNFs of type DisjointPositive∧DisjointNegative can be decided in quadratic time, and the model set can be output in polynomial total time.
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.