SAT Notation

The expression shown above can be satisfied if we set

K-SAT

SAT is NP-Complete.

k-SAT is NP-Complete for all k >= 3

Simplifying input

We keep repeating the above approach until we run out of unit clause.

Eventually we will end up with an empty formula which is satisfied, or we end up with a formula where all the clauses are of size exactly 2 in the above case since it is a 2-SAT problem.

$f$ is satisfiable is satisfiable

Graph of implications

In generic terms,

For a clause

Graph Properties

2SAT Algorithm

$f$ should be simplified before starting the algorithm.