3
$\begingroup$

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

$\endgroup$
3
  • $\begingroup$ 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? $\endgroup$
    – D.W.
    Feb 15, 2022 at 7:47
  • $\begingroup$ 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. $\endgroup$
    – Fabio Dias
    Feb 15, 2022 at 12:41
  • $\begingroup$ 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. $\endgroup$ Feb 15, 2022 at 12:48

1 Answer 1

5
$\begingroup$

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*}$$

$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$
    – Fabio Dias
    Feb 15, 2022 at 12:36
  • $\begingroup$ 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. $\endgroup$ Feb 15, 2022 at 12:39
  • $\begingroup$ 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. $\endgroup$ Feb 15, 2022 at 12:43
  • $\begingroup$ 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. $\endgroup$
    – Fabio Dias
    Feb 15, 2022 at 12:48
  • $\begingroup$ 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 cs.stackexchange.com rather than here. $\endgroup$ Feb 15, 2022 at 12:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.