Notes - Logic and Proof MT24, 2-CNF formulas
-
[[Course - Logic and Proof MT24]]U
- [[Notes - DAA HT23, Strongly connected components]]U
- [[Notes - DAA HT23, Depth-first search]]U (for topological ordering of SCCs in satisfiability algorithm)
Flashcards
What is a 2-CNF/Krom formula?
A CNF formula in which every clause has at most two literals.
Suppose $F$ is a 2-CNF formula containing propositional variables $p _ 1, \ldots, p _ n$. Can you state an @algorithm which will find a satisfying assignment or will return “unsatisfiable” if no assignment exists.
- Construct the implication graph $\mathcal G$
- $\mathcal G = (V, E)$
- $V = \{p _ 1, \ldots, p _ n, \lnot p _ 1, \ldots, \lnot p _ n\}$
- Rewrite all clauses in implication form (since it’s 2-CNF, all clauses are already in the form $L \lor M$ where $L, M$ are literals)
- For each pair of literals such that $L \to M$ is a clause of $F$, include edge $(L, M)$ and $(\overline M, \overline L)$, i.e. the implication and its contrapositive.
- Compute the strongly connected components $C _ 1, \ldots, C _ n$ of $\mathcal G$
- If any $p$ and $\lnot p$ are in the same strongly connected component, return unsat
- Find a topological ordering of strongly connected components
- Initialise $v := \emptyset$
- While there is an unassigned variable:
- Pick the greatest SCC in the ordering $C$ whose literals are unassigned (greatest means that no edges should point from this SCC to unvisited SCCs, but unvisited SCCs might point to this one)
- Assign true to all the literals in $C$ and assign false to all the literals in $\overline C$ (where $\overline C$ is another SCC obtained by taking the dual of all the literals)
- Return $v$
If $F$ is a 2-CNF formula containing propositional variables $p _ 1, \ldots, p _ n$ then the following will find a satisfying assignment or will return “unsatisfiable” if no assignment exists:
- Construct the implication graph $\mathcal G$
- $\mathcal G = (V, E)$
- $V = \{p _ 1, \ldots, p _ n, \lnot p _ 1, \ldots, \lnot p _ n\}$
- Rewrite all clauses in implication form (since it’s 2-CNF, all clauses are already in the form $L \lor M$ where $L, M$ are literals)
- For each pair of literals such that $L \to M$ is a clause of $F$, include edge $(L, M)$ and $(\overline M, \overline L)$, i.e. the implication and its contrapositive.
- Compute the strongly connected components $C _ 1, \ldots, C _ n$ of $\mathcal G$
- If any $p$ and $\lnot p$ are in the same strongly connected component, return unsat
- Find a topological ordering of strongly connected components $C _ 1 < C _ 2 < \cdots < C _ n$ such that if $i < j$ then there is no path from $C _ j$ to $C _ i$.
- Initialise $v := \emptyset$
- While there is an unassigned variable:
- Pick the greatest SCC in the ordering $C$ whose literals are unassigned (greatest means that no edges should point from this SCC to unvisited SCCs, but unvisited SCCs might point to this one)
- Assign true to all the literals in $C$ and assign false to all the literals in $\overline C$ (where $\overline C$ is another SCC obtained by taking the dual of all the literals)
- Return $v$
@Prove the correctness of this algorithm.
- $\mathcal G = (V, E)$
- $V = \{p _ 1, \ldots, p _ n, \lnot p _ 1, \ldots, \lnot p _ n\}$
- Rewrite all clauses in implication form (since it’s 2-CNF, all clauses are already in the form $L \lor M$ where $L, M$ are literals)
- For each pair of literals such that $L \to M$ is a clause of $F$, include edge $(L, M)$ and $(\overline M, \overline L)$, i.e. the implication and its contrapositive.
- Pick the greatest SCC in the ordering $C$ whose literals are unassigned (greatest means that no edges should point from this SCC to unvisited SCCs, but unvisited SCCs might point to this one)
- Assign true to all the literals in $C$ and assign false to all the literals in $\overline C$ (where $\overline C$ is another SCC obtained by taking the dual of all the literals)
First, say that $\mathcal G$ is consistent if there is no literal such that $L$ and $\overline L$ lie in the same SCC of $\mathcal G$. If $\mathcal G$ is consistent then the SCC can be arranged into dual pairs: if $C$ is an SCC, then $\overline C = \{\overline L : L \in C\}$ is a different SCC.
$F$ is satisfiable $\iff$ its implication graph $\mathcal G$ is consistent:
Suppose $\mathcal G$ is not consistent. Then there are paths from $p$ to $\lnot p$ and from $\lnot p$ to $p$. Then if $F$ is satisfied by $v$, $v[p] \le v[\lnot p]$ and $v[\lnot p] \le v[p]$. But then $v[p] = v[\lnot p]$, a contradiction. So $F$ must be unsatisfiable.
Suppose $\mathcal G$ is consistent. We aim to show that the above procedure produces a satisfying assignment.
Consider the loop invariant that if a literal is assigned true by $v$, then all literals reachable from $L$ are also assigned true by $v$. This guarantees the assignment $v$ satisfies $F$ on termination.
- Initialisation: No variables have been assigned.
- Maintenance: The assignments are well-defined, since for each literal $L \in C$, the dual literal $\overline L$ lies in $\overline C$, which by the consistency of $\mathcal G$ is in a different SCC. By the maximality of $C$, there is no path from $C$ to unassigned literal, and by the loop invariant, there is no path from $C$ to an SCC that is already assigned false. But then assigning to all literals in $C$ and false to all literals in $\overline C$ preserves the invariant.