# Reducing 3-XOR-SAT to HORN-SAT

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?

• 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$. Dec 23, 2019 at 8:14
• 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? Dec 23, 2019 at 9:09