26
$\begingroup$

Is it possible to translate a boolean formula B into an equivalent conjunction of Horn clauses? The Wikipedia article about HornSAT seems to imply that it is, but I have not been able to chase down any reference.

Note that I do not mean "in polynomial time", but rather "at all".

$\endgroup$
  • 1
    $\begingroup$ What do you mean by "translate"? It's obvious there are SAT instances that cannot be written as a HornSAT formula. For instance, the clause (p or q). But perhaps you mean that you want a reduction such that the input SAT formula is satisfiable iff the output HornSAT formula is satisfiable? In that case of course, there's the trivial reduction since you don't care for efficiency... $\endgroup$ – arnab Aug 18 '10 at 0:17
  • $\begingroup$ I do not mean equisatisfiable, since that is indeed trivial without restrictions on efficiency. I mean equivalent as in "have the same satisfying assignments" when we consider the variables common to both the SAT instance and the corresponding HornSAT instance (if we had to add some auxiliary variables, we project them out). I agree that it shouldn't be possible, exactly for the example (P v Q), but I do not know how to prove it. Do you have a proof sketch in mind? $\endgroup$ – Evgenij Thorstensen Aug 18 '10 at 1:14
  • 3
    $\begingroup$ The question is still ambiguous. Can you explain what you mean by "project them out"? Do you mean "assignment A satisfies the SAT instance F iff there is an assignment B to auxiliary variables such that (A,B) satisfies the HornSAT instance F'"? If so, then I think you can do it by simply using the P-completeness of HornSAT. $\endgroup$ – Ryan Williams Aug 19 '10 at 3:01
24
$\begingroup$

No. Conjunctions of Horn clauses admit least Herbrand models, which disjunctions of positive literals don't. Cf. Lloyd, 1987, Foundations of Logic Programming.

Least Herbrand models have the property that they are in the intersections of all satisfiers. The Herbrand models for $(a \lor b)$ are $\{\{a\}, \{b\}, \{a,b\}\}$, which doesn't contain its intersection, so as arnab says, $(a \lor b)$ is an example of a formula which can't be expressed as a conjunction of Horn clauses.

Incorrect answer overwritten

$\endgroup$
  • $\begingroup$ Clever, but the clause -a_1 & ... & -a_n -> # is not a Horn clause. $\endgroup$ – Evgenij Thorstensen Aug 18 '10 at 14:52
  • $\begingroup$ @Evgenij: It is. $\endgroup$ – Radu GRIGore Aug 18 '10 at 15:50
  • 4
    $\begingroup$ A horn clause is a disjunction of literals with at most one positive literal. Translating the above to a disjunction of literals, we get a_1 v ... v a_n, with all the literals positive. The above clause is dual-Horn, but that doesn't help my interest. $\endgroup$ – Evgenij Thorstensen Aug 18 '10 at 16:14
  • $\begingroup$ @rgrig: No, I was confused. @Evgenij: Answer fixed. $\endgroup$ – Charles Stewart Aug 19 '10 at 10:26
5
$\begingroup$

Equisatisfiability can be achieved in the following manner (reduction from 2SAT to HornSAT). So $(p \lor q)$ can also be reduced to a Horn formula in this manner. Thanks to Joshua Gorchow for pointing out this reduction.

Input: A 2-SAT formula $\phi$, with clauses $C_1$, ..., $C_k$ on variables $x_1$, ..., $x_n$.

Construct a Horn formula $Q$ as follows:

There will be 4 $\times$ ($n$ choose $2$) $+ 2n + 1$ new variables, one for every possible possible 2-cnf clause on the $x$ variables with at most 2 literals (Not only the $C_i$ clauses in $\phi$) -- this is including unit clauses and the empty clause.. The new variable corresponding to a clause $D$ will be denoted by $z_D$.

The 4 $\times$ ($n$ choose $2$) comes from the fact that each pair of $(x_i, ~x_j)$ gives rise to four 2-cnf clauses. The $2n$ comes from the fact that each $x_i$ can create 2 unit clauses. And finally the "one" comes from the empty clause.. So the total number of possible 2-cnf clauses is $=$ 4 $\times$ ($n$ choose $2$) $+ 2n + 1$.

If a 2-cnf clause $F$ follows from two other 2-cnf clauses $D$ and $E$ by a single resolution step, then we add the Horn clause $(z_D \land z_E \to z_F)$ to $Q$... Again, we do this for all possible 2-cnf clauses -- all 4$\times$ ($n$ choose $2$) $+2n+1$ of them -- not just the $C_i$.

Then we add the unit clauses $z_{C_i}$ to $Q$, for each clause $C_i$ appearing in the input $\phi$... Finally, we add the unit clause $(\neg z_{empty})$ to $Q$.

The Horn formula $Q$ is now complete. Observe that the variables used in $Q$ are completely different from those used in $\phi$.

$\endgroup$
  • $\begingroup$ Is anyone aware of an algorithm in the other direction? Given a Horn formula $\phi_1$, is there a method to obtain an equivalent 2SAT (2CNF) expression $\phi_2$, so that $\phi_1$ is satisfiable if and only if $\phi_2$ is? Using the same set of variables, or using extra variables, or using a completely different set of variables (as done in the above answer)? Or a proof that this is impossible? $\endgroup$ – Martin Seymour Apr 30 '15 at 1:27
2
$\begingroup$

I don't think it's possible. There's no way, for example, to write $\phi = (X_1 \vee X_2 \vee \neg X_3 \vee \neg X_4)$ as a conjunction of horn clauses since $\phi$ only outlaws a single truth assignment, namely 0011. Any horn clause with less than 4 literals would outlaw more than 1 truth assignment, and horn clauses with 4 literals can only outlaw truth assignments with at most one 0.

Edit: oops didn't notice this was answered already

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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