Using `z3` To Solve Logic Puzzles

Recently, I learned about point-free programming. The day after I learned about it, I was idly wishing for a puzzle book on converting program code to point-free form. A point-free programming puzzle book would be a good exercise on how well I can compose functions. Sadly, I'm not aware of such a puzzle book, nor am I qualified to write one.

However, thinking of puzzles again reminded me of how I liked logic puzzle books when I was younger (anyone remember PennyPress?). A few years ago, I solved a logic puzzle using an SMT solver out of curiosity. I was motivated to do this after seeing Claire Wolf doing the same to solve a similar "guess the combination to the lock given hints" puzzle. I'd intended to write a blog post about how I mapped the word problem of a logic puzzle to an SMT query, but I never followed up on it.

I know my last post was in late 2019. 2020 through 2023 has not been kind to the world and our collective social/mental bandwidth. Mine included. So while the thought of fun logic puzzles from my youth were fresh in my head yesterday (2023-06-30), I forced myself remember how I solved a logic puzzle with an SMT solver 5 years ago. And at last I'm going to document it here.

Prerequisites

This post assumes a background in Boolean logic and/or one programming language (along with how to use its Boolean operators). Familiarity with S-expressions is also a plus, because the input to the z3 program we're using uses S-expressions. However, I will be explaining all the input we send to z3 line-by-line. So feel free to learn about S-expressions at your own pace while or after reading this post.

When referencing concepts common in other programming languages, I refer to Rust documentation, because at this writing (2023-07-01), it's easiest for me to find the analogous concepts in the Rust language's documentation.

And lastly, you should know what a logic puzzle is. Enjoying solving logic puzzles is a nice bonus :).

What is an SMT Solver?

Before I explain what an SMT solver is, and how to use them to solve puzzles, I need to explain what SAT and SAT solvers are as prerequisites.

Suppose you have some Boolean expressions- a bunch of Boolean variables chained together- with Boolean operators- &&, ||, !, etc. Here is an example query:

A || (B && !C)
B && C

SAT, or SATisfiability, is the process of determining whether a set of Boolean expressions like above can all be made true (1) for one or more combination of the values for the given Boolean variables.

Given n Boolean variables, where each variable has 2 possible values- true (1) and false (0)- you can determine whether there's an assignment that satisfies all the Boolean expressions by "substituting all combinations of values for the variables in the expressions" (brute-forcing).

For instance, here's how we can brute-force the above query in (up to) 8 (2^3) easy steps:

A=0,B=0,C=0: UNSAT
```
0 || (0 && !0) = 0
0 && 0 = 0
```
A=1,B=0,C=0: UNSAT
```
1 || (0 && !0) = 1
0 && 0 = 0
```
A=0,B=1,C=0: UNSAT
```
0 || (1 && !0) = 1
1 && 0 = 0
```
A=1,B=1,C=0: UNSAT
```
1 || (1 && !0) = 1
1 && 0 = 0
```
A=0,B=0,C=1: UNSAT
```
0 || (0 && !1) = 0
0 && 0 = 0
```
A=1,B=0,C=1: UNSAT
```
1 || (0 && !1) = 1
0 && 1 = 0
```
A=0,B=1,C=1: UNSAT
```
0 || (1 && !1) = 0
1 && 1 = 1
```
A=1,B=1,C=1: SAT
```
1 || (1 && !1) = 1
1 && 1 = 1
```

Indeed, our query is SATisfiable when all three Boolean variables are set to 1.

SAT Solvers

When checking for satisfiability, if just one combination of variable values makes all the expressions in your query equal to 1, you're done- the query is SAT. Unfortunately, this means you have to try 2^n combinations of values for n Boolean variables if you have a query that is UNSATisfiable. And even if the query is SAT, you may have to try many combinations of variable values before you find a combination that returns SAT, such as the above example.

To make matters worse, real-world SAT problems can have thousands of expressions and millions of variables. Unlike my toy example above, it is completely impractical to try to brute-force 2^1000000 different combinations of Boolean variables. It is believed that for some SAT problems, there is no better strategy than brute forcing all 2^n combinations. However, real-world SAT problems are better behaved and can be solved efficiently using, for instance, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm or Conflict-Driven Clause Learning (CDCL) algorithm.

SAT solvers are a type of computer program optimized for solving Boolean satisfiability problems. They take advantage of these algorithms and hueristics common to real-world SAT problems to efficiently find whether a query is SAT or UNSAT1 .

SMT And SMT Solvers

Satisfiability Modulo Theory (SMT) problems and solvers are what you get when you're no longer limited to queries of just Boolean variables. Queries can be taken over Booleans, reals, integers, arrays of Booleans, functions, enumerations, and many more! You can even create queries of combinations of these data types! As might be expected, by relying on queries over data types besides Booleans can result in dramatic speedups, as well as dramatic increases in complexity :).

