1
$\begingroup$

In this question - XOR-SAT to Horn-SAT reduction, two algorithms are described for reducing any XOR-SAT formula to a HORN-SAT formula.

My question is: say I limit the clauses of an XOR-SAT formula to exactly three variables per clause, is there a specific HORN-SAT formula that is equisatisfiable with each clause? If so, why not just replace all of the XOR clauses using that formula and instead go through the algorithms described in the question above?

As an example of what I mean, it is possible to reduce any 3SAT clause to an equisatisfiable XSAT clause as described here: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Exactly-1_3-satisfiability. Is the same possible for 3-XOR-SAT and HORN-SAT?

Improve this question
$\endgroup$
2
  • $\begingroup$ Replacing each clause with an equisatisfiable one does not preserve satisfiability of the whole formula. Indeed, except for empty clauses, every clause on its own is satisfiable, hence equisatisfiable with $1$. $\endgroup$
    – Emil Jeřábek
    Dec 23, 2019 at 8:14
  • $\begingroup$ Yes, so maybe your are right and equisatisfiable isn't the correct term, but like the example I provided, does there exist a formula that each of it's solution is also a solution to the 3-XOR-SAT clause? $\endgroup$
    – Tal K
    Dec 23, 2019 at 9:09

1 Answer 1

Reset to default
6
$\begingroup$

The question is not very clear, as equisatisfiability of individual clauses does not imply equisatisfiability of the whole formulas.

However, if you mean a construction where each XOR clause is replaced by a set of of Horn clauses—possibly using new variables—so that the satisfying assignments of the original clause are exactly the projections of the satisfying assignments of the new set of clauses, this is impossible. In other words, this would make the XOR clause pp-definable from a set of Horn clauses, but all Boolean relations pp-definable from Horn clauses have the binary conjunction operation as a polymorphism, whereas conjunction is not a polymorphism of any XOR clause in more than two variables.

Improve this answer
$\endgroup$

Your Answer

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

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