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

<p>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 <strong>impossible</strong>. 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.</p>

CC BY-SA 4.0
2019-12-23T10:17:53.550Z
2019-12-23T10:17:53.550Z
Emil Jeřábek
<p>In this question - <a href="https://cstheory.stackexchange.com/questions/36704/xor-sat-to-horn-sat-reduction">XOR-SAT to Horn-SAT reduction</a>, two algorithms are described for reducing any XOR-SAT formula to a HORN-SAT formula.</p>

<p>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?</p>

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

CC BY-SA 4.0
2019-12-23T08:14:47.347Z
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$.
Emil Jeřábek
CC BY-SA 4.0
2019-12-23T09:09:23.483Z
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?
Tal K
<sat><reductions>
Reducing 3-XOR-SAT to HORN-SAT
Tal K
# Reducing 3-XOR-SAT to HORN-SAT

(Asked by: username_0 on 2019-12-23)

In this question - [XOR-SAT to Horn-SAT reduction](https://cstheory.stackexchange.com/questions/36704/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?

**Tags:** sat, reductions

> **Comments:**
> **username_1**: 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$.  
> **username_0**: 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?  

---

## 1 answers

### Answer by username_1 on 2019-12-23. Score: 6 | Accepted answer

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.


---

