The Boolean Satisfiability Problem [SAT] and SAT Solvers

by IMPERIUM

This is a quick sum-up and a beginner guide to the Boolean Satisfiability Problem. This guide is a summary of a blog post by Archy Wilhes on 0a.io. Please check out the blog post if you would like a more indepth explanation on SAT and SAT solvers.

What is the Boolean Satisfiability Problem?

The Boolean Satisfiability Problem (SAT) is the problem of determining if a propositional statement is satisfiable. A propositional statement is satisfiable when it is possible to assign some true-false values for the variables in such a way that the statement is true, else the statement is unsatisfiable. It's something like trying to flip a bunch of switches to find the setting that makes a light bulb turn on.

A propositional statement is simply made up of:

• variables
• brackets
• and the following 3 symbols
1. ¬ meaning not
2. ∧ meaning and
3. ∨ meaning or

Some examples of statements using these three symbols:

These symbols are also known as logical connectives. They are arranged in order of precedence above.

Here is a example of a propositional statement. See if you can find an assignment for the variables a, b, c and d to make the propositional statement true. To see a solution, click the solve button.

You may have noticed that we explicitly say a solution. This is because there may be multiple solutions to one propositional statement. Here are three solutions to the statement above:

Here is another example of a propositional statement. See if you can find an assignment for the variables to make the statement true:

Here is yet another example, go ahead and try to find an assignment for the variables (hint this is a trick question):

It is not satisfiable! This is because there is no value we can assign to a such that a ∧ ¬a would yield true and therefore it is impossible for the whole statement is true.

Conjunctive Normal Form

Before we get to SAT solvers we need to figure out how to represent propositional statements in a way that a SAT solver can understand it. This is where Conjunctive Normal Form (CNF) comes in. CNF is used as input for SAT solvers.

A formula in conjunctive normal form consists of:

• clauses joined by ∧ (and)
• each clause, in turn consists of variables joined by ∨ (or)
• A variable can be preceded by a ¬ (not) to negate a variable.

Here is example of a CNF:

But you might be asking why CNF. Here are two reasons why:

1. Input-related reason: Electronic circuit logic can be converted to CNF in linear time and space.
2. Solver-related: Most SAT solver variants can understand CNF. This is because it is easy to detect conflicts, it is easy to remember assignments that don't work, and its easy to be translated into simple data structures.

Now you might want to start making your own CNFs and using a SAT solver to solve them, right? Great! There is just one more thing, though the above propositional statement is in CNF form this is not quite how inputs for SAT solvers look like. The format most SAT solvers use is called the DIMACS CNF.

Here is the above CNF formatted in DIMACS CNF format:

Lets break it down:

• The first line is the problem line, hence it starts with a p. It tells us three things about the problem:
  1. The problem is in conjunctive normal form indicted by the cnf.
  2. The problem has 3 variables indicated by the 3.
  3. The problem has 4 clauses indicated by the 4.
• Each proceeding line is a clause made up of variables represented as integers. Each variable is separated by a space and a negated variable is represented as a negative integer.
• Each clause is also terminated with a 0. This allows more than one clause appear on the same line.

This is enough for you to make your own DIMACS CNF, but there are a few more details which we did not mention here. If you would like to learn more about CNFs check out this great article about CNF Files.

SAT Solvers

So what is a SAT solver? A SAT solver is a algorithm that can solve some, but not all instances of SAT. There are two classifications of SAT solvers:

1. Complete
2. Incomplete

A complete SAT solver will always tell you if a problem is satisfiable or unsatisfiable.

Incomplete SAT solvers, on the other hand, are less reliable. They may be unable to prove unsatisfiability (when it’s impossible for the formula to yield true), or unable to find a solution when the formula is satisfiable. Incomplete SAT solvers are a lot more useful in scenarios when the instances of SAT cannot be solved by complete algorithms in reasonable time.

To compare the performance between different SAT solvers, we give them a large set of formulas and see how well each performs. The set of formulas is often referred to as a benchmark instance. A solver previously lost to another solver may do better if different type of benchmark instances are used.

Many modern SAT solvers are based on the original DPLL algorithm designed in the 60’s which is a complete algorithm. Our SAT solver is not based on the original DPLL algorithm, but instead uses genetic algorithms (GA) to find an answer. In summary it guesses the first assignment then evaluates how good the assignment is with a scoring function, the GA then tries to evolve assignments with better scores. Our GA SAT solver is a incomplete SAT solver. If you would like to know why it is not complete or just learn more about GA SAT solvers please read the academic article which our SAT solver is based on.

Conclusion

Though we only scratched the surface of SAT and SAT solving it should be enough for you to get started. If you would like to submit your own CNF to be solved you can do it here.

Further Reading:

1. Boolean Satisfiability: Theory and Engineering (2014)
2. The Quest for Efficient Boolean Satisfiability Solvers (2002)
3. The SAT Phase Transition (1994)
4. Satisfiability Solvers
5. Empirical Study of the Anatomy of Modern Sat Solvers
6. Handbook of Satisfiability
7. Algorithms for the Satisfiability Problem: A Survey (1996)
8. Theory and Applications of Satisfiability Testing - SAT 2014

IMPERIUM

© Imperium 2017

---