Satisfiability

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$¹. As evidence of SAT’s prominence, Donald Knuth recently released a 320 page addition to The Art of Computer Programming² 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

Input:

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

Example:

• $(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)$

Output:

• $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}$

Applications

• 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