While some data types map nicely2 to Boolean expressions such as bitvectors, modern SMT solver use theories to map more complex data types back to Boolean expressions. Just like how Booleans are governed by the theory of Boolean algebra, each data type an SMT solver supports has a theory that explains "what you can and cannot do" with the data type. For instance, consider the following expressions, comparing equality of integers I, J, and K:

(I == 1) && (J == I + 1)
(I == 2) || (K == J + 3)
(I == 2) && (J == K + 2)

The expressions I == 1, J == I + 1, I == 2, K == J + 3, J ==K + 2 and all yield Boolean values, and can therefore be converted to and from Boolean values A, B, C, D, and E respectively:

A && B
C || D
C && E

While Boolean expressions can be solved for using the above algorithms for SAT, solving for equality is governed by the congruence closure, and the theory of integers is governed by, well, number theory. The DPLL/CDCL algorithms can be modified to handle conversion to and from Boolean expressions, as well as handle congruence closure and other theories. This is known as the DPLL(T) framework3 .

`z3` And SMT-LIB

Our SMT solver of choice will be Microsoft Research's z3. Other SMT solvers exist, such as yices, and thanks to each using different algorithms, there is not a single SMT solver that solves all practical SMT problems better than the others. Speedups and slowdowns can be dramatic depending on which SMT solver you use4 . However, a query to solve a logic puzzle will not tax any SMT solver, so seeing that I'm familiar with its API, I chose z3.

For our purposes, z3 is invoked as the following:

z3 -smt2 model.txt

model.txt is a text file we will create in SMT-LIB format. SMT-LIB is an S-expression-based text input/output format widely-supported by SMT solvers, z3 included. It contains commands to construct input queries for many different theories, run the solver on your query via check-sat, and examine the solver's output. In particular, after running check-sat, you can use SMT-LIB to:

Display the value of the variables the solver used to satisfy your query (get-model, where the values are written in terms of define-fun).
Display a proof that your query is UNSAT (get-proof).
Evaluate functions that the solver knows about, including functions defined for you by the solver (get-value)!

As is custom for an S-expression format, SMT-LIB has a large amount of parantheses to represent nested data structures. While I show a generic example of how to use all our needed SMT-LIB commands, I will be skimming over the meaning of the parentheses nesting for this example application.

An Example In SMT-LIB Format

Like SAT solvers, SMT solvers can handle Boolean expressions just fine, as long as they're in the SMT-LIB format. Using the SAT example earlier in the post, the equivalent SMT-LIB query would look something like this:

(set-option :produce-models true)
(set-logic QF_UF)

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (or a (and b (not c)))) ; A || (B && C)
(assert (and b c)) ; B && C
(check-sat)
(get-model)

There are a few things to note comparing the SAT example I created above:

The first line set-option :produce-models true enables the get-model command. The second line set-logic restricts the data types and theories that the solver will use. The SMT-LIB website provides a catalog of logics that can be used with set-logic, and QF_UF is a simple sub-logic suitable for a Boolean-only query.

Although z3 tolerates the first two lines missing, its good practice to add those lines for other solvers like yices and for optimizing. Assuming that some data types and theories can't occur in a given query sometimes allows the solver to speed up proofs.

Variables are not implicit in SMT-LIB, and need to be declared with declare-const. declare-const takes a variable name, and a type- Bool in this case, but an SMT solver understands other types. During check-sat, the solver will fill in a value for you for each variable. The value of a variable is the same everywhere that the variable is used, hence the const part.
As is traditional with S-expressions, operators such as and, or, etc are written in prefix notation rather than infix notation. Parentheses are required around operators and their arguments to actually evaluate the expression/do the calculation5 .
The Boolean expressions you want to check for satisfiability aren't implicit either; you must tell the solver about your query using one more more asserts. The solver must find a way to make all asserts true simultaneously for your query to return SAT. A query without any asserts returns true.
Comments are preceded with ;.
check-sat checks whether your query is SAT or UNSAT, and nothing else. In contrast, get-model returns the value of the variables the solver used to satisfy your query if your query was SAT. In this case, the output of the solver, including the variable values chosen, matches the SAT example:
```
sat
(
  (define-fun b () Bool
    true)
  (define-fun a () Bool
    true)
  (define-fun c () Bool
    true)
)
```
Additionally, there is also get-value. As will become clear later, get-value is sometimes more useful than get-model for presenting information about a model which satisfies your query. get-value is especially when you're interested in the return values of uninterpreted functions.
Although not represented in the above example, there are a few additional operators available to the Bool theory in SMT-LIB that are not available in a SAT solver due to being polymorphic: =, distinct, and ite.
- = checks whether two generic types T have equal value. If T is Bool, this is equivalent to XNOR. Unlike many programming languages, SMT-LIB uses single-equals (=), not double-equals (==) for comparison.
- distinct checks whether two generic types T are not of equal value. If T is Bool, this is equivalent to XOR.
- ite corresponds to if-then-else expressions in your favorite programming language. The if predicate requires Bool, while the then and else branches of the expression require a T as input.
  
  The entire expression returns a T as output. It returns the value of the then branch when the if predicate evaluates to true, and returns the value of the else branch when the if predicate evaluates to false. When T is Bool, ite has the following truth table:
  
  I T E O
  0 0 0 0
  0 0 1 1
  0 1 0 0
  0 1 1 1
  1 0 0 0
  1 0 1 0
  1 1 0 1
  1 1 1 1

