Under Construction: Consider this content a preview of the real thing which is coming soon (hopefully).

Satisfiability (SAT) is infamous because it’s the first problem proven to be in $NPC$1. As evidence of SAT’s prominence, Donald Knuth recently released a 320 page addition to The Art of Computer Programming2 dedicated to SAT. This humble work in only an introduction; however, it provides sufficient details to satisfy the needs of the majority of software professionals.

  • constrained case of 2-SAT
  • Using the local search design paradigm, it’s possible to solve in polynomial time


  1. $n$ boolean variables $x_1, x_2,…,x_n$
  2. $m$ clauses of 2 literals each (“literal” $=x_i$ or $\neg x_i$) that are or-ed together


  • $(x_1 \lor x_2) \land (\neg x_1 \lor x_3) \land (x_3 \lor x_4) \land (\neg x_2 \lor \neg x_4)$


  • $yes$ if there is an assignment that simultaneously satisfies every clause, $no$ otherwise

Example: $yes$ via $x_1=x_3=TRUE$ and $x_2=x_4=FALSE$

Solvable by:

  • Reduction to computing strongly connected components
  • Backtracking
  • Randomized local search

3-SAT is not tractable

  • Brute-force search $\approx 2^n$
  • $\approx (\frac{4}{3})^n$ via randomized local search (Schoning)

Papadimitrious’s 2-SAT Algorithm - special in that sense that’s it’s one of the only local search algorithms that guaranteed to run in polynomial time and produce a correct answer.

  1. Repeat $\log_2{n}$ times
    1. Choose random initial assignment
    2. Repeat $2n^2$ time:
      1. if current assignment satisfies all clauses, halt + report this
      2. Else, pick arbitrary unsatisfied clause and flip the value of one of it’s variables [choose between the two uniformly at random]
    3. Report unsatisfiable

Runtime = $O(2n^2 \log_2{n})$

  • Runs in polynomial time
  • Always correct on unsatisfiable instances
  • Probability of finding satisfying assignment if one exists is $\geq 1 - \frac{1}{n}$


  • Semantic Versioning solvers Under Construction

Asymptotic Complexity

Under Construction

Pseudo Code

Under Construction

Source Code

Full Repo

Relevant Files:

  • Under Construction

Click here for build and run instructions

  1. See John Cook’s 1971 paper entitled The Complexity of Theorem Proving Procedures 

  2. The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability by Donald E. Knuth. It’s available on Amazon