5
$\begingroup$

It is well known that satisfiability of Horn formulae can be checked in polynomial time using unit propagation.

But suppose we relax the condition for horn clauses from at most one un-negated literals to two un-negated literals. Then is it possible to prove that satisfiability of such a formula can be checked in time polynomial in the size of the formula?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
6
$\begingroup$

I think 3SAT can be reduced to your problem, since

($a_1$ OR $a_2$ OR $a_3$) AND ($b_1$ OR $b_2$ OR $b_3$) AND ($c_1$ OR $c_2$ OR $c_3$) AND ...

is satisfiable iff

(NOT $A_1$ OR $a_2$ OR $a_3$) AND ($A_1$ OR $a_1$) AND (NOT $B_1$ OR $b_2$ OR $b_3$) AND ($B_1$ OR $b_1$) AND (NOT $C_1$ OR $c_2$ OR $c_3$) AND ($C_1$ OR $c_1$) AND ...

is.

Improve this answer
$\endgroup$
10
$\begingroup$

In the paper The complexity of satisfiability problems MR0521057, Tom Schaefer characterizes exactly which general classes of satisfiability problems are in P and which are NP-complete. Those problems which are in P fall into six cases:

  • Every relation in S is satisfied when all variables are 0.

  • Every relation in S is satisfied when all variables are 1.

  • Every relation in S is definable by a CNF formula in which each conjunct has at most one negated variable.

  • Every relation in S is definable by a CNF formula in which each conjunct has at most one unnegated variable.

  • Every relation in S is definable by a CNF formula having at most 2 literals in each conjunct.

  • Every relation in S is the set of solutions of a system of linear equation over the two-element field {0,1}.

Here, S is a set of boolean relations that one takes as primitives for the language; the associated satisfiability problem is then deciding the satisfiability of a finite conjunction of such primitives. Schaefer moreover shows that any set of relations which does not fall into one of the above has a NP-complete satisfiability problem. In your example, S would be a set of boolean relations definable by a CNF formulas in which each conjunct has at most two unnegated variables. This is not in the above list, so the corresponding satisfiability problem is NP-complete.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ It does not seem to be widely known that Schaefer’s dichotomy theorem is wrong as stated in his paper, it only works if $S$ does not contain the empty relation $\varnothing$. In general, the first two cases have to be modified to “Every relation in $S-\{\varnothing\}$ is satisfied when all variables are 0” and “Every relation in $S-\{\varnothing\}$ is satisfied when all variables are 1”, respectively. For example, consider $S=\{\varnothing,x\lor y\lor\neg u\lor\neg v\}$. Then $S$ does not fall into any of the six original cases, nevertheless $\mathrm{SAT}(S)$ is trivially in P: ... $\endgroup$
    – Emil Jeřábek
    Jun 14, 2012 at 14:40
  • 1
    $\begingroup$ given an instance of $\mathrm{SAT}(S)$, either the instance includes the empty relation, in which case it is unsatisfiable, or it does not, in which case it is satisfied by the assignment of all variables to 0 (or to 1, if you prefer). $\endgroup$
    – Emil Jeřábek
    Jun 14, 2012 at 14:42
  • $\begingroup$ Thanks for the correction, Emil! I did not know about this... $\endgroup$
    – François G. Dorais
    Jun 14, 2012 at 14:54
  • $\begingroup$ The underlying error in the proof is due to a widespread confusion in the literature on Boolean clone and co-clone theory about whether nullary functions are admitted in clones. Many results on clones (e.g., descriptions of Post’s lattice) assume functions have nonzero arity, whereas the empty relation is usually not excluded from co-clones. This breaks down the duality of clones and co-clones: the minimal co-clone and the co-clone generated by the empty relation are distinct, but the only functions that are polymorphisms of the former and not of the latter are the nullary functions. $\endgroup$
    – Emil Jeřábek
    Jun 14, 2012 at 14:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.