SAT Part 1 — Boolean logic

This is the first part of the SAT series. For your convenience you can find other parts using the links below:
SAT Part 1 — Boolean logic
SAT Part 2 — Arithmetic
Part 3 — Reducing ILP to SAT

Today we are going to implement some Boolean logic in SAT.

Equal and not equal

Let’s begin with equality. We have a clause a and we want to add clause b which is equal to a. This means that if a is 1 in some assignment then b is 1 as well. We get this with the following:

If a is 1 then first clause is satisfied. For the second to be satisfied b must be 1 as well.
However, if a is zero then second clause is satisfied but the first one is not. In that case -b must be 1 so b must be 0.

For inequality (or binary negation) we have the following:

When a is 1 then we need to have -b set to 1 in second clause so b is 0. When a is 0 then b must be 1 in the first clause.


We have clauses a and b, and we want to have clause c being conjunction of a and b:

For a = b = 0 we have last clause make c being 0.
For a = 0, b = 1 third clause makes c being 0.
For a = 1, b = 0 we have second clause doing the same.
Finally, for a = b = 1 we have first clause which makes c equal to 1.


Goes this way:

For a = b = 0 we have first clause making c equal to 0. All other clauses cover other permutations.


For exclusive or we can use:

For a = b = 0 third clause makes c=0. For a = b = 1 fourth clause does the same. Similarly, for a = 1 and b = 0 we have first clause which makes c = 1.

Introducing numbers to the model

Let’s now say that we would like to introduce some constant integer to the model. What we need to do is represent it in U2 system and set flags accordingly.

Let’s take 5 = 101_2. We add one clause for each bit with the following constraints:

You can see that this will correctly assign values to clauses and from now on we can use these clauses as bits of the number.

In the next part we will implement some arithmetic.