Propositional Logic and SAT Problems

Original article was published by Tim de Boer on Artificial Intelligence on Medium


Propositional Logic and SAT Problems

A decision tree of a SAT-problem

In this first part of the series on Knowledge Representation (KR), we will dive into one of the well-studied fields of KR: Boolean Satisfiability Checking, in short written as SAT-checking. The idea of SAT-checking is to translate a real world problem into a question which contains multiple terms. We want to find a assignment of truth values (True or False) to these terms for which the question or problem will be solved. This assignment of truth values gives us the solution to the original problem!

Disclaimer: The series of blog posts Introduction to Knowledge Representation follows the contents of the KR course I followed at university the last eight weeks. I do not claim to be an expert in this field, nor do I claim that this blog posts will cover all material. I do hope to state all concepts provide links to other content and provide practice questions in each segment. If you cannot solve these questions with the material in this blog post, I recommend going on your own Google adventure to find out more about the concepts.

However, a problem arises when randomly assigning truth values to our terms: when we have n terms, we have to search through all n² combinations of truth values! For small problems, a computer will solve the problem in less than a couple of seconds. However, realistic problems can have up to a million terms! Try typing 1.000.000² in your calculator….

Luckily, a lot of smart people have thought about this problem and tried to come up with faster and more efficient ways of searching through all the combinations of truth values. This is the field of SAT-solving! Before we head into this field though, I would first like to give a overview of the logic on which SAT-solving is based: Propositional Logic.

Propositional Logic

Statements in a knowledge base of Propositional Logic, or PL, are facts about the current world of which we know are true of false. In PL, we make a new statement for every observation we encounter, such as ‘John has red hair’, ‘Mary is a girl’ for which we assign True of False to. We can combine statements with connectives to derive new information (which is called inference).

Below, the most important connectives are stated in order of precedence (meaning that statements should first be solved for the most important connective):

  • Not (Negation) : ¬. A statement ¬p is true when p is false.
  • And (Conjunction) : ∧. A statement p ∧ q is true when p and q are both true, else false.
  • Or (Disjunction) : ∨. A statement p ∨ q is true when p or q is true, or both are true.
  • XOR (Exclusive Disjunction) : ⊕. A statement p ∨ q is true when p or q is true, but NOT when both are true.
  • Implication : →. The logical meaning of implication p → q is a claim that if p is true, q should also be true. If p is false, I make no claim and the statement will be true regardless of q.
  • Bi-implication : ↔. A statement p ↔ q is true if p and q have the same truth value (both true of both false).

Not sure yet about the implications of these connectives? Fill in some formula’s on this website from Stanford, which will automatically derive the truth table for you.

We can derive truth tables ourselves for complex statements to find the results of all possible truth assignments, for example for the statement:
(p ∨ ¬q) ∧ r

  • Take all 8 combinations of possible truth values of p, q and r.
  • Calculate the value of ¬q from the values of q
  • Calculate the value for (p ∨ ¬q) by combining values from p and ¬q
  • Calculate the value of (p ∨ ¬q) ∧ r by combining values from (p ∨ ¬q) and r.

A statement is a tautology (or a valid statement) if the results of the truth table is true for all combinations. A statement is inconsistent (or invalid) if the result is false for all combinations. A statement is satisfiable if at least one combinations of truth assignments gives true as result.

For complex statements with multiple terms, multiple combinations of truth assignments could make the statement true. However, when solving problems with 1.000.000 terms, we really do not want to manually derive a truth table and write down all combinations of terms which would make the statement true. Researchers have found that finding a satisfiable truth assignment for complex problems writing the problem in Conjunctive Normal Form (CNF) can decrease the search time for SAT algorithms.

Practice questions PL:

PL1
Write truth tables for the following statements:
p ↔ q
¬p ∨ q
p ∧ ¬p
p ∧ q ∧ r
p → q → r
(p ∧ q) ∨ (q ∧ r)
((p ∧ q) ∧ ¬ r) → p

Are any of these statements a tautology? Or inconsistent? After trying for some minutes, check your truth table answer at this website from Stanford.

PL2
Select the logic statement answer that best expresses the following proposition:
If the test is hard and Peter does not study for the test, then Peter will fail the test.
with the following symbols:
p=the test is hard
q=Peter studies for the test
r=Peter passes the test