I	T	E	O
0	0	0	0
0	0	1	1
0	1	0	0
0	1	1	1
1	0	0	0
1	0	1	0
1	1	0	1
1	1	1	1

While the above example doesn't really use an SMT solver's true power, it does illustrate the fundamentals of how to interface with one. We will discuss how to use other datatypes and theories with SMT-LIB as we turn a logic puzzle into an SMT query.

SMT And Logic Puzzles

With the whirlwind introduction to SMT out of the way, my goal with this post is to show you how to map the word problem presented by a logic puzzle to a SATisfiable SMT query. I will introduce an example logic puzzle first, and then show how to use various SMT-LIB commands to create some datatypes and constraints to represent the puzzle.

At a high level, if you visualize a logic puzzle grid, such as the one below, the conversion process looks like this:

The SMT theory of algebraic datatypes will be used to represent the headers of each row and column of data.
Correlating each row to the correct columns of data will be represented by the theory of uninterpreted functions .
Clues/hints and constraints implicit in a logic puzzle will be represented by asserts.

An empty logic puzzle grid corresponding to the puzzle described in the next section.

This empty logic puzzle contains 9 rows and columns, along with headers for each row and column. The column headers, in left-to-right order, are: Batman, Jake, Dibii, Lazer, Sleep, Ball, 1, 2, and 3. The row headers in top-to-bottom order, are: Ruby, Spot, and Starbuck, 1, 2, 3, Lazer, Sleep, and Ball.

Each set of 3 row and column headers belong to the same category:

Batman, Jake, Dibii are tomcats.
Ruby, Spot, and Starbuck are queen cats.
Lazer, sleep, and ball are activities.
1, 2, and 3 are number of kittens.

To solve the puzzle, you are intended to mark each table entry a ✓ if the row and column are associated with each other, or ✗ if the row and column are not associated with each other, based on clues given to you (not represented in the above image).

A table entry whose row and column are of the same category does not need to be marked. The pictured table represents this by completely omitting such entries, making the table similar to an upper triangular matrix.

The bottom part of the puzzle consists of a table with the columns queen, tom, activity, and number of kittens. The column queen is filled in for you with Ruby, Spot, and Starbuck. You fill the remaining rows of this table based on which row and columns you marked with a ✓ in the above table.

I got the logic puzzle template (before filling in the headers) from Daydream Puzzles.

An Example Puzzle

For this post, I'll be using a puzzle from Aha! Puzzles as an example. I'm not going to copy the puzzle description, since a person presumably spent time to create the puzzle (among others), and I don't want to steal their work. Instead I will paraphrase the puzzle and grid, which describes a set of cats.

Description

There are three queens named Ruby, Spot, and Starbuck.
Each queen has a partner, favorite activity, and number of kittens. As is customary for this type of problem, it is implied that each Queen has a different partner, favorite activity, and number of kittens.
The possible partners (toms, as in tomcats) are: Batman, Jake, and Dibii.
Activities include: chasing a Lazer, Sleeping, and chasing a Ball.
Each queen/tom pair has between 1 to 3 kittens (inclusive).

Given the above information, and the following clues, figure out each queen's partner, favorite activity, and the number of kittens they have.

Clues

The puzzle is intended to have a unique answer. However, using only the description above, there are multiple correct answers. The clues below are intended to limit the multiple correct answers down to a single unique answer6 :

Batman's partner likes to chase a ball. She was not Starbuck.
Dibii's partner liked the lazer.
Ruby was a cat who liked to sleep.
Starbuck has two more kittens than whoever Batman's companion is.

Mapping The Puzzle To An SMT Query

Now that we have a puzzle, we can map the textual description to a query and a mathematical model that the SMT solver will return. Let's create the query piece by piece, starting with initial setup code:

(set-option :produce-models true)
(set-logic ALL)

The first two lines we've already seen, but we have a new logic ALL. set-logic ALL is a bit of a cop-out; SMT-LIB allows ALL for applications which generate queries on-the-fly. ALL is not intended for handwritten queries. Unfortunately, z3 doesn't really have that many logics that support datatypes. And none of the logics that do support datatypes seem to support both integers and uninterpreted functions.7

