# Complexity of Double-Horn-SAT?

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 ?

• 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. – Vor Dec 3 '13 at 21:34
• 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 – Vor Dec 3 '13 at 21:38
• Oups my mistake - let me check. – Xavier Labouze Dec 3 '13 at 21:39
• 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$.) – Xavier Labouze Dec 3 '13 at 21:46
• 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. – Vor Dec 3 '13 at 21:49

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.