# 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$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

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