So, without any better options for now, I'm just making explicit that z3 should use "whatever means necessary" to solve the logic puzzle8 .

Enums

declare-datatypes is part of the most recent version of SMT-LIB, version 2.6. It is a very general function that allows you to create complex data types, including recursive data types. In our usage we will only be using it to create the equivalent of enums without data in other programming languages9 .

In general, you create an enum Foo whose variants A, B, C (and more, if wish) have data using the following syntax10 :

(declare-datatypes ((Foo 0)) (((A) (B) (C))))

Anywhere in your query where a value of type Foo is used, the SMT solver has no choice but to make the value either A, B, or C. Additionally, the following properties hold11 :

A = A, B = B, and C = C (reflexivity)
A != B, B != C, and A != C (antisymmetry).

This can be confirmed with the following query, which returns SAT:

(declare-datatypes ((Foo 0)) (((A) (B) (C))))
(assert (and (= A A) (= B B) (= C C)))
(assert (and (distinct A B) (distinct A C) (distinct B C)))
(check-sat)

With the above syntax and properties in mind, the names of the cats and their activities correspond very nicely to enums whose variants don't have data:

(declare-datatypes ((Tom 0)) (((Batman) (Jake) (Dibii))))
(declare-datatypes ((Queen 0)) (((Ruby) (Spot) (Starbuck))))
(declare-datatypes ((Activities 0)) (((Lazer) (Sleep) (Ball))))

Uninterpreted Functions

Functions form the backbone of programming languages and mathematics, and SMT formulas are no exception. We can create pure functions to abstract away common parts of our query using define-fun. Here is an example add function that "adds one to its input Int":

(define-fun add ((x Int)) Int (+ x 1))
(check-sat)
(get-value ((add 1) (add 2) (add 10)))

The above query returns SAT in response to check-sat. After check-sat, your model has an add function that the solver can call.

We don't have any asserts in the above query, so get-model returns nothing. However, we can display the result of calls to our add function using get-value. get-value takes a single argument, but this single argument can take an arbitrary number of terms. Each of the three terms to the get-value call above will make the solver read, evaluate, and print the results of calling your add function on various integers- exciting!

sat
(((add 1) 2)
 ((add 2) 3)
 ((add 10) 11))

Not only can we define functions, we can also declare functions, without bothering to define/fill in the function body! We can request the solver to fill in the function body for us by using declare-fun:

(declare-fun add_two (Int) Int)
(check-sat)
(get-model)
(get-value ((add_two 1)))

The above query returns sat in response to check-sat. get-model will then return the definition of add_two that the solver created:

sat
(
  (define-fun add_two ((x!0 Int)) Int
    0)
)
(((add_two 1) 0))

In this case add_two returns the literal 0. Not particularly interesting. What if we add an assert, to force add_two to return 3 when given the input 1?

(declare-fun add_two (Int) Int)
(assert (= (add_two 1) 3))
(check-sat)
(get-model)
(get-value ((add_two 1)))

sat
(
  (define-fun add_two ((x!0 Int)) Int
    3)
)
(((add_two 1) 3))

It's a function that returns 3 for all inputs. Now the solver is being cute. "Technically correct" is the best type of correct. The solver won't create a more interesting function body unless forced to via proper constraints on the input arguments and return values12 .

We will constrain our uninterpreted functions shortly, but for now, let's declare 4 uninterpreted functions with declare-fun. These functions will in fact return the answers for our logic puzzle, once the solver fills them in:

(declare-fun QueenPartner (Queen) Tom)
(declare-fun QueenActivity (Queen) Activities)
(declare-fun QueenKittens (Queen) Int)
(declare-fun TomPartner (Tom) Queen)

To be specific:

QueenPartner returns the Tom partner of the given Queen.
QueenActivity returns the given queen's favorite activity.
QueenKittens returns the number of kittens a given Queen has as an Int.
TomPartner returns the Queen partner of the given Tom.

Implicit Constraints

By their very nature, logic puzzles contain some usually-implied rules that we must follow when solving them if we don't want incoherent, nonsensical answers:

Each possible choice in each category is different from all the other choices. It should be apparent that, for instance, Batman and Dibii are different tomcats (uniqueness).
There are a finite number of choices for each category, and this number is the same for each category. E.g. each of the three queens can choose from one of three activities. There is no fourth "secret" activity that the logic puzzle knows about and we don't (finiteness).
As mentioned earlier, each queen has a mutually-exclusive partner, number of kittens, and activity with respect to other queens.
We can also deduce that a tom has the same number of kittens and activity as its queen partner.

