# XOR-SAT to Horn-SAT reduction

Horn-SAT (conjunction of Horn clauses) is P-complete and XOR-SAT (conjunction of xor clauses) is in P. This means that there is a reduction from XOR-SAT to Horn-SAT weaker than a polynomial reduction. I am looking for such a reduction; can anyone help me? Thank you.

• Given an instance of XOR-SAT, solve the instance in polynomial time and then produce the Horn-SAT instance $(a \rightarrow a)$ if it was satisfiable and the instance $(\neg a \rightarrow a) \wedge (a \rightarrow \neg a)$ otherwise. The same can be done for any replacement of Horn-SAT with a language $L \not \in \{\emptyset, \Sigma^*\}$. – Yonatan N Oct 3 '16 at 0:35
• So, the right question is to give a more efficient kind of reduction, say, logspace, FO, or even logtime. The straightforward answer is to describe the computation of a Gaussian elimination algorithm by Horn clauses, which is going to be fairly unsightly. So, the right right question is if we can find something simpler. – Emil Jeřábek supports Monica Oct 3 '16 at 5:47
• @EmilJeřábek Emil you are right, I am looking for a weaker reduction than a polynimial reduction (log-space or NC for example). If we use polynomial reduction, all problems in P are complete, as Wikipedia say link – Mario Giambarioli Oct 3 '16 at 9:41

XOR-SAT is in $\mathsf{L}^{\oplus\mathsf{L}} = \oplus\mathsf{L}$ (because it can be viewed as the feasibility of a system of linear equations mod 2 hence by Allender-Beals-Ogihara). Thus using a division free determinant algorithm (e.g. by Mahajan-Vinay) we can reduce it to the problem of iterated matrix product over $F_2$ by a finegrained reduction (certainly Log-space will work but something finer like Dlogtime projection should also). Now design an $\mathsf{NC}^2$ circuit to multiply together several matrices over $F_2$ using $\{\vee,\wedge,\neg\}$-gates. Thus composing the above reductions with the reduction from CVP to HornSAT gives the final reduction.

• First of all thanks for the answer. I don’t understand the following case: if we have the simple xor instance a$\oplus$b, which is the Horn-SAT instance that is satisfiabile iff a and b have opposite truth values (a$\oplus$b is false if a and b have the same truth value)? – Mario Giambarioli Oct 30 '16 at 8:07
• @MarioGiambarioli I don't know off-hand but you can work through the chain of reductions to obtain the actual HornSAT formula. – SamiD Oct 30 '16 at 8:12
• Ok, but in the a$\oplus$b case we have only one equation a$\oplus$b=1 (not a system of equations), then we have a matrix with only one row, therefore there isn’t a determinant neither a rank (the rank is 1). So I don’t know how to apply the chain of reductions that you say. – Mario Giambarioli Oct 30 '16 at 8:31
• True. This is the answer. Since the formula you mention is satisfiable. – SamiD Oct 30 '16 at 8:41
• The part at the beginning about XOR-SAT being in parity-L. Is this a known result? Also, when I went through the paper that you link (which is great and directly relevant), I couldn't quite figure out how to apply their result to get that XOR-SAT is in parity-L. Would you be willing to explain more about this? Thank you very much for all of your help!! :) – Michael Wehar Jun 29 '18 at 23:42

$\def\F{\mathbb F_2}\let\ET\bigwedge$Let me convert my old comment above to a proper answer, as it is a much simpler construction than in the other answer.

XOR-SAT can be computed in polynomial time by Gaussian elimination. Thus, it is reducible to Horn-SAT. The reduction amounts to describing the local conditions for correctness of a transcript of a run of the Gaussian elimination algorithm, and with a reasonable representation of the output, it can be made a DLogTime reduction.

In fact, Gaussian elimination is simple enough that a (slightly optimized) reduction can be described completely explicitly. Assume that we are given a matrix $A=(a_i^j)\in\F^{m\times(n+1)}$, representing the linear system \begin{align*} a_1^1x_1+\dots+a_n^1x_n&=a_{n+1}^1\\ \tag{L}\vdots\\ a_1^mx_1+\dots+a_n^mx_n&=a_{n+1}^m \end{align*} over $\F$. We will produce a system (H) of Horn clauses such that (L) is solvable iff (H) is satisfiable. The definition of (H) will simulate the following version of Gaussian elimination over $\F$:

while $A\ne0$ do:

if some row has a unique nonzero entry in its $(n+1)$th column: REJECT

let $p$ be the first nonzero column of $A$

let $q$ be the first nonzero entry in column $p$

add row $q$ to all rows of $A$ with nonzero entry in column $p$

ACCEPT

Note that the pivot row in particular gets added to itself, which zeroes it out (we won’t need it any more). Since each iteration kills at least one column, the loop will iterate at most $n$ times.

Now, the Horn system (H) uses variables $$y_{t,i,j,a}\qquad(0\le t\le n;1\le i\le n+1;1\le j\le m;a\in\F)$$ with the intended meaning “after $t$ iterations, the $(i,j)$th entry of $A$ has value $a$”. The system consists of the “initial” clauses $$y_{0,i,j,a_i^j}\tag1$$ for $1\le i\le n+1$ and $1\le j\le m$; the negative “rejection” clauses $$\ET_{i=1}^ny_{t,i,j,0}\to\neg y_{t,n+1,j,1}\tag2$$ for $0\le t\le n$ and $1\le j\le m$; and the “next iteration” clauses $$\ET_{i=1}^{p-1}\ET_{j=1}^my_{t,i,j,0}\land\ET_{j=1}^{q-1}y_{t,p,j,0}\land y_{t,p,q,1}\land y_{t,k,l,a}\land y_{t,p,l,b}\land y_{t,k,q,c}\to y_{t+1,k,l,a+bc}\tag3$$ for $0\le t<n$, $1\le p\le n$, $1\le q\le m$, $1\le k\le n+1$, $1\le l\le m$, and $a,b,c\in\F$.

It should be clear from the discussion that (H) is equisatisfiable with (L).