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