The Subtle Power of Booleans

Programming with truth and statefulness.

I like formal specification because I don’t really understand it. That is kind of my personality, curiosity blended with absolute raw stubbornness.

In my quest to understand formal specification I’ve started to learn more about logic programming than I did before. I first encountered logic programming when Pierre de Lacaze came to a meetup I belonged to and gave a talk about Prolog. I was fascinated, but couldn’t find any resources to learn how to use Prolog and was endlessly frustrated when every tutorial I did find stopped at building a Sudoku solver. This did not seem relevant to anything I wanted to do and so I never looked closely at it.

Alloy and SAT solvers

But logic programming doesn’t begin and end with tools like Prolog. One formal specification tool I like using is Alloy , which is basically just a nicer interface on top of a SAT (for SATISFIABILITY) solver. SAT solvers are programs that look for solutions that satisfy all the facts much in the same way that Prolog does. There are many different ways of implementing SAT solvers, this post is only the tip of the iceberg in that regard!

You write models in Alloy using a markup language that defines the spec around relationships. Alloy has signatures , which you can think of as a little bit like objects. Signatures can inherit from each other and have parameters that are used to specify connections (or relationships) between signatures. For example:

sig Duck{
    member: one Flock
}sig Flock {
    group: set Duck
}

In this spec a Flock is defined as a set of Ducks and each Duck belongs to one Flock. To make this spec effective we’d probably want to add some constraints the specify the exact nature of the relationship between Flocks and Ducks like so:

fact{
    all d: Duck, f: d.member | d in f.group
    all f: Flock, d: f.group | d.member = f
    no f:Flock | lone f.group
}

Which clarifies that when a Duck thinks it is in a Flock, that Flock should also have the Duck as a member (and vice versa). Since sets can be empty, we also add a fact that tells Alloy that no Flocks should have one or less (lone) Ducks.

When you run this model, Alloy converts relational logic into boolean logic and runs a SAT solver, then takes the output of that solver and converts it back to relational in order to visualize it. What I particularly like about Alloy is you can use assertions and have it test whether specific states are even possible, which is useful for bug checking and verification. Or you can run the model without assertions and explore the various states that are possible given the definitions of the spec. I love that flexibility.

But how does Alloy take our spec and calculate possible states? Under the hood the true/false rules Alloy is producing are written out in Conjunctive Normal Form (CNF), or to be more specific the simplified version called DIMACS (named after the Center for Di screte Ma thematics and Theoretical C omputer S cience at Rutgers University) CNF which looks like this:

p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

The first line is a header called the problem statement (hence it begins with the letter p) that tells the SAT solver that this is CNF format, there are 5 variables that can be either true or false and that we have 3 clauses. The three lines that follow are those clauses. Each number in the clause is a variable, not a value. Positive numbers mean the statement or concept the variable represents is true and negative numbers mean the same concept is false. Each clause must be terminated with a zero so that especially long clauses can be broken up over multiple lines for easier reading.

In other words, the line 1 -5 4 0 reads ‘the first variable is true OR the fifth variable is false OR the fourth variable is true.’ The line -3 -4 0 reads ‘either the third variable OR the fourth variable is false.’

ANDs in DIMACS CNF are from line to line. If you wanted to say that variable 2 and variable 3 must be true. You would write that like so:

This is pretty easy to understand but not so easy to apply to practical programming problems. Formal specification tools use SAT solvers (and their cousin the SMT solver) to identify possible states that violate the spec’s defined constraints. By doing so they can check your model for bugs that might not be obvious. But how do you convert your code into a series of variables that are either true or false?

Example 1: Sudoku

Turns out the reason why Sudoku is the Hello World of logic programming is that it is actually a pretty good demonstration of how complex problems can be converted to true/false clauses.

If you are not familiar with Sudoku, it’s a puzzle game in which you must fill in boxes with numbers so that the values 1–9 appear once and only once per row, per column and per section. The game board is seeded with some starting values, the more starting values the easier the puzzle.

If we think of each box as a variable holding a number between 1–9, the 9x9 grid would give us 81 variables — except we cannot express 1–9 as true/false, so actually we need a variable for each potential state that can be assigned to each box, or 729 variables. The resulting set of instructions is well over 10,000 clauses.

This is one box, it has nine possible values:

The numbers make sense if you think about dealing out cards to each box in a row of sudoku until each one has nine cards. The first box gets card 1 and by the time you come back to deal the second card you’re at card 10 , then you deal out cards to the eight other boxes in the row and the third card box one receives is number 19 in the deck. Therefore variable 1 represents the first box with a value of 1, variable 10 represents the first box with a value of 2 and so on…

As the numbers are variables, what true/false statements they represent only matter in that they are unique and predictable enough to map them back to the box they belong to and value between 1–9 they represent.

Another way we could represent this is joining the row position and column position and the value into one number. In that case the same row would become 111 112 113 114 115 116 117 118 119 0

