Satisfiability

Summary

We can build a graph from a logical statement. Once we have that graph, we can build a system of Strongly Connected Components (SCCs) to determine a satisfying assignment for the original statement.

Contents

• Notation
• SAT Problem
  • Simplifying input
  • Graph of Implications
  • Finding assignments
    • Approach 1
    • Approach 2
    • 2-SAT Algorithm

Notation

Boolean formula

• n variables
  • $x_1, x_2, \ldots, x_n$
• 2n literals
  • $x_1, \bar{x_1}, x_2, \bar{x_2}, \ldots, x_n, \bar{x_n}$
• AND
  • $\land$
• OR
  • $\lor$
• Conjunctive Normal Form
  • Several clauses
    • OR of several literals
      • $\left( x_3 \lor \bar{x_5} \lor \bar{x_1} \lor x_2 \right)$
  • AND of several clauses
    • $\left( x_2 \right) \land \left( \bar{x_2} \lor x_3 \right)$
  • F is satisfiable if every clause it true

SAT Problem

INPUT: Formula F in CNF with n variables and m clauses

OUTPUT: assignment (assign T or F to each variable) statisfying if one exists

$\begin{aligned} f &= \left( \bar{x_1} \lor \bar{x_2} \lor x_3 \right) \land \left( x2_ \lor x_3 \right) \land \left( \bar{x_3} \lor \bar{x_1} \right) \land \left( \bar{x_3} \right) \ x_1 &= F \ x_2 &= T \ x_3 &= F \end{aligned}$

Simplifying input

Consider input f for 2-SAT problem

simplify unit clauses and remove them

$\begin{aligned} \left( x_3 \lor \bar{x_2} \right) &\land \underline{\left( \bar{x_1} \right)} &\land \left( x_1 \lor x_4 \right) &\land \left( \bar{x_4} \lor x_2 \right) &\land \left( \bar{x_3} \lor x_4 \right) \ \left( x_3 \lor \bar{x_2} \right) &\land \underline{\left( T \right)} &\land \left( x_1 \lor x_4 \right) &\land \left( \bar{x_4} \lor x_2 \right) &\land \left( \bar{x_3} \lor x_4 \right) \ \left( x_3 \lor \bar{x_2} \right) &\land \left( T \right) &\land \underline{\left( F \lor x_4 \right)} &\land \left( \bar{x_4} \lor x_2 \right) &\land \left( \bar{x_3} \lor x_4 \right) \ \left( x_3 \lor \bar{x_2} \right) &\land \left( T \right) &\land \underline{\left( F \lor T \right)} &\land \left( \bar{x_4} \lor x_2 \right) &\land \left( \bar{x_3} \lor x_4 \right) \ \left( x_3 \lor \bar{x_2} \right) &\land \left( T \right) &\land \left( F \lor T \right) &\land \left( \bar{x_4} \lor x_2 \right) &\land \underline{\left( \bar{x_3} \lor T \right)} \ \vdots \end{aligned}$

We either end up with an empty formula (which is definitionaly true) or a formula with exactly 2 liters per clause

Graph of Implications

Take f with all clauses of size 2, n variables, m clauses

Create a directed graph with

• 2n vertices
  • $x_1, \bar{x_1}, x_2, \bar{x_2}, \ldots, x_n, \bar{x_n}$
• 2m edges
  • implications per clause

$\left( \bar{x_1} \lor \bar{x_2} \right) \land \left( x_2 \lor x_3 \right) \land \left( \bar{x_3} \lor \bar{x_1} \right)$

$x_1 = T \implies x_2 = F$

$x_2 = T \implies x_1 = F$

$\text{path } = x_1 \rightarrow \bar{x_2} \rightarrow x_3 \rightarrow \bar{x_1}$

$x_1 \leadsto \bar{x_1} \implies x_1 = T \land \bar{x_1} = T$

$\phantom{x_1 \leadsto \bar{x_1}} \implies x_1 = T \land x_1 = F$

$\phantom{x_1 \leadsto \bar{x_1}} \implies \bot$

$x_1 \leadsto \bar{x_1} & \bar{x_1} \leadsto x_1 \implies \text{ f is not satisfiable}$

if $x_i & \bar{x_i}$ are in same SCC, then f is not satisfiable

Finding assignments

Approach 1

• Take sink SCC S
• Set S = T
  • Satisfy all literals in S
• Remove S
• Repeat

It would be great if complement to S was a source, since it would have no incoming implications.

Approach 2

• Take source SCC S’
• Set S’ = F
• Remove literals
• Repeat

Starting with a source or a sink is the same thing

2-SAT Algorithm

If for all i, $x_i & \bar{x_i}$ are in different SCCs, then $S \text{ is a sink SCC } \implies \bar{S} \text{ is a source SCC}$

2SAT(f):
  Simplify f to assume all clauses are of size exactly 2
  Construct graph G for f
  while G has nodes:
    Take a sink SCC S
    Set S = T
    Remove S