XORSAT to HornSAT reduction

Question

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

(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

Answer 1

You can’t do this. By Schaefer's 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*}$$