1
$\begingroup$

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.

|cite|improve this question|||||
$\endgroup$
  • $\begingroup$ Is there even a "short proof that a Horn3SAT formula is" satisfiable? ​ (A satisfying assignment would have nearly-linear length.) ​ ​ ​ ​ $\endgroup$ – user12859 Aug 9 '15 at 2:36
  • $\begingroup$ @RickyDemer Short proof mean polynomial in the input size (as it understood in the literature). So, yes. Horn3SAT has short proof. $\endgroup$ – Mohammad Al-Turkistany Aug 9 '15 at 2:39
  • $\begingroup$ 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. $\endgroup$ – D.W.♦ Aug 9 '15 at 5:06
  • $\begingroup$ Horn3SAT means each clause has at most 3 letrals. $\endgroup$ – Mohammad Al-Turkistany Aug 9 '15 at 18:02
2
$\begingroup$

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.

|cite|improve this answer|||||
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Mohammad Al-Turkistany Aug 9 '15 at 9:18
  • $\begingroup$ 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. $\endgroup$ – Mohammad Al-Turkistany Aug 9 '15 at 13:58
  • $\begingroup$ @MohammadAl-Turkistany, yes, that's exactly what I meant. I've edited the answer accordingly. $\endgroup$ – D.W.♦ Aug 10 '15 at 1:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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