For today's menu, I banged my head repeatedly on trying to use a CNF SAT solver to optimize logic problems. And succeeded!

Recipe difficulty

Statistics: 🔥🔥🔥🔥🔥 - no statistics required, but lots of optimization and logic knowledge required to even get started. Your brain will melt.
Technical: 🔥 - literally no code ability required.
Time required: 🕜🕜🕜 - it looks easy, but takes quite some time to even get the hang of it...

What it is

A SAT solver (shorthand for SATisfiability) is a NP-hard problem solver that tries to satisfy a set of boolean constraints.

The solver itself is written by the pros (and there's no point in re-inventing the wheel). Translating the problem into boolean logic is what's hard!

Basically we need to translate any set of constraints into expressions called CNFs, or conjunctive normal form.

This is an expression of the following form: (A or B) and (C or D) and ...

Why is it useful?

From optimizing shipments, to wedding seats, to solving Sudoku, to basically any constrained problem in the world - SAT solvers are the best, provided you can get the logic constraints set to work.

In this post we will look into a very simple problem, with just three constraints.

Let's assume we are having a birthday party and want to invite a few friends. Since we know how a SAT solver works, we must not have many. Let's say three friends: Anna, Brian and Carlos. However:

Anna loves Carlos. If we invite Anna we need to invite Carlos
Brian likes Carlos. If we invite Brian, we need to invite Carlos
Brian hates Anna. If we invite Brian, we can't invite Anna

Clearly there is only one solution to this problem: we invite Anna and Carlos, and we leave Brian home. Or is there?

Translating this into CNF

The first expression, can be expressed as Anna => Carlos (Anna implies Carlos). The truth table for this is:

Anna	Carlos	Anna => Carlos
1	1	1
1	0	0
0	1	1
0	0	1

Remember we need to translate the expression into an A or B CNF.

There's procedures to do so, but those are best left to my undergraduate years. For now, let's just intuitively look at the truth table. We know the OR disjunction is only false (0) when both A and B are false (0).

Clearly, in this case, the expression \[ Anna \rightarrow Carlos \] is equivalent with \[ \neg Anna \wedge Carlos \]

Anna	Carlos	Not Anna	(Not Anna) or Carlos
1	1	0	1
1	0	0	0
0	1	1	1
0	0	1	1

The same can be said for the second condition: indeed, \[ Brian \rightarrow Carlos = \neg Brian \wedge Carlos \]

Finally, for the third condition, we have \[ Brian \rightarrow \neg Anna \]

Brian	Not Anna	Brian => (not Anna)
1	1	1
1	0	0
0	1	1
0	0	1

Which is trivially the same as 'not Brian or not Anna'.

Putting this all in a cnf, we get:

# Anna = 1, Brian = 2, Carlos = 3

names = ['','Anna', 'Brian','Carlos','not Carlos','not Brian','not Anna']
cnf = [[-1,3], # not Anna or Carlos, and
       [-2,3], # not Brian or Carlos, and
       [-2,-1]] # not Brian or not Anna, and

Solving is literally two lines of code using pycosat

import pycosat
for solution in pycosat.itersolve(cnf):
    print(solution,'->', [names[i] for i in solution])

[-1, -2, 3] -> ['not Anna', 'not Brian', 'Carlos']
[-1, -2, -3] -> ['not Anna', 'not Brian', 'not Carlos']
[-1, 2, 3] -> ['not Anna', 'Brian', 'Carlos']
[1, -2, 3] -> ['Anna', 'not Brian', 'Carlos']

We get four solutions:

either we only invite Carlos
or we don't invite anyone
or we invite Carlos and Brian
or we invite Anna and Carlos

Clearly, one of these solution is trivial (the 'don't invite anyone') solution. However, adding this constraint to the cnf array is quite easy: we only need Anna, or Brian, or Carlos to be present, hence:

cnf.append([1,2,3])
for solution in pycosat.itersolve(cnf):
    print(solution,'->', [names[i] for i in solution])

[-1, -2, 3] -> ['not Anna', 'not Brian', 'Carlos']
[-1, 2, 3] -> ['not Anna', 'Brian', 'Carlos']
[1, -2, 3] -> ['Anna', 'not Brian', 'Carlos']

If this all seems quite trivial, remember our initial guess for the solution. As humans, we always start from the assumption that the computer has all the relevant knowledge to take an informed decision.

In this case, however, if we don't tell the solver specifically that we want to invite at least one person, it will just ignore this (implicit, and obvious to us) constraint.

Something to keep in mind when developing larger and more complex models!