KAIST SoC 19’

3 minute read

A propositional logic formula is in conjuncitve normal form (CNF) if it is a conjunction of disjunctions of literals $L_{i,j}$:

\[F = \bigwedge _{i=1} ^{n} \left( \bigvee _{j=1} ^m L_{i, j} \right)\]

Horn formula is special class of CNF formula that each clause contains at most one positive literal. For instance, for the literals $x_1, x_2, x_3$,

\[(\neg x_1 \vee \neg x_2 \vee x_3) \wedge (\neg x_1 \vee x_2) \wedge (\neg x_1 \vee \neg x_3) \wedge x_2 \tag{1} \label{1}\]

is a Horn formula, but

\[(\neg x_1 \vee \neg x_2 \vee x_3) \wedge (x_1 \vee x_2) \wedge (\neg x_1 \vee \neg x_3)\]

is not a Horn formula. $(x_1 \vee x_2)$ is a clause that contains two positive literals.

In general, satisfiability of CNF formula is NP-complete by Cook-Levin theorem. What makes Horn formula special is, satifiability of any Horn formula is solvable in polynomial time. In other words, Horn formula is a special type of CNF formula that poly-time satisfiability is guaranteed. Let’s call the satisfiability problem of Horn formula as Horn-SAT.

Implication Form

Horn formulas can be rewritten as conjunections of implications($\rightarrow$), called implication form. From the fact that $p \rightarrow q$ is equilvalent to $\neg p \vee q$, we can convert every clauses in Horn formula into an implication. You can check that Horn formula $\eqref{1}$ is easily rewritable into following form.

\[(x_1 \wedge x_2 \rightarrow x_3) \wedge (x_1 \rightarrow x_2) \wedge (x_1 \wedge x_3 \rightarrow false) \wedge (true \rightarrow x_2)\]

Horn Satisfiability Algorithm

Theorem. Horn-SAT is polynomial-time solvable.

To show this, claim that following algorithm is a Horn-SAT solver.

    \begin{algorithm}
    \caption{Horn-SAT}
    \begin{algorithmic}
    \INPUT{Horn formula $F$}
    \PROCEDURE{Horn-SAT}{$F$}
        \STATE $T := \emptyset$
        \WHILE{$T$ does not satisfy $F$}
            \STATE pick an unstaisfied clause $p_1 \wedge \cdots \wedge p_k \rightarrow G$
            \IF{$G$ is a variable}
                \STATE{$T:=T\cup \{G\}$}
            \ENDIF
            \IF{$G = false$}
                \RETURN{\textsc{UNSAT}}
            \ENDIF
        \ENDWHILE
        \RETURN{$T$}
    \ENDPROCEDURE
    \end{algorithmic}
    \end{algorithm}

In this algorithm, $T$ is an encoding of an assignment which collects only true variables. It starts with emptyset, which means every variable is assigned as false. After that, while loop chooses unsatisfied loop and change variables into true until there is no unsatisfied loop.

Soundness

It is untrivial that this algorithm is valid for all Horn-SAT. What happens if it goes the wrong way? What if, the algorithm assigns some variable $x=true$ after several iterations and concluded the formula is unsatisfiable, however there is a satisfying assignment that $x=false$?

To show that no such case exists, we need to show that the algorithm assigns $x=true$, then $x$ is true for all satisfying assignment. Let’s formalize this by claiming an invariant $I$ for the while loop - forall satisfying assignment $\mathcal{A} \models F$, $T \subseteq \mathcal{A}$.

The invariant holds because

  • (base) If $T = \emptyset$, it is straight-forward. For all (satisfying) assignment $\mathcal{A}$, $\emptyset \subseteq \mathcal{A}$.

  • (step) Suppose that $T \subseteq \mathcal{A}$ for all satisfying assignment $\mathcal{A}$ and $T$ does not satisfy $F$, then $T \cup \{ p \}$ satisfies the invariant. ($p$ is the positive variable in picked unsatisfied clause)

    Let the picked unsatisfied clause as $p_1 \wedge \cdots \wedge p_k \rightarrow p$ where $p_1, \cdots, p_k, p$ are variables. Then $p_1 \wedge \cdots \wedge p_k $ is true, and $p$ is false. Therefore $\{p_1, \cdots, p_k\} \subseteq T$ since these variables should be assigned as true. By the assumption, $T \subseteq \mathcal{A}$ for every satisfying assignment, so $\{p_1, \cdots, p_k\} \subseteq \mathcal{A}$. Since $\mathcal{A}$ is a satisfying assignment, $p \in \mathcal{A}$ holds, so $T \cup \{p\} \subseteq \mathcal{A}$ for every $\mathcal{A} \models F$.

Now we can show that the algorithm always solves Horn-SAT in polynomial time.

  • If the algorithm returns satisfying assignment $T$, the formula is satisfiable.

  • If algorithm returns UNSAT, take a look on the last iteration of while loop. By invariant $I$, $T \subseteq \mathcal A$ forall satisfying assignment, and there exists an unsatisfied clause that $p_1 \wedge \cdots \wedge p_k \rightarrow false$. Then $\{p_1, p_2, \cdots, p_k\} \subseteq T \subseteq \mathcal{A}$ by the same argument hence the clause is unsatisfied in $\mathcal{A}$. Therefore, there is no such $\mathcal{A}$ such that satisfies $F$, so $F$ is unsatisfiable.

  • The algorithm ends in finite time. $F$ has finite number of variable, and the while loop assigns one variable as true in each iteration. It takes quadratic time $O(N^2)$ to finish this in the worst case where $N$ is number of literals. quadratic time is because, the satisfied clause can be updated to unsatisfied as the algorithm assigns true to variables. Thus this naive algorithm needs to check all clauses to identify an unsatisfied clause.

Exercise. Refine this algorithm to run in $O(N)$. (Hint: track the number of negatives in each clause and update the number of negatives after each iteration)

Leave a comment