Notes  Logic and Proof MT24, 2CNF formulas

[[Course  Logic and Proof MT24]]^{U}
 [[Notes  DAA HT23, Strongly connected components]]^{U}
 [[Notes  DAA HT23, Depthfirst search]]^{U} (for topological ordering of SCCs in satisfiability algorithm)
Flashcards
What is a 2CNF/Krom formula?
A CNF formula in which every clause has at most two literals.
Suppose $F$ is a 2CNF 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 $L \lor M$ in implication form
 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$
 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
 Assign true to all the literals in $C$ and assign false to all the literals in $\overline C$
 Return $v$
If $F$ is a 2CNF 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 $L \lor M$ in implication form
 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$
 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
 Assign true to all the literals in $C$ and assign false to all the literals in $\overline C$
 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 $L \lor M$ in implication form
 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
 Assign true to all the literals in $C$ and assign false to all the literals in $\overline C$
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 welldefined, 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.