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.

翻译：CNF格式的布尔函数若每个子句C要么是正子句（即C中的所有文字均为正文字），要么是负子句（即C中的所有文字均为负文字），则称为正∧负型。众所周知，判定此类CNF的可满足性是NP完全的。若CNF的子句均为正文字且互不相交，则称其为DisjointPositive型；对称定义DisjointNegative型。研究表明，DisjointPositive∧DisjointNegative型CNF的可满足性可在二次时间内判定。此外，其模型集可在多项式总时间内输出。这一结论具有重要意义，因为它不仅影响正∧负型CNF的模型集，更广泛地影响Horn∧AntiHorn型CNF的模型集。后者例如与单调布尔网络的不动点问题相关联。