Logic Puzzles and SAT Solvers: A match made in heaven
Logic puzzles are quite infectious and a challenging exercise for the gray cells. Typically, they involve a set of logic statements and a goal. They can be solved by systematic reasoning about the statements and deducing new facts, finally arriving at the solution. This can get quite complicated especially when there are many statements and require a series of complex logical deductions.
It sounds like a problem tailor-made for computers using automated formal reasoning tools like SAT (Boolean Satisfiability) solvers. In this post, we will cover the following:
- A brief primer on the relevant logic background
- An example logic puzzle
- Encoding it as a logic formula
- Using a SAT solver (MiniSat) to solve it
- Conclusion
A brief primer on logic
The basic concept in propositional logic is an atomic proposition. A proposition is a statement that can be assigned a True or False value, like:
- “The earth is a planet”
- “2 minus 1 equals 0”
Atomic propositions can be represented by boolean variables and combined to create compound propositions using logical connectives like ∨ (or/disjunction), ∧ (and/conjunction), ¬(negation), →(implies), ↔(iff).
A boolean formula in propositional logic represents a compound proposition that evaluates to True or False, given an assignment of boolean variables. Let’s consider a boolean formula “p ∨ (¬r ∨ q)” with three variables p, q, r. The truth table below shows several satisfying assignments.
Let’s consider a boolean formula “(p∨ q) ∧ (p∨ ¬q)∧ (¬p∨ q) ∧ (¬p∨ ¬q)” with 2 variables p, q. The truth table below has no satisfying assignments.
Boolean satisfiability (SAT)
SAT refers to the problem of determining whether a boolean formula is satisfiable i.e. determining the existence of an assignment of boolean variables (to True or False) that satisfies it (makes it True). The boolean formula “p ∨ (¬r ∨ q)” is satisfiable with many satisfying assignments e.g. “(p, r, q) = (F, F, F)”; (refer to the truth table above). On the other hand, the boolean formula “(p∨ q) ∧ (p∨ ¬q)∧ (¬p∨ q) ∧ (¬p∨ ¬q)” is unsatisfiable; it has 4 clauses all of which cannot be true simultaneously (refer to the truth table above).
The SAT problem is proven to be NP-complete. However, in practice, SAT solvers like MiniSat use heuristic algorithms and simpler input structures to solve extensive formulas involving millions of boolean variables and clauses.
A clause is a disjunction of one or more literals (p, q, ¬r). A boolean formula in the Conjunctive Normal Form (CNF), is a conjunction of clauses (AND of OR’s). For instance, the boolean formula “(p ∨ q) ∧ (¬r ∨ s) ∧ …” is in CNF. CNF is useful as input to automated reasoning tools like the MiniSat solver as it has a simpler structure and fewer connectives.
Any boolean formula can be transformed to an equivalent boolean formula in CNF using rules like De Morgan’s laws, logical equivalences, distributive law, double negation elimination. In some cases, naive transformation to CNF can result in an exponential explosion in the size of the formula.
SAT Solvers
A SAT solver (like MiniSat) takes a boolean formula as input in CNF (DIMACS representation) and outputs whether it is satisfiable or unsatisfiable. If it is satisfiable, it also finds a satisfying assignment to the boolean variables.
A logic puzzle
One typical logic puzzle (see image below) involves finding a 3-digit code to unlock a lock using the provided logic statements.
Let’s first try to solve the problem using logical reasoning. Each logic statement asserts some facts about the correctness and placement of the 3 digits (0–8) in the 3 available slots (1–3). Let’s name the five rules as R1, R2, R3, R4, and R5. For instance, R1 asserts that one digit (6,8,2) is both valid and in the correct slot. The following deductions can be drawn based on the rules:
- Digits 7, 3, and 8 are invalid (by R₄)
- Digit 0 is correct and in slots 1 or 2 as a) digits 7, 8 are invalid (by R₄) and b) it is in the incorrect slot (by R5)
- By R₃ and given that digit 0 is correct (by 2.), 0 cannot be in slot 2 and is therefore in slot 1. So we have (0 * *) as the code so far
- Either digit 6 or 2 is valid and in the correct slot (by R1 and as digit 8 is invalid by R₄)
- By R₃, R5 digit 2 in slot 3 is correct, and hence digit 6 is invalid. So we have (0 * 2) as the code so far
- Considering R₂ and the fact that 6 is invalid (by R1, R3, R5) both 1 and 4 are candidates for slot 2. As the correct value is in the wrong slot (by R₂), 1 is an invalid choice for slot 2. Hence 4 is the right answer for slot 2 with the final solution being (0 4 2)
As is evident, logical reasoning requires a systematic approach for deriving deductions from given logic statements to finally arrive at the conclusion. However, even in this simple example, it gets quite complicated to keep track of the deductions.
The alternative is to express the problem formally as a boolean formula and use automated reasoning tools (like MiniSat) to solve it. This works at scale and also, expressing the problem formally brings clarity.
Encoding it as a logic formula
The prerequisite to using a SAT solver is to represent the puzzle as a boolean formula. The first step is to identify the boolean variables and then string them together to represent the rules above i.e. R1, R2, R3, R4, and R5. The two important elements are the digit and the slot in which it is placed. If we use boolean variables ∀i ∈ (1–3), ∀j ∈ (0–8) Sij (where i is the slot and j is the digit placed in the slot) to represent if slot i is occupied by digit j. For e.g. slot 1 is occupied by digit 0, then S10 is True.
We translate the 5 rules and 2 latent conditions to the following 7 boolean formulas.
- Rule R₄ states that code 738 has all invalid digits. This implies that variables S17, S13, S18, S27, S23, S28, S37, S33, S38 are all False. We will use this to optimize the boolean formulas representing the other rules. This is represented by the boolean formula below.
2. Rule R1 states that the code 682 has one digit valid and in the correct slot. This implies that at least one of the following is true and all other placements of digits 6,8, or 2 incorrect:
- Slot 1 occupied by digit 6
- Slot 2 occupied by digit 8
- Slot 3 occupied by digit 2
This is represented by the boolean formula below with 3 clauses representing the above possibilities (vars marked in red). For e.g. if digit 6 is valid and in slot 1 then slot 1 cannot hold digits 8, 2 and furthermore slot 2 and 3 cannot hold 6, 8 or 2.
3. Rule R₂ states that the code 614 has one digit valid but in the incorrect slot. This implies that at least one of the following is true (with all other placements of digits to slots being invalid):
- Slot 1 is occupied by digits 1 or 4
- Slot 2 is occupied by digits 6 or 4
- Slot 3 is occupied by digits 6 or 1
This is represented by the boolean formula below with 6 clauses representing the above possibilities (vars marked in red).
4. Rule R₃ states that the code 206 has two valid digits but placed in incorrect slots. This implies that there are three valid 2 digit combinations i.e. (20),(26),(06) and their nine possible slot placement options are:
(0 2 *) (6 2 *) (0 6 *)
(0 * 2) (6 * 2) (6 * 0)
(* 2 0) (* 6 2) (* 6 0)
This is represented by the boolean formula below with 9 clauses representing the above possibilities (vars marked in red)
5. Rule R5 states that the code 870 has 1 valid digit but placed in the incorrect slot. This implies that at least one of the following is true:
- Slot 1 is occupied by digits 7 or 0
- Slot 2 is occupied by digits 8 or 0
- Slot 3 is occupied by digits 8 or 7
This is represented by the boolean formula below with 6 clauses representing the above possibilities (vars marked in red)
6. At least one: Each slot 1,2,3 must be occupied by at least one digit. The following 3 clauses for each slot represent this rule
7. At most one: Each slot 1,2,3 must be occupied by at the most one digit. The following 15 clauses (3 slots * 5 digits) for each slot represent this rule (ignoring digits 7,3,8 by R₄)
8. Remove variables that are definitively False: We add a formula to remove the False or missing variables. The missing variables are included only for completeness as the SAT solver takes integers as variables and in our formulation variables like {S[1–9], S[1–3]5, S[1–3]9} are irrelevant. The variables that have been deduced as False in the previous steps are S16, S21, S34 (by R2), S30 (by R5), and S12, S20, S36 (by R3).
Using a solver to solve it
We have translated the rules R1, R2, R3, R4, R5, and the at least one, at most one, invalid vars conditions into 8 optimized boolean formulas above. The combined (ANDed) boolean formula composed of the 8 individual formulas represents the puzzle and a satisfying boolean variable assignment will represent the solution i.e. the boolean variables ∀i ∈ (1–3), ∀j ∈ (0–8) Sij (where i is the slot and j is the digit placed in the slot) that are set to True. There should be 3 such variables for slots (1,2,3) set to True and the rest set to False
As stated earlier, a SAT solver (like MiniSat) takes a boolean formula as input in CNF (DIMACS representation) and outputs whether it is satisfiable (with an assignment) or unsatisfiable. We will convert each of these 8 boolean formulas into CNF, combine them into one input CNF file, and then use the solver.
Conversion to CNF
For the purposes of this post, we have used a hosted logic tool boolean formula optimization, and subsequent conversion to CNF (In a future post we will cover CNF conversion).
As an example, the optimized formula for Rule R1 is:
Using the tool to convert this formula to CNF (AND of OR’s) we get the following:
This can be converted to DIMACS format (1 line per clause) as below:
In a similar manner, we convert all 8 formulas to DIMACS format and concatenate them in one CNF file for input to MiniSat. This is the equivalent of ANDing all 8 formulas in CNF form.
Caveat: For some of the 8 formulas above we used the online logic tool to optimize the expression further before converting to CNF)
Running MiniSat
MiniSat requires as input a combined CNF file for all the 8 boolean formulas. Executing it as “minisat all.cnf out” we get the following content in the “out” file. It indicates that the solver was able to find a satisfying assignment (indicated by SAT) and the solution is the variables below that are not negated i.e. 10, 24, and 32. These indicate that the variables S10, S24, and S32 are true (and the rest False); The solution is thus (0 4 2) which matches what we found using the logical deduction approach earlier.
In order to conclude that this is the only satisfying assignment, we will add the negation of the solution above and see if there are any other satisfying assignments or the problem is unsatisfiable. The negation of the above solution is:
Adding the negation to all.cnf and executing it as “minisat all.cnf out” we get the following output. It indicates that the solver was unable to find a satisfying assignment (indicated by UNSATISFIABLE). Thus (0 4 2) is the only solution.
Conclusion
We have demonstrated that expressing a logic puzzle formally as a boolean formula and using a SAT solver to find a satisfying assignment works and brings clarity, especially when non-trivial deductions are required or the problem size is large. Many problems (far beyond puzzles) can be expressed in terms of boolean logic and solved using SAT solvers. We also saw that, like other approaches, this too requires optimizing the boolean formula representation of the different logical facets of the problem.
We conclude that formally expressing problems as boolean logic is powerful and SAT solvers are very useful tools to include in your toolbox
References
- Boolean Satisfiability
- Conjunctive Normal Form (CNF)
- DIMACS
- A truth table generator was used to generate the truth table used in this post
- A hosted logic tool was used for boolean formula optimization and subsequent conversion to CNF
- SAT solver MiniSat
- Running MiniSat on Mac
