1
$\begingroup$

On one hand, Horn-SAT is known to be tractable in linear time - where Horn-SAT is the problem of deciding whether a given set of propositional Horn clauses (with at most one positive literal) is satisfiable or not. On the other hand, Double-SAT is NP-complete (see this post : Proving Double-SAT is NP-complete) - where Double-SAT is the problem of deciding whether a given set of propositionnal clauses has at least two models.

Let Double-Horn-SAT be the problem of deciding whether a given set of propositional Horn clauses has at least two models.

What is the complexity of Double-Horn-SAT ?

Improve this question
$\endgroup$
8
  • $\begingroup$ Perhaps this is a polynomial time solution: given a set $X$ of Horn clauses, find the first solution $S_1$, then for each variable $x_i$ repeat the following procedure: augment the set $X$ with the clause $C_{n+1} = \lnot x_i$ if $x_i=true \in S_1$, or $C_{n+1} = x_i$ if $x_i=false \in S_1$ and check if the augmented set has a solution $S_2$ (which is also a valid second solution for the original set $X$). If no solutions are found for the augmented sets, then the original $X$ doesn't have a second solution. $\endgroup$
    – Vor
    Commented Dec 3, 2013 at 21:34
  • $\begingroup$ Why? (a Horn clause is a clause with at most one positive literal ... but perhaps I'm missing something trivial ) $X \cup x_1$, $X \cup \lnot x_1$ are both valid sets of Horn clauses $\endgroup$
    – Vor
    Commented Dec 3, 2013 at 21:38
  • $\begingroup$ Oups my mistake - let me check. $\endgroup$
    – Xavier Labouze
    Commented Dec 3, 2013 at 21:39
  • $\begingroup$ I dont see why if no solutions are found for the augmented set, then the original $X$ doesn't have a second solution - because your augmented set is much more restrictive (it doesn't forbid only $S_1$.) $\endgroup$
    – Xavier Labouze
    Commented Dec 3, 2013 at 21:46
  • $\begingroup$ Suppose that in the first solution $x_1 = false$, then the augmented set $X \cup x_1$ forbids all $x_1=false$ solutions ... but the second model must differ from the first solution in at least one variable; so checking the $n$ sets (the Horn-SAT algorithm is run n times): $X \cup (\lnot)x_1$, $X \cup (\lnot)x_2$, ..., $X \cup (\lnot)x_n$ should (I'm still thinking about it) to a valid second solution (different from the first one) if and only if it exists. $\endgroup$
    – Vor
    Commented Dec 3, 2013 at 21:49

1 Answer 1

Reset to default
4
$\begingroup$

Double-Horn-SAT is polynomial-time solvable.

Given a set of Horn-clauses $X = \{C_1,C_2,...,C_n\}$ and a solution $x_1=b_1,x_2=b_2,...,x_n=b_n$, $b_i \in \{true,false\}$ we can observe that a second solution must differ in at least one variable $x_i$. So we can run the Horn-SAT algorithm $n$ times on the augmented set $X_i' = X \cup \{ \lnot x_i \}$ if in the first solution $x_i = true$ or on the augmented set $X_i' = X \cup \{ x_i \}$ if in the first solution $x_i = false$. If we find a solution for one of the $X_i'$ then it is a valid solution for the original set $X$, too and by construction it differs from the first one; otherwise the original set doesn't have a second solution, as can be easily proved by contradiction.

See also the question "Complexity of finding a second solution given a correct solution to an NP-complete problem" on cstheory and Laurent Juban, Dichotomy theorem for the generalized unique satisfiability problem (1999)

Improve this answer
$\endgroup$

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.