In any case, both of these clauses say that the first box in the first row can be 1 OR 2 OR 3 OR… any number between 1–9

But one box cannot be filled in with two numbers at the same time. After our clause defining the box and its potential values we need a series of shorter clauses that establish if one value is true, all other values must be false. This is expressed in head to heads. If Box 1 has a value of 1 it cannot have a value of 2… either the value of 1 is false OR the value of 2 is false or both are false. Either the value of 2 is false OR the value of three is false… and so on for all possible values:

-1 -10 0
-1 -19 0
-1 -28 0
-1 -37 0
-1 -46 0
-1 -55 0
-1 -64 0
-1 -73 0
-10 -19 0
-10 -28 0

But we also can’t have any duplicate numbers across rows and columns. We need to repeat the same process for every potential value of 1 in the first row of the puzzle. That looks like this:

1 2 3 4 5 6 7 8 9 0
-1 -2 0
-1 -3 0
-1 -4 0

Going back to the dealing cards to each box metaphor, cards 1–9 are all the first card boxes 1–9 in the first row of the puzzle get. So they all represent the number one. The first clause says anyone of these boxes can have the value of one, the shorter clauses that follow say only one box can have that value.

Same thing for columns. If the first box in the first row gets card 1, the first box in the second row gets card 82 so the first column looks like this:

1 82 163 244 325 406 487 568 649 0
-1 -82 0
-1 -163 0
-1 -244 0
-1 -325 0 
-1 -406 0
-1 -487 0

And what about the 3x3 sections? We can do the exact same thing for all of the 9 boxes:

But Sudoku isn’t Sudoku if we don’t have seed values narrowing the field of possible solutions. These are easy to represent since they are just single positive values like:

Which tells the SAT solver that in the first row of our puzzle the sixth box has a value of 1 and the fourth box has a value of eight.

Once we have the full CNF written out, the SAT solver can consider all the possible legal combinations and produce a solution.

Example 2: The Zebra Problem

You’ve probably encountered the Zebra Problem before:

There are five houses.
The Englishman lives in the red house.
The Spaniard owns the dog.
Coffee is drunk in the green house.
The Ukrainian drinks tea.
The green house is immediately to the right of the ivory house.
The Old Gold smoker owns snails.
Kools are smoked in the yellow house.
Milk is drunk in the middle house.
The Norwegian lives in the first house.
The man who smokes Chesterfields lives in the house next to the man with the fox.
Kools are smoked in the house next to the house where the horse is kept.
The Lucky Strike smoker drinks orange juice.
The Japanese smokes Parliaments.
The Norwegian lives next to the blue house.
Now, who drinks water? Who owns the zebra?

Like Sudoku we have a series of potential states for each of the five houses:

• The nationality of the owner
• The color of the house
• What the owner drinks
• What the owner smokes
• The owner’s pet

Most of these statements can be broken up into clauses pretty easily. For example, in CNF we would not say the Englishman lives in the red house we would say either the owner of the house is NOT the Englishman OR the house is red (which effectively means the same thing).

Then there are other statements that are a bit different. What we know from the statement “The green house is immediately to the right of the ivory house” is that the last house is not ivory and the first house is not green. “Milk is drunk in the middle house” has a similar translation. The middle house is house 3, the owner of house 3 drinks milk

This is all well and good, but how do we encode this information in a series of true/false variables? Unlike the Sudoku where we needed to map 9 possible states across 81 boxes, with the Zebra Puzzle we have only five boxes for each piece of information.

In DIMACS one can include comments by starting the line with c . That means we can include a mapping of these concepts to their variables so we don’t lose track of each possible state we’ve assigned.

It looks something like this:

c 1 is "1:Englishman"
c 2 is "1:red"
c 3 is "2:Englishman"
c 4 is "2:red"
c 5 is "3:Englishman"
c 6 is "3:red"
c 7 is "4:Englishman"
c 8 is "4:red"
c 9 is "5:Englishman"
c 10 is "5:red"
c 11 is "1:Spaniard"
c 12 is "1:dog"
c 13 is "2:Spaniard"
c 14 is "2:dog"

And so on (for the full DIMACS encoding see Lars Hellstrom’s paper on this [warning: PDF will download automatically])

There are a couple of states that we know to be impossible from the puzzle. For example, we know that the first house is not green. Given our mapping this would be state 21 so after our problem statement we list the states that we know to be either true or false:

p cnf 125 547c 21 "1:green" 
-21 0c 45 "5:ivory"
-45 0c 66 "3:milk"
66 0c 67 "1:Norwegian"
67 0c 104 "2:Norwegian"
-104 0c 106 "3:Norwegian"
-106 0

I’ve included comments to make the snippet easier to make sense of but with 547 clauses you probably wouldn’t bother ;)

From this point the set up is very much like Sudoku. Any house can be the red house, but only one house can be the red house in the same way that any box in a row can have the value of 1 but only one box in the row can have that value.

