<p>You can’t do this. By <a href="https://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem" rel="nofollow noreferrer">Schaefer's dichotomy theorem</a>, satisfiability of sets of XOR clauses mixed with Horn clauses is an NP-complete problem, hence it does not have a poly-time reduction to Horn-SAT unless P = NP.</p>
<p>For an explicit reduction of SAT to this problem, given a CNF <span class="math-container">$F(x_1,\dots,x_n)$</span>, introduce new variables <span class="math-container">$y_1,\dots,y_n$</span> to represent <span class="math-container">$\neg x_1,\dots,\neg x_n$</span>, and let <span class="math-container">$F'(\vec x,\vec y)$</span> be the (purely negative) Horn system obtained from <span class="math-container">$F(\vec x)$</span> by replacing all positive occurrences of <span class="math-container">$x_i$</span> with <span class="math-container">$\neg y_i$</span>. Then <span class="math-container">$F$</span> is satisfiable iff <span class="math-container">$F'$</span> is satisfied by an assignment that solves the linear system
<span class="math-container">$$\begin{align*}
x_1\oplus y_1&amp;=1,\\
&amp;\;\;\vdots\\
x_n\oplus y_n&amp;=1.
\end{align*}$$</span></p>

CC BY-SA 4.0
2022-02-15T12:36:30.597Z
Thanks for your reply. At which point the link breaks? Stepping back a little, if XORSAT can be reduced to HornSAT, why would that not mean that you can write a XORSAT as a set of Horn clauses?
Fabio Dias
CC BY-SA 4.0
2022-02-15T12:39:29.610Z
For any XOR-CNF system, you can construct an *equisatisfiable* Horn-CNF system, but it will have a different set of variables that are not directly connected to variables of the original system.
Emil Jeřábek
CC BY-SA 4.0
2022-02-15T12:43:37.020Z
For a simpler example of the same phenomenon, Dual-Horn-SAT is trivially reducible to Horn-SAT by just negating all literals, but this does not mean that any dual Horn CNF is equivalent to a Horn CNF, and of course, you cannot test satisfiability of a mix of Horn and dual Horn clauses in polynomial time unless P = NP.
Emil Jeřábek
CC BY-SA 4.0
2022-02-15T12:48:51.627Z
Let's forget for now I want to mix XORSAT with HornSAT. Let's assume it impossible. But, for example, how can I produce a set of HornSAT clauses that is equisatisfiable to the simple XORSAT problem A XOR B = 1? Thanks a lot.
Fabio Dias
CC BY-SA 4.0
2022-02-15T12:54:18.797Z
I already answered that: *any* satisfiable Horn system, for example $x$, is equisatisfiable with A XOR B = 1. It seems you do not understand the basics of what *satisfiability* means; please take further questions like that to https://cs.stackexchange.com  rather than here.
Emil Jeřábek
CC BY-SA 4.0
2022-02-15T12:28:00.250Z
2022-02-15T12:35:06.850Z
2022-02-15T12:35:06.850Z
Emil Jeřábek
<p>I am trying to write a practical piece of code that solves a XORSAT by first reducing it to HornSAT and then solving the HornSAT (instead of doing Gaussian Elimination over F2). The reason for this code is that I want to find the solutions of a XORSAT that at the same time also satisfy another HornSAT (let’s call it a small HornSAT). By rewriting the XORSAT as set of HornSAT clauses and then joining these clauses with the ones of the small HornSAT I would form a big HornSAT. I am expecting that the solution of the big HornSAT would therefore be what I want: an assignment that satisfies at the same time the XORSAT and the small HornSAT.</p>
<p>In this link someone has already started a similar thread, but I can’t see how the answers can be translated to a practical implementation that can be chained to the small HornSAT: <a href="https://cstheory.stackexchange.com/questions/36704/xor-sat-to-horn-sat-reduction">XOR-SAT to Horn-SAT reduction</a></p>
<p>(edit)
Let's forget for now I want to mix XORSAT with HornSAT. Let's assume it impossible. But, for example, in none of the answers given there I can see how I would produce a set of HornSAT clauses that is equivalent to the simple XORSAT problem A XOR B = 1 (never mind a full XORSAT problem).</p>
<p>If HornSAT is P-complete, why can't a XORSAT problem be written as a set of Horn clauses? Where does the link break?</p>
<p>Any papers or books that you can point me to would also be highly appreciated.</p>
<p>Thanks a lot</p>

CC BY-SA 4.0
2022-02-15T07:47:37.137Z
Please don't refer to "first answer" and "second answer" since the sort ordering can change depending on people's settings, and can change over time as different answers acquire votes.  Can you [edit] your question to describe which approach you're consider and link to the answer you are referring to?
D.W.
CC BY-SA 4.0
2022-02-15T12:41:02.623Z
My question is more basic. Let's ignore for now I want to mix XORSAT with HornSAT. If I only wanted to transform a XORSAT into a set of horn clauses, I can't see from those answers, for example, how I would come up with a set of horn clauses that is equivalent to the basic formula A XOR B = 1, never mind a full XORSAT problem.
Fabio Dias
CC BY-SA 4.0
2022-02-15T12:48:50.840Z
There is no set of Horn clauses *equivalent* to A XOR B = 1. There is any number of sets of Horn clauses that are *equisatisfiable* with A XOR B = 1 (namely, any satisfiable set of Horn clauses will do). The existence of a reduction of the XOR-SAT problem to the Horn-SAT problem means the latter, not the former.
Emil Jeřábek
CC BY-SA 4.0
2024-08-18T23:18:20.033Z
Of related interest (similar but NOT the same):  https://cstheory.stackexchange.com/questions/200/translating-sat-to-hornsat
Shuxue Jiaoshou
<cc.complexity-theory><boolean-functions><boolean-formulas>
XORSAT to HornSAT reduction
Fabio Dias
# XORSAT to HornSAT reduction