A logic puzzle grid such as above visually makes it easy to follow these rules. Unfortunately, an SMT solver knows nothing about logic puzzles without our help, so we must explain those implicit constraints in our query. We use asserts to force an SMT solver to reject nonsensical-but-valid answers to a query of variables, where in the case of a logic puzzle, our variables are our uninterpreted functions.

Our enums we created via declare-datatype already encode these uniqueness/finiteness constraints mentioned above. We can also represent the number of kittens each cat pair has as a NumKittens enum, but for convenience that will become clear shortly, I chose to use an Int. While Ints have a uniqueness constraint (1 is different than 2), in SMT-LIB, Ints do not have a finiteness constraint. Thus without additional information, the solver free to set NumKittens for each cat pair to 1, 10, or even 1,234,567, among other fine Ints, if the solver so chooses.

The puzzle's description ~~implies~~ outright says that the number of kittens each cat pair must be between 1 and 3 inclusive. We can constrain the values for number of kittens the solver will try using an assert:

; Integer constraint
(assert (and 
    (>= (QueenKittens Ruby) 1) (<= (QueenKittens Ruby) 3)
    (>= (QueenKittens Spot) 1) (<= (QueenKittens Spot) 3)
    (>= (QueenKittens Starbuck) 1) (<= (QueenKittens Starbuck) 3)))

While the uniquess constraints of enums and Ints gets us far, it's not quite enough. As quoted above:

As is customary for this type of problem, it is implied that each queen has a different partner, favorite activity, and number of kittens.

Although the solver recognizes that each tom is a different cat, without additional information, nothing prevents the solver from giving an answer which assigns, for instance, two queens to the same tomcat partner.