2 6 4 8 10 0
-2 -4 0
-2 -6 0
-2 -8 0
-2 -10 0
-4 -6 0
-4 -8 0
-4 -10 0
-6 -8 0
-6 -10 0
-8 -10 0

Hopefully this is starting to look familiar! We have a little extra information then we do with Sudoku. We don’t know which house is the red house, but we do know that if house 2 has an Englishman in then house 3 cannot be any other color than red. We need to represent that in DIMACS too:

c Either there's no Englishman in house 1 or house 1 is red
-1 2 0
c Either there's no Englishman in house 2 or house 2 is red
-3 4 0
c Either there's no Englishman in house 3 or house 3 is red
-5 6 0
c Either there's no Englishman in house 4 or house 4 is red
-7 8 0
c Either there's not Englishman in house 5 or house 5 is red
-9 10 0

Once we have represented all possible states, we will be able to feed the DIMACS CNF file into a SAT solver and have it solve the puzzle for us.

Flock of Ducks

Let’s go back to our simple model with our Ducks and Flocks.

Fun fact: you can have Alloy export your model to a CNF file for you by going to Options>Solver>Output CNF to file . If we don’t tell Alloy how many ducks and how many flocks there are it will default to 4 each, which will give us a long CNF file with too many variables to really make sense of. Instead we’ll tweak the spec to make it super simple:

sig Duck{}sig Flock {
    group: one Duck
}pred model {}run model for exactly 1 Flock, 1 Duck

First thing we’ve done is remove the circular relationship between Flocks and Ducks. Then we removed all the rules and specified that the model should have only one Duck and one Flock.

There are a couple of different potential states from these pieces. If we were going to write out the CNF ourselves we might think of it this way:

c 1 there is a Duck
c 2 there is a Flock
c 3 Duck is in the Flock

When we look at the CNF output Alloy gives us we see this:

p cnf 4 3
-2 1 -3 0
2 0
3 0

If Alloy maps things to variables the same way we do then -2 1 -3 0 reads No Flock OR Duck OR No Duck in Flock. Then the lines below that are Flock is true and the Duck is in a Flock. When we run this there is only one possible solution. One Flock with one Duck in it.

But constructing CNF problems can get complicated the larger and more robust the model becomes. What happens when we take the same simple model and change the specification so that we have TWO flocks? It doubles our CNF:

p cnf 8 8
2 -5 0 
-2 1 -4 0
4 -5 0
3 -7 0
-3 1 -6 0
6 -7 0
5 0
7 0

Although we haven’t changed the relationship between Ducks and Flocks, we have added a few new states and our existing states are not being encoded the same exact way. On top of that, not all of these states are easy to reason about. What we’d find out if we ran this in Alloy is that while we told the model that a Flock can only have one Duck, we did not say that one Duck cannot be in two different Flocks at the same time ;)

Since the variables themselves represent states, not numerical values, different tools will produce different CNFs depending on how they calculate the universe of possible states. Alloy, for example, converts things to Kodkod formulas before exporting them to CNF. Kodkod builds a matrix of possible values based on the relationship of signatures to one another, but even with simple specs this can get pretty complicated. After two weeks of reading source code, playing around with breakpoints in Eclipse and reading published papers I wasn’t able to translate the CNF output with 100% confidence I was representing Alloy/Kodkod internal processes correctly. On the bright side, the papers put out by the MIT community on this are some of the more readable CS papers I’ve encountered. If you’re interested in getting deeper into the internals I would recommend these:

• Automating First-Order Relational Logic (Alloy’s internals before they integrated Kodkod)
• A Constraint Solver for Software Engineering: Finding Models and Cores of Large Relational Specifications (Emina Torlak’s PhD dissertation in which she describes how Kodkod works)
• A structure-preserving clause form translation (A paper describing how to condense CNF by representing subformulas with a single variable)

Leveraging Boolean Logic in Real Programming

Part of the reason why tools like Alloy exist is to help facilitate using SAT solvers for system design. When turning a program or architecture into a specification it is useful to think about things in terms of state change, rather than steps in an algorithm. When we solve Sudoku or the zebra puzzle, we’re assigning various possible states to variables and then defining constraints that filter which states are possible under certain conditions (The Englishman lives in a red house, therefore a house can only be in a red state if the Englishman lives there). I use these steps to convert programs written in an imperative programming style to something that can be reasoned about with boolean logic:

• Make it look like a state machine. Define what changes state in your program (data, instances, objects, etc) and when/how it changes
• Figure out what states should be impossible and why. This is different from a state being simply undesirable. Remember there are no maybes in booleans. Early on in my experiments with formal specification I tried to model problems with load balancers , and I struggled because I was looking to represent states that I knew to be possible as model failures.
• Write the spec to demonstrate why the impossible states are impossible.
• Run the model checker to prove it.

In my experience, there’s a lot of value just in the thought experiment. When I’m writing specs I often find myself confronting questions about the expected behavior of systems that I do not know the answer to. Trying to figure out the answer to them never fails to trigger interesting conversations with my engineering teams.