# Good characterization of unsatisfiable Horn3SAT formula?

Horn3SAT is $P$-complete problem under logspace reductions. Since Horn3SAT is in $P$ its complement must have short witnesses. I am looking for natural short proof that a Horn3SAT formula is not satisfiable. Examples for similar problems in $P$ are 2-coloring problem and planarity problem. A graph is not 2-colorable if and only if it contains an odd cycle. A graph is not planar if and only if it contains a subgraph that is a subdivision of $K_5$ or $K_{3,3}$.

Is there a good characterization of Horn3SAT formulas that are not satisfiable? What does constitute a natural short witness for unsatisfiable Horn3SAT formulas?

I am not interested in algorithmic proof such as running an algorithm for deciding Horn3SAT problem. I am only interested in good characterizations similar in spirit to the above two examples.

EDIT: As illustrated by the two examples above, I am only interested in characterizations of the complement set of Horn3SAT in terms of some forbidden structure.

• Is there even a "short proof that a Horn3SAT formula is" satisfiable? ​ (A satisfying assignment would have nearly-linear length.) ​ ​ ​ ​ – user12859 Aug 9 '15 at 2:36
• @RickyDemer Short proof mean polynomial in the input size (as it understood in the literature). So, yes. Horn3SAT has short proof. – Mohammad Al-Turkistany Aug 9 '15 at 2:39
• Can you be more precise about what would count as a "proof"? I'm used to a proof being something that can be checked in polynomial time. In that case, the empty string would suffice as a proof, as it is possible to check in polynomial time that a given Horn3SAT problem is not satisfiable. If you just want characterizations, it sounds more like a pure math problem rather than a CS problem. – D.W. Aug 9 '15 at 5:06
• Horn3SAT means each clause has at most 3 letrals. – Mohammad Al-Turkistany Aug 9 '15 at 18:02

You should not expect a proof that is asymptotically shorter than the formula itself. For instance, consider

$$(x_1 \implies x_2) \land (x_2 \implies x_3) \land \dots \land (x_{n-1} \implies x_n) \land x_1 \land \neg x_n.$$

This formula is not satisfiable, but any proof of unsatisfiability will need to have size $\Omega(n)$.

If you're willing to accept a "proof" of size $n$, then the formula itself arguably qualifies as a proof (as it's easy to check that a given formula is not satisfiable).

Alternatively, any chain of deductions that ends in a contradiction qualifies as a proof, where each step in the chain is a variable and its inferred truth value, as justified by a clause in the Horn3SAT formula and previously inferred variable truth values. If the formula is not satisfiable, then there must exist such a chain of deductions of size $O(n)$. The chain of deductions is easily verifiable and thus constitutes a proof of unsatisfiability. In other words, we derive a directed implication graph from the input Horn3SAT formula; the proof of unsatisfiability is then a directed path in the graph from some $x_i$ to $\neg x_i$.

If none of these meets your needs, you'll need to define what you're looking for more carefully.

• Thanks for your answer which I am aware of it. I already gave two examples above for characterizing the complement set in terms of some forbidden structure. – Mohammad Al-Turkistany Aug 9 '15 at 9:18
• However, I guess that you mean we can convert an input Horn3SAT formula into a directed implication graph and the proof of unsatisfiability then would be a directed path in the graph from some $x_i$ to $\neg x_i$. If that was your intention, please modify your answer accordingly. – Mohammad Al-Turkistany Aug 9 '15 at 13:58
• @MohammadAl-Turkistany, yes, that's exactly what I meant. I've edited the answer accordingly. – D.W. Aug 10 '15 at 1:05