We can further constrain the solver from trying to assign two queens the same partner, number of kittens, and activity by constraining the uninterpreted functions we defined earlier via more asserts. For instance, the statement (assert (not (= (QueenPartner Ruby) (QueenPartner Spot))) tells the SMT solver "However you decide to fill the function body, I need the function QueenPartner to not return the same value for Ruby and Spot". To properly constrain our query, you need one assert for each possible pair of values in each category, which can be combined into a single large conjuction 13 :

; "Only one dot in each row/col" consistency check.
(assert (and
    (not (= (QueenPartner Ruby) (QueenPartner Spot)))
    (not (= (QueenPartner Ruby) (QueenPartner Starbuck)))
    (not (= (QueenPartner Spot) (QueenPartner Starbuck)))
    (not (= (QueenKittens Ruby) (QueenKittens Spot)))
    (not (= (QueenKittens Ruby) (QueenKittens Starbuck)))
    (not (= (QueenKittens Spot) (QueenKittens Starbuck)))
    (not (= (QueenActivity Ruby) (QueenActivity Spot)))
    (not (= (QueenActivity Ruby) (QueenActivity Starbuck)))
    (not (= (QueenActivity Spot) (QueenActivity Starbuck)))))

The above check is morally equivalent to a human making sure a logic grid has only one ✓ per row and column for each combination of values in each category. Because of the uniqueness constraints for each enum and Int, the above is sufficient to make sure the solver knows that each queen has a mutually exclusive partner, number of kittens, and activity and that such a solution exists14 .

Lastly, each cat pair shares a favorite activity and the number kittens they have. So far, we've only written constraints for each queen in the cat pair. However, we don't need to rewrite the constraints for each tom! There is another consistency check we need, and a side-effect, we can represent each tom's favorite activity and number of kittens for free in terms of this constraint.

The TomPartner uninterpreted function returns the Queen who is the partner of the given Tom. Likewise, the QueenPartner function returns the Tom whose partner is the given Queen. Without extra constraints, the SMT solver doesn't know "obvious" facts like "'the partner of the partner' of a cat is the same cat you started with"15 . We can represent this fact with another assert:

; All other constraints for Tom are implied if the partner of the partner is the same.
(assert (and
    (= (QueenPartner (TomPartner Batman)) Batman)
    (= (QueenPartner (TomPartner Jake)) Jake)
    (= (QueenPartner (TomPartner Dibii)) Dibii)))

After this constraint, TomPartner unambiguously maps a tom back to queen. Since a cat pair has the same favorite activity and number of kittens, the solver now has enough information to solve for each tom's favorite activity and number of kittens in terms of queens.

Explicit Constraints

The implicit constraits are necessary but not sufficient to constrain the logic puzzle to a unique answer. If an SMT solver is presented with only the above lines, but there will be multiple ways to fill in our uninterpreted functions which satisfy that query. The solver will choose to present to you16 one interpretation for each function out of all valid ones, and chances are, it won't be the intended answer to the logic puzzle based on the clues.

If you incorporate the clues, however, the SMT solver should17

be limited to only one valid answer to your query. In this sense, the clues given above form the explicit, outright-stated constraints unique to a specific logic puzzle. Explicit constraints are handled identically to the implicit constraints in the previous section, by mapping a textual description of the clues described earlier to asserts:

Batman's partner likes to chase a ball. She was not Starbuck.

; 1. Batman chose the female who liked to chase a ball, but she was not Starbuck.
(assert (= (QueenActivity (TomPartner Batman)) Ball))
(assert (not (= (TomPartner Batman) Starbuck)))

Dibii's partner liked the lazer.

; 2. Dibii's companion liked to chase the laser light.
(assert (= (QueenActivity (TomPartner Dibii)) Lazer))

Ruby was a cat who liked to sleep.

; 3. Ruby loved to cuddle up to her male for a long afternoon nap in the sun.
(assert (= (QueenActivity Ruby) Sleep))

Starbuck has two more kittens than whoever Batman's companion is.

This clue is the reason I represented the number of kittens as an Int. While I would have to reinvent addition if I used a NumKittens enum, the SMT solver already knows the theory of Ints and can add them using +18 .

; 4. Starbuck had two more kittens than Batman's companion.
(assert (= (QueenKittens Starbuck)
           (+ (QueenKittens (TomPartner Batman)) 2)))

Getting An Answer

Once, we add check-sat, our query text file is finished, and we can feed it to z3 using the invocation described to check whether our query is satisfiable. You can download the completed query here and run it online (as of 2023-08-13) if you wish.

Many times, knowing SAT or UNSAT is "good enough". But for a logic puzzle, we actually want the variable values. get-model works, but this shows the definition of the uninterpreted functions you asked the solver to fill in. While seeing the function bodies are useful information, for solving a logic puzzle, it's probably better to use get-value to see individual outputs of each now-interpreted function for "interesting" inputs.

To compare and contrast, I use all of check-sat, get-model, and get-value:

(check-sat)
(get-model)

(echo "
Spot:")
(get-value ((QueenPartner Spot)
            (QueenKittens Spot)
            (QueenActivity Spot)))

(echo "
Ruby:")
(get-value ((QueenPartner Ruby)
            (QueenKittens Ruby)
            (QueenActivity Ruby)))

(echo "
Starbuck:")
(get-value ((QueenPartner Starbuck)
            (QueenKittens Starbuck)
            (QueenActivity Starbuck)))

Running the entire query through my local copy of z3 gives the following output:

sat
(
  (define-fun QueenKittens ((x!0 Queen)) Int
    (ite (= x!0 Spot) 1
    (ite (= x!0 Starbuck) 3
      2)))
  (define-fun QueenPartner ((x!0 Queen)) Tom
    (ite (= x!0 Spot) Batman
    (ite (= x!0 Starbuck) Dibii
      Jake)))
  (define-fun QueenActivity ((x!0 Queen)) Activities
    (ite (= x!0 Starbuck) Lazer
    (ite (= x!0 Ruby) Sleep
      Ball)))
  (define-fun TomPartner ((x!0 Tom)) Queen
    (ite (= x!0 Jake) Ruby
    (ite (= x!0 Dibii) Starbuck
      Spot)))
)


Spot:
(((QueenPartner Spot) Batman)
 ((QueenKittens Spot) 1)
 ((QueenActivity Spot) Ball))

Ruby:
(((QueenPartner Ruby) Jake)
 ((QueenKittens Ruby) 2)
 ((QueenActivity Ruby) Sleep))

Starbuck:
(((QueenPartner Starbuck) Dibii)
 ((QueenKittens Starbuck) 3)
 ((QueenActivity Starbuck) Lazer))

First off, the query is sat, which is a good start! The model returned by get-model isn't hard for me to follow either. I could fairly quickly figure out each answer to the logic puzzle using get-model alone, and I'm sure anyone else reading this post could too. But using get-value to evaluate the functions the solver filled in for us gives us the logic puzzle answers directly, ready to be written down! So let's save ourselves the trouble and populate the puzzle's answers thanks to get-value!

Was the solver correct? Well, as of this writing (2023-07-23), Aha! Puzzles lets you solve logic puzzles interactively online. I'll just let the below screenshot speak for itself:

The popup says "Congratulations, you win!", so indeed z3 was correct. Although the logic puzzle grid and answer table is obscured by the popup, there is just enough of the grid and answer table shown to verify that I filled in the puzzle with the answers returned by z3.

Conclusion/Next Steps

I still find logic puzzles fun to work through manually. To me, asking a machine to solve every logic puzzle for you defeats the satisfaction of working your brain to solve the puzzle yourself. So while I hope the above example provides some insight as to how to map word problems to an SMT query/model, I wouldn't suggest that you start solving every logic puzzle with an SMT solver.

That said, I found that trying to map a logic puzzle to an SMT solver query was also intellectually stimulating. It is a low-stakes problem that gave me the opportunity to exercise my skills at creating SMT queries, as opposed to my typical usage where I have a program generate queries and models for me. I was excited after I got my query working, and I wanted to document the result.

Speaking of generating queries and models, it's possible to take this logic puzzle-solving use case further by creating a Domain-Specific Language (DSL). Like how the previously-linked SymbiYosys converts Verilog to SMT-LIB queries, this DSL would convert a more convenient textual representation of a logic puzzle into SMT-LIB queries. It's a bit more up-front work than writing SMT-LIB queries manually, and probably not worth the time spent other than for learning. However, since this project is meant to be low-stakes and for fun, I may look into a DSL in the future for a follow-up post. It's about time I wrote a(nother) compiler anyway.

Thanks

I would like to thank my friends Screwtape and Alyssa Rosenzweig for their general feedback and a few last-minute corrections on the final draft of this post.

Footnotes

1 I will not be discussing how to write a SAT solver; for those interested I suggest this tutorial for building a SAT solver in Python. The tutorial is based on Donald Knuth's "SAT0W" solver.

Although I have not personally done so yet, I would probably also look at Knuth's "SAT10" solver, which is based on the Davis–Putnam–Logemann–Loveland (DPLL) algorithm.

2 To be honest, I'm going by what Wikipedia says here. There's no external reference:

Early attempts for solving SMT instances involved translating them to Boolean SAT instances (e.g., a 32-bit integer variable would be encoded by 32 single-bit variables with appropriate weights and word-level operations such as 'plus' would be replaced by lower-level logic operations on the bits) and passing this formula to a Boolean SAT solver.

3 Just like for SAT solvers, I will not be discussing how to write an SMT solver. While in the process of writing this post, I have been learning about the DPLL(T) framework myself. I've found the following set of slides useful:

Lecture 7 of Emina Torlak's CSE507. In particular, Emina's slides outline the DPLL(T) algorithm in terms of Conflict-Driven Clause Learning (CDCL), an extension of DPLL.
Lecture 2 of Wes Weimer's CS590.

4 In my own experience, yices is significantly faster at many problems involving formal verification of HDL. However, it is not universal. This is why the Symbiyosys front end for HDL verification will run the same query against multiple SMT solvers in parallel if you have them installed.

5 If you don't include parentheses to actually evaluate operators, weird things you probably didn't intend will happen. For instance, try comparing the result of the query (assert (= or true false true)) to (assert (= (or true false) true)).

6 More succinctly, the clues "constrain the solution space".

7 The logic that's closest to what I need, Quantifier-Free Finite Domain (QF_FD), has some additional restrictions which cause my logic puzzle query to return UNKNOWN. I'm not actually certain why it returns UNKNOWN, but I suspect I'm running afoul of the restrictions by using datatypes with uninterpreted functions, and not just equality (=) comparisons.

8 I belive `ALL` is z3's default logic anyway.

9 declare-datatypes is not required, and the logic puzzle can be solved without them. In fact, I have constructed a working query without datatypes for this logic puzzle- twice! I wanted to solve the puzzle with yices as well as z3 as an exercise; while yices does support enums and the like, they are not compatible with SMT-LIB.

As shown in the linked yices examples, declare-sort, declare-const, and declare-fun, plus some assert constraints can emulate declare-datatypes and finite integers reasonably. However, for a handwritten example, I wanted to focus on creating constraints appropriate to a logic puzzle rather than reinventing enums.

10 The integer argument to declare-datatypes is used for parametric polymorphism. It represents, informally, "the number of types to be filled in later".

11 What A, B, and C actually are in terms of "bits in memory somewhere" doesn't matter as long as the solver manipulates these values of type Foo according to the above rules.

12 To make the example more interesting, I tried to use asserts to get the solver to generate a function body which uses + (integer addition), but got bored and gave up. This post is getting long anyway.

13 Readers familiar with using z3 may notice that I can more-succinctly represent the exclusivity constraints using a forall quantifier. Indeed, this works, and was how I originally solved the example logic puzzle. Except for an extra pair datatype, the quantifier version of our query is very similar to the quantifier-free query constructed in this blog post; just compare the comments.

However, I decided not not to discuss quantifiers in this post for a few reasons:

The quantifiers are not required for enumerations with finite variants to create the constraints.
I am not exceptionally familiar with using quantifiers in SMT queries and when they are actually required. I haven't needed them for HDL verification, for instance.
Quantifiers complicate the SMT solver's job. While queries without quantifiers can always be determined to be SAT or UNSAT, some queries with quanitifers are undecidable. As of this writing (2023-07-02) I don't think I'm qualified to discuss undecidability other than in passing.
Not all SMT solvers support quantifiers (e.g. yices).

Therefore, while the quantifiers are likely harmless here, I'd rather them when they are actually required, not just as a means to make queries take fewer lines.

14 If two enum variants could be equal each other in value (i.e. not distinct), it would be impossible for our uninterpreted functions to return three distinct enum variants to three different values of input enum variants.

To show this, play with this commented query online:

(declare-sort Foo 0) ; declare-sort declares a new type, like `Int`, `Bool`.
                     ; It has fewer assumptions baked-in than `declare-datatypes`.

; Create some named values for our types.
; These are like our `enum` variants.
(declare-const foo_one Foo)
(declare-const foo_two Foo) 
(declare-const foo_three Foo)

(declare-sort Bar 0)
(declare-const bar_one Bar)
(declare-const bar_two Bar)
(declare-const bar_three Bar)

; Our uninterpreted function. Takes a `Foo`, returns a `Bar`.
(declare-fun my-fun (Foo) Bar)

; Ensure each constant has a unique value. This is implied 
; `declare-datatypes`.
;
; Change _any_ of the 6 asserts from `distinct` to `=`.
; The solver will return `unsat`.
(assert (distinct foo_one foo_two))
(assert (distinct foo_one foo_three))
(assert (distinct foo_two foo_three))

(assert (distinct bar_one bar_two))
(assert (distinct bar_one bar_three))
(assert (distinct bar_two bar_three))

; Prevent the solver from trying to create more values for our types
; from thin air. This is implied in `declare-datatypes`.
(assert (and
    (or
        (= (my-fun foo_one) bar_one)
        (= (my-fun foo_one) bar_two)
        (= (my-fun foo_one) bar_three))
    (or
        (= (my-fun foo_two) bar_one)
        (= (my-fun foo_two) bar_two)
        (= (my-fun foo_two) bar_three))
    (or
        (= (my-fun foo_three) bar_one)
        (= (my-fun foo_three) bar_two)
        (= (my-fun foo_three) bar_three))))

; Each input to my-fun should return a unique output.
; This is impossible unless foo_{one, two, three} have
; different values according to `=`.
(assert (distinct (my-fun foo_one) (my-fun foo_two)))
(assert (distinct (my-fun foo_one) (my-fun foo_three)))
(assert (distinct (my-fun foo_two) (my-fun foo_three)))

(check-sat)
(get-model)

15 While I praise the SMT solver for being open-minded, polyamory is not within the scope of this logic puzzle.

16 By default an SMT solver will give you one answer. It is possible to get all possible answers to an SMT query. Since a logic puzzle is intended to have a single answer, ensuring that the number of unique answers is 1 would be another good consistency check at the cost of execution time. Unfortunately, I don't remember how to do this.

17 The puzzle should have a unique answer if it was designed properly.

18 I chose to write the assert in terms of Int and + as an example. When numbers you can choose from in a category aren't sequential, and/or the clues are more complicated, I think it's useful to be able to model clues with other theories the SMT solver provides.

In this case, because we know that NumKittens is constrained from 1 to 3 inclusive, you could just as easily derive the constraint as:

(assert (= (QueenKittens Starbuck) 3))
(assert (= (QueenKittens (TomPartner Batman)) 1))

Last Updated: 2023-08-15

WDJ

Using `z3` To Solve Logic Puzzles

Prerequisites

What is an SMT Solver?

SAT Solvers

SMT And SMT Solvers

`z3` And SMT-LIB

An Example In SMT-LIB Format

SMT And Logic Puzzles

An Example Puzzle

Description

Clues

Mapping The Puzzle To An SMT Query

Enums

Uninterpreted Functions

Implicit Constraints

Explicit Constraints

Getting An Answer

Conclusion/Next Steps

Thanks

Footnotes

Recommend

科华生物上半年度营收增长54.66%，净利润下降54.50%

Ku-Go: The World War II Death Ray

数据中心：等级分类系统

Blinded With Science

物联网技术综合指南

Nature发文：LK-99不是超导体

You don't hate JIRA, you hate your manager

Comparing 2.8.6...3.0.0 · hexagonkt/hexagon · GitHub

Break Out of Tutorial Hell, Build up The Python Coding Habit on Our Platform 💪

Google Ads to sunset Enhanced CPC on Shopping campaigns

About Joyk

WDJ

Using z3 To Solve Logic Puzzles

Prerequisites

What is an SMT Solver?

SAT Solvers

SMT And SMT Solvers

z3 And SMT-LIB

An Example In SMT-LIB Format

SMT And Logic Puzzles

An Example Puzzle

Description

Clues

Mapping The Puzzle To An SMT Query

Enums

Uninterpreted Functions

Implicit Constraints

Explicit Constraints

Getting An Answer

Conclusion/Next Steps

Thanks

Footnotes

Recommend

About Joyk

Using `z3` To Solve Logic Puzzles

`z3` And SMT-LIB