1. What’s the SAT problem?

Given a boolean formula with some variables that can be (TRUE or FALSE), can you make an algorithm that finds the value of the variables so the formula is truthful?

$ find the value of a,b,c that makes this formula truthful.
a ∧ b ∨ c

Sounds easy right? I mean, if c is true, the formula is truthful. Let’s give another example.

$ find the value of c that makes this formula truthful.
¬c ∧ c

Oh… There’s no such value of c that makes this formula truthful. Because of the properties of logical formulas, this will always false (UNSAT). But you probably figure this out.

As humans, solving this problem can be easy, our brain does some euristic for us, but if the formula is huge, with 50+ variables, it can take us a bit of time. Maybe with 5000+ variables it can take us weeks or months.

So, let’s create an algorithm for that, can you make one that is solvable in polynomial time? idk. In fact, if you did, congrats! You’ve proven that P=NP and you are now a millionare and turing award winner!

1.1 Formal Definition

The SAT problem, AKA the Satisfability Problem (and sometimes called Propositional Satisfability Problem), tackles the question wheter there exists an interpretation that satisfies a given boolean formula.

This was the first problem proven to be NP-Complete.

In this case, our goal is to return the assignments that makes a formula truthfull, or UNSAT if there’s no set of assignments possible.

SAT(a ∧ b ∨ c) -> [a:true, b:true, c:false]
SAT(a ∧ b ∨ c) -> [a:false, b:false, c:true]
SAT(¬c ∧ c) -> UNSAT

1.2 How to solve it?

Brute Force, jk.

Well, it’s NP-Complete, we cannot find a solution in a polynomial time. But what we can do is come up with heuristics to help us lower the terrible runtime in worst cases!

SAT Solvers like MiniSat, Glucose and Z3 uses heuristics and some techniques to solve for SAT. And we are going to walk through them and in the end make our own SAT solver (in rust 🦀)

2. SAT Solvers heuristics

2.1 DPLL - Davis Putman Logemann Loveland

<== TODO ==>
https://en.wikipedia.org/wiki/DPLL_algorithm
Key Concepts: Backtracking + Bruteforce + Implication Graph to detect conflicts.

1. Select random variable
2. Complete implication graph
3. If conflict, backtrack
4. If done, answer found!

2.2 CDCL - Conflict Driven Clause Learning

<== TODO ==>
https://en.wikipedia.org/wiki/Conflict-driven_clause_learning
Upgrade Non-Chronological backjumping and deep conflict analysis.

2.3 DRAFTs + Ideas

There’s also “constant propagation” and some optimizations by moore laws that can be helpful.