The New Turing Omnibus Chapter 34 Satisfiability (also featuring: Sentient)
We welcomed lots of new faces to the club and struggled to make space for the 20+ people who showed up. We distributed multi-coloured copies of the notes. After an incredibly efficient round of everyone's names, we were ready to begin.
We began by talking through the Big Picture. Chris explained that there are hard problems that we don't have efficient algorithms to solve. One way of solving these problems is by turning them into a boolean satisfiability problem (also known as SAT) and using established techniques such as the DPLL algorithm for solving that instead. Chris has been building a programming language that compiles down to SAT and makes use of existing SAT solvers.
This meeting centred around two main topics:
- The chapter, which is about the boolean satisfiability problem
- Sentient, which is the programming language Chris has been building
Before diving into the language itself, we thought it would be useful to understand what the satisfiability problem is. We wrote up the first example in the book and talked about it using the whiteboard.
Chris explained that a satisfiability problem is a boolean formula made up of some variables. Typically, these variables are ORed together and arranged into clauses that are ANDed together. This is called a "product of sums" or conjunctive normal form (also known as CNF).
The goal is to find a set of true / false assignments for these variables that make the formula true. If a set of values exists (even if you don't know the exact values), this problem is said to be satisfiable.
We talked through the assignment of x1, x2, x3, x4 = true, true, true, true
which does not satisfy the formula and x1, x2, x3, x4 = false, true, true, true
which does.
We discussed whether these satisfiability problems had to be in conjunctive normal form to be a SAT problem but any boolean expression can be used, it's just that CNF is the standard format of expressions used as inputs to SAT solvers.
Q: Can any boolean expression be turned into this form?
A: Yes. That's a good point. A product of sums is quite a strict form. If you want to use anything richer, you have to figure out how to turn it into this structure.
Every boolean expression can be converted into CNF using rules of logical equivalence such as De Morgan's laws.
Q: Can you convert any problem into SAT?
A: Probably not – the types of problem you can convert into SAT are decision problems. These are problems where you're looking for a yes / no answer. However, SAT is a little bit unique in that it does something constructive. It answers the question [of satisfiability] and it also tells you how it arrived at that answer.
This means that if you can express a seemingly difficult problem in terms of SAT, you can use SAT solvers to not only tell you whether it is possible to solve but also give you one possible answer.
To better understand the kinds of problems that benefit from translation into SAT, we looked at a graph colouring problem: colouring vertices with one of three colours such that no two vertices of the same colour were connected by an edge.
We attempted to brute force a solution for the first graph given in the book but could not find a way to colour the graph within the constraints provided.
However, given a slightly different graph with the same number of vertices, we did find a solution:
We then discussed the chapter's example of how such a problem could be translated into SAT by expressing each node as a boolean expression (e.g. (r1 || y1 || b1)) and then expressing the invariants that no connected vertices could be the same colour (e.g. (!r1 || !r2)).
James expanded a full boolean expression for a simple graph with three vertices on the whiteboard:
Armed with an understanding of SAT, the kinds of problems it can express and how we might utilise a solver, we dove into Chris' work on Sentient, a programming language to leverage this technique.
We began by immediately looking at an application of Sentient to solve the subset sum problem: Subset Sum
This browser-based implementation showed how Sentient could take a problem with several variables (both the input set of numbers and the desired total) and produce solutions as we changed both the input and the total.
We skimmed the source code to show the JavaScript stack-oriented language powering Sentient:
We briefly saw how the problem was expressed in terms of typed variables and invariants.
We then looked at a more recent (and much more complicated example) problem: an extension of the aforementioned 3-colouring graph problem where not only did we have the same colouring constraints but each vertex had to contain an integer such that the sum total of all vertices equalled a given number and each node with the same integer shared the same colour.
Chris challenged the club to implement a solution to this problem in any other programming language of choice as a testament to the power of using SAT to express such self-referential problems.
Q: While we've seen how you can express problems in SAT and get solutions as boolean assignments, how can you translate this back into your original problem domain?
To answer this question, we walked through Sentient's execution model, showing how it is structured in layers which translate both down and up between various representations. This is made possible by adding metadata to its output to keep track of how the various layers relate.
Chris explained the lowest-level output of Sentient: the DIMACS CNF format used as a standard input to SAT solvers:
We then attempted to solve various exercises set by Chris using Sentient's stack-oriented language.
Chris first explained how we express simple arithmetic addition:
And an alternate form using Sentient's invariant instruction:
We discussed how Sentient's integers require their width to be declared up front but how it can automatically resize integers based on arithmetic instructions such as addition and multiplication:
We ended the meeting by squeezing in solutions to the first two exercises and there was much rejoicing:
- What had drawn so many newcomers to the meeting? There seemed to be no single answer: a few people had come based on a recommendation from a friend, others were particularly interested in Satisfiability, we wondered whether Joel's more concerted efforts to market and organise the meeting following the last retrospective also contributed;
- There was great praise again for a mix of theoretical and practical content (much like the Game Trees meeting);
- We reiterated the huge difference Chris' efforts had made to the quality of the meeting;
- We wondered again if we should move away from our dedication to one topic per meeting with little to no continuity as there was some appetite for more Sentient adventures in another meeting.
Thanks to Dan and Geckoboard for hosting, Joel for organising the meeting and, of course, to Chris for the enormous effort he has both put into Sentient and into preparation for this meeting.
Following the meeting, Paul built an implementation of ISBN-10s and ISBN-13s in Sentient which can both convert and recover lost information from both formats of book identifiers.