(Asked by: username_0 on 2022-02-14)

I am trying to write a practical piece of code that solves a XORSAT by first reducing it to HornSAT and then solving the HornSAT (instead of doing Gaussian Elimination over F2). The reason for this code is that I want to find the solutions of a XORSAT that at the same time also satisfy another HornSAT (let’s call it a small HornSAT). By rewriting the XORSAT as set of HornSAT clauses and then joining these clauses with the ones of the small HornSAT I would form a big HornSAT. I am expecting that the solution of the big HornSAT would therefore be what I want: an assignment that satisfies at the same time the XORSAT and the small HornSAT.

In this link someone has already started a similar thread, but I can’t see how the answers can be translated to a practical implementation that can be chained to the small HornSAT: [XOR-SAT to Horn-SAT reduction](https://cstheory.stackexchange.com/questions/36704/xor-sat-to-horn-sat-reduction)

(edit)
Let's forget for now I want to mix XORSAT with HornSAT. Let's assume it impossible. But, for example, in none of the answers given there I can see how I would produce a set of HornSAT clauses that is equivalent to the simple XORSAT problem A XOR B = 1 (never mind a full XORSAT problem).

If HornSAT is P-complete, why can't a XORSAT problem be written as a set of Horn clauses? Where does the link break?

Any papers or books that you can point me to would also be highly appreciated.

Thanks a lot

**Tags:** cc.complexity-theory, boolean-functions, boolean-formulas

> **Comments:**
> **username_1**: Please don't refer to "first answer" and "second answer" since the sort ordering can change depending on people's settings, and can change over time as different answers acquire votes.  Can you [edit] your question to describe which approach you're consider and link to the answer you are referring to?  
> **username_0**: My question is more basic. Let's ignore for now I want to mix XORSAT with HornSAT. If I only wanted to transform a XORSAT into a set of horn clauses, I can't see from those answers, for example, how I would come up with a set of horn clauses that is equivalent to the basic formula A XOR B = 1, never mind a full XORSAT problem.  
> **username_2**: There is no set of Horn clauses *equivalent* to A XOR B = 1. There is any number of sets of Horn clauses that are *equisatisfiable* with A XOR B = 1 (namely, any satisfiable set of Horn clauses will do). The existence of a reduction of the XOR-SAT problem to the Horn-SAT problem means the latter, not the former.  
> **username_3**: Of related interest (similar but NOT the same):  https://cstheory.stackexchange.com/questions/200/translating-sat-to-hornsat  

---

## 1 answers

### Answer by username_2 on 2022-02-15. Score: 5

You can’t do this. By [Schaefer's dichotomy theorem](https://en.wikipedia.org/wiki/Schaefer%27s_dichotomy_theorem), satisfiability of sets of XOR clauses mixed with Horn clauses is an NP-complete problem, hence it does not have a poly-time reduction to Horn-SAT unless P = NP.

For an explicit reduction of SAT to this problem, given a CNF $F(x\_1,\dots,x\_n)$, introduce new variables $y\_1,\dots,y\_n$ to represent $\neg x\_1,\dots,\neg x\_n$, and let $F'(\vec x,\vec y)$ be the (purely negative) Horn system obtained from $F(\vec x)$ by replacing all positive occurrences of $x\_i$ with $\neg y\_i$. Then $F$ is satisfiable iff $F'$ is satisfied by an assignment that solves the linear system
$$\begin{align\*}
x\_1\oplus y\_1&=1,\\
&\;\;\vdots\\
x\_n\oplus y\_n&=1.
\end{align\*}$$

> **Comments:**
> **username_0**: Thanks for your reply. At which point the link breaks? Stepping back a little, if XORSAT can be reduced to HornSAT, why would that not mean that you can write a XORSAT as a set of Horn clauses?  
> **username_2**: For any XOR-CNF system, you can construct an *equisatisfiable* Horn-CNF system, but it will have a different set of variables that are not directly connected to variables of the original system.  
> **username_2**: For a simpler example of the same phenomenon, Dual-Horn-SAT is trivially reducible to Horn-SAT by just negating all literals, but this does not mean that any dual Horn CNF is equivalent to a Horn CNF, and of course, you cannot test satisfiability of a mix of Horn and dual Horn clauses in polynomial time unless P = NP.  
> **username_0**: Let's forget for now I want to mix XORSAT with HornSAT. Let's assume it impossible. But, for example, how can I produce a set of HornSAT clauses that is equisatisfiable to the simple XORSAT problem A XOR B = 1? Thanks a lot.  
> **username_2**: I already answered that: *any* satisfiable Horn system, for example $x$, is equisatisfiable with A XOR B = 1. It seems you do not understand the basics of what *satisfiability* means; please take further questions like that to https://cs.stackexchange.com  rather than here.  

---

