SAT, CDCL and Theories

In the first post of the series, I'll discuss the main idea of an SMT solver and the theories involved to understand the algorithm behind the SMT solver such as Z3.

Basic Terminologies
What is a SAT Solver?
The Algorithm behind SAT Solver
What is SMT?

Basic Terminologies

Clause

It is an expression formed by finite collection of literals (suppose Boolean literals for now) and it's logical operator. Mathematically written as

${isplaystyle l_{1}ee dots ee l_{n}}$

In this series, the clause we are gonna talk about is Disjunctive Clause, so if i say clause anywhere it means that. It is a clause where the logical operator included with the literal is OR or denoted as ∨ . Example:

`(A ∨ B)`

This denotes A "OR" B.

Conjunctive Normal Form (CNF)

It is a standard form to represent logical formulas where a formula consists of multiples clauses joined by a conjunction (AND).

Example:

`(A ∨ B) ∧ (~B ∨ C)`

What is a SAT Solver?

Suppose we are given a CNF formula:

(A ∨ B) ∧ (~B ∨ C)

There might exist some Boolean Assignment to these literals that will possibly make the whole equation True, which is our ultimate goal at this point. As for SAT solver, the only possibilities of the assignment is either True or False.

If we are to find the values of the literals that satisfies the equation, there are a variety of possible ways one being brute-force, which is self-explanatory. But, in this case, the brute-force would take 2 ^ 3 = 8 evaluations to get us the results. If we are taking thousands of literals and using brute-force to find the results, it would be realistically, not possible.

Here's where the SAT solver comes into play. Instead of just blind-folding and trying all the possible inputs, SAT solver actually uses proven algorithms to output whether the formula is satisfiable or not, hence the name SAT . It is NP-Complete, plus modern solvers can handle millions of variables in a possible time.

The Algorithm behind SAT Solver

The most core and base structure of a SAT Solver is the DPLL Algorithm. While being the base, the much more powerful version, is CDCL (Conflict-Driven Clause Learning). CDCL, while solving the formula, it learns from the conflict if it encounters it.

Decision Level

Every time our solver makes an assignment, i.e picks a variable and sets it value, it increases the decision level. {DL0, DL1...}.

Unit Propagation

Assume we have a 3 literal clause with 2 pre-defined literals resulting to false itself, because each clause needs to be satisfied, the 3rd result must be true.

Implication Graph

It is a directed graph (G = (V, E)) that visually represents the reasoning behind the variable assignments. This helps in identifying conflicts and learning new clauses (I'll talk about this later).

Here, Nodes V means variable assignment eg. A = false.
Edges, E means implications.
The logic:

If the clause (~A ∨ B) becomes a unit clause assuming we are taking A = True, then the edge from A = True -> B = True. The B must be assigned True for the clause to be True.
Assume we get a conflict for 2 formulas, we might need to assign, say, C = True for first, and C = False for second. These opposite assignments meet at a node, meaning contradiction. This will lead us to Backjumping.
Once the conflict is, CDCL analyzes the implication graph to figure out
- The set of assignments made.
- The decision edges that led us.
  
  To do this, we find a UIP (Unique Implication Point), which is basically a node from where, all the paths from the latest decision tree made, must pass-through.
Once we do the above steps, we can derive an equation that prevents the same combination that led to conflict, from appearing again. This is generally done by negating (~) the decision-tree clause.
After we have the learned clause, we backjump to the second highest decision level, and propagate the learned clause.

If all the given formulas are True, with all the variables being assigned. The solver will return SAT (Satisfiable) and the model (containing assignments). Meaning there exists a model such that F(m) = True.

However, during the process, if a conflict arises at DL0, which conflicts with already assigned literals. At this point, no further backjumping or clause learning can help to resolve it. Hence, the solver will return UNSAT (Unsatisfiable). Conceptually, no such model exist such that F(m) = True.

I'll try to show an example on how CDCL actually works, I'll just take these 2 statements out of my desk:

(A ∨ D) ∧ (A ∨ ~C ∨ ~H)
(~G ∨ ~C ∨ I) ∧ (~G ∨ H ∨ ~I)

The example taken below is assuming that we heuristically assign a variable False, only to assign it True if it needs to satisfy a clause.

Let's take things visually, first

Here we have the first clause, FYI:

The yellow circle represents decision taken by us,
The blue circle represents decision taken through unit propagation.

I'll just skip the decision making part until the conflict.

Here we see that assigning I leads to a conflict, hence we find the clause we need to learn ->

The red line shows the cut in graph which helps us finding variables, hence the learned clause is ~C ∨ ~G ∨ H , taking the negation of the variables leading to the decisions I.

After this, we backjump our way to the decision level when the G was assigned, making G: False. This gives us a model independent of I.

Hence the assignments that satisfy the above are A = False, H = False, G = False, C = True, D = True.

VSIDS (Variable State Independent Decaying Sum)

One thing that modern SAT solvers have is a technique called VSIDS. I am not gonna go deep into this, but cut-to-the-chase it stands out because it dynamically adjusts the priority of the variable, or literal, based on their involvement in conflicts to make better decisions. The idea is to prioritize variables that are more likely to cause conflicts, thereby increasing efficiency.

What happens is:

Each variable is assigned a score, starting with 0.
Every time this variable causes conflict, they are given a boost in their score. Higher the score, higher the variable is likely to cause conflict.
After each decision level, the score of the variable decays. This is important as the solver shouldn't entirely focus on a single variable if is involved in a number of conflicts but not recently.

What is SMT (Satisfiability Modulo Theories)?

In SAT solvers, we are concerned with Boolean Satisfiability, but what about different mathematical domains such as integers, bit-vectors, or arrays? This is where SMT comes into play. Built on top of SAT solvers, it determines whether or not a first-order logic formula is satisfiable or not, with respect to one more more theories involved.

There are multiple theories involved in an SMT solver, such as

Linear Integer Arithmetic (LIA) and Linear Real Arithmetic (LRA): These deal with arithmetic operations.
- (assert (< (+ (* 2 x) 3) 10)) in SMT-LIB, is same as 2x + 3 < 10
Bit-Vectors: Fixed size binary values supporting operations like XOR, Shifts... etc.

Anyways, i am not going full-fledged into the theories. A lot of theory and mathematics goes into SMT, so i will just save it up for another part.

An SMT solver from scratch - Part 1: Theory