The answer will be presented at the end of the article.

Conjunctive Normal Form

Statements can get very complex, with lots of combinations of the connectives. However, every statement can be simplified by rewriting the statement to CNF. Transforming a problem statement to CNF gives a general form of the statement which we can give as input to a SAT-solver. A CNF is a conjunction of disjunctions, which looks like:
(p ∨ q ∨ r) ∧ (p ∨ s ∨ ¬t) ∧ (¬q ∨ s)
In which every statement in parentheses is a clause;
A letter is a variable, where it’s negation is a different variable;
An unit clause is a clause with only 1 variable;
The letter and the negation of that letter together is a literal;
A pure literal is a literal which only appears in its normal form or only in it’s negated form.
If you’re interested in how every statement can be rewritten in CNF, check this YouTube video.

Practice question CNF:
CNF1. In CNF: (p ∨ q ∨ r) ∧ (p ∨ s ∨ ¬t) ∧ (¬q ∨ s),
How many variables, clauses and literals does this CNF have?
CNF2. Is the following statement True of False?
If one clause in a CNF with multiple clauses is a tautology, the full CNF statement is a tautology as well.

The answers will be presented at the end of the article.

SAT-Problem and SAT-solvers

Now that we got our problem stated in CNF, we can discuss how SAT-solver will efficiently find a truth assignment for the problem.
SAT-solvers can be categorized in two categories: systematic and stochastic. A systematic solver will search through all possible truth assignment until it finds a satisfiable assignment, or all possible assignments have been searched and no satisfiable assignment has been found; which makes the problem unsatisfiable (UNSAT).

A systematic solver is a complete algorithm; if a satisfiable truth assignment exists, the solver will find it. On the other hand we have the stochastic solvers, which are better and faster for big, random problems but does not search through all possible truth assignments and thus will not find all the possible solutions and also cannot return UNSAT; the solver is incomplete. The classic systematic solver is the Davis Putnam Logemann Loveland (DPLL) solver, which we will discuss next. After DPLL, we will discuss a basic stochastic solver, namely the Greedy incomplete SAT (GSAT).

Practice assignment:
Google the definition for a complete algorithm, as well as for a sound algorithm.

DPLL

The DPLL algorithm uses the CNF formula to it’s advantage to postpone a random truth assignment as much as possible. The algorithm does this by the following steps:

  • Tautology checking: if one of the clauses has a tautology, this clause is impossible to satisfy, so the problem is UNSAT. This step only needs to be done once at the beginning.
  • Unit propagation: If one of the clauses is an unit clause, the variable in this clause must be true to satisfy the statement. We set the truth value of this variable to true, delete all clauses with this variable (since the clause has now been satisfied), store the truth value and erase the full literal from the CNF.
  • Pure literals: If a literal only occurs as a pure literal, the truth assignment of this literal does not matter; we can set it to true or to false, store the truth value, delete all clauses with this literal (since the clause has now been satisfied.
  • Random assignment: If after these steps, there are still clauses remaining, we have to randomly pick a variable and assign a truth value to this variable, delete all clauses with this variable (since the clause has now been satisfied) and erase the literal from the CNF. Then, unit propagation and pure literals and random assignment is repeated until the statement has no variables left, which means the statement is SAT, or until the statement has conflicting truth values for a literal and thus, cannot be satisfied with this truth assignment. We now go back till the most recent random assignment (backtracking), and choose the other truth value of that variable and see if that gives a SAT answer (otherwise we keep going back). If even after full backtracking no SAT answer is possible, the problem is UNSAT.
  • For the random assignment of a truth value to a variable, improved methods have been developed, such as choosing the most occurences of a literal (DLCS), most occurences of a variable (DLIS) and other more complex formula’s exists for splitting on variable (JW, MOM). Also a method for more efficient backtracking has been invented, called Conflict learning. This blog post explains this method and it’s differences with DPLL in a very well-done visual way.

Practice question DPLL:
Use the DPLL algorithm to try to find a satisfiable truth assignment for the following CNF statement and state which method you use for every step:
(X ∨ Y ∨ Z) ∧ ( X ∨ ¬Y) ∧ (Y ∨ ¬Z) ∧ (Z ∨ ¬X) ∧ (¬X ∨ ¬Y ∨ ¬Z)

GSAT

The basic GSAT algorithm is as follows:

  • Make a guess (random or with a certain method) for the truth values of all variables in the problem statement
  • Test how many clauses are satisfied with this assignment
  • Try to flip the truth value of one variable and test again how many clauses are satisfied; if the number of satisfied clauses increases, apply this flipping, if number of satisfied clauses decrease; do not apply this flipping. Else, just pick a random truth value for this variable. Now go to another variable until the full problem statement is SAT.
  • Since this algorithm is incomplete, you do not know if you reached the best possible truth assignment. That is why we give a maximum amount of flipping and maximum amount of full restarts (restarting from step 1). If one of these maxima is reached, we stop the algorithm.
  • This type of searching has overlap with Gradient Descent; which also searches a maximum of minimum in a landscape.

The flipping of the truth value of a random variable often does not improve the problem statement in terms of the number of satisfied clauses. A variation of GSAT has been invented to decrease the amount of flipping without improvement which is called WalkSAT:

  • If a variable flip does not turn the currently satisfied clauses to unsatisfied, this variable can me flipped without ‘’damage’’, so this variable is chosen.
  • If no such variable exists, we make a choice between two options with some chosen probability for option A or B, where option A is to do the random flip as in GSAT and option B is to chose a variable which minimizes the amount of currently satisfied clauses which become unsatisfied by this flipping.

MAX-SAT

For some unsatisfiable problem, we are still interested in the maximum amount of satisfied clauses, which can be a measure of how unsatisfiable this problem may be. MAX-SAT is also used for finding the maximum amount of satisfied clauses under some constraints, such as hard clauses, which must be satisfied. We write this as (clause, ∞), meaning a infinitive high weight for this clause. For other clauses, we also want to assign a importance-level, which we do by assigning a non-infinitive weight: (clause, 5). This clause would be 5 times more important than a normal clause.

Conclusion and further learning

This blog post covered:

  • The syntax and semantics of propositional logic;
  • Deriving truth tables of propositional logic statements and why this can be expensive for complex problems;
  • The solution for simplifying these problems, namely CNF;
  • How advanced SAT-algorithms (DPLL, GSAT) use CNF to futher simplify the problem and how these algorithms efficiently find a satisfiable truth assignment;
  • And even if a problem is UNSAT, doing research (MAX-SAT) on these problem is still useful and interesting.

For the KR course I followed at university, we had to come up with our own research concerning SAT-solving for Sudoku puzzles. In the study my group and I had set up, we compared human solving time with solving time of different variations of DPLL. In case you’re interested, the paper can be read here.

Thanks a lot for reading this blog post and I hope you learned something from it.

Answers to practice questions

PL2: p ∧ ¬q → ¬r

CNF1: 3 clauses, 5 literals and 6 variables.

CNF2: False. A CNF is a tautology if and only if all clauses are a tautology as well.

DPLL:
Multiple variations of this answer is possible depending on the random assignments, but the end answer is the same.
(X ∨ Y ∨ Z) ∧ ( X ∨ ¬Y) ∧ (Y ∨ ¬Z) ∧ (Z ∨ ¬X) ∧ (¬X ∨ ¬Y ∨ ¬Z)
No unit clauses or pure literals, so we do random assignment that X = True. Store this assignment and delete the clauses for which X=True (because these clauses are satisfied) and delete the variable ¬X from the other clauses in the CNF.
(Y ∨ ¬Z) ∧ (Z) ∧ (¬Y ∨ ¬Z)
Now we have one unit clauses: (Z). So we assign true to Z.
(Y) ∧ (¬Y)
This is a conflict, so we backtrack to the last random assignment which was X = True. So we make X = False.
(Y ∨ Z) ∧ (¬Y) ∧ (Y ∨ ¬Z)
Unit clause (¬Y) so we assign Y = False
(Z) ∧ (¬Z)
Which is also UNSAT. Since no other backtracking is possible, this problem is UNSAT. Check for yourself that beginning with a truth assignment for Y and Z would give the same result.