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.
Table of Contents
Equal and not equal
Let’s begin with equality. We have a clause 
and we want to add clause 
which is equal to . This means that if is 
in some assignment then is as well. We get this with the following:
|
1 2 |
a -b 0 -a b 0 |
If is then first clause is satisfied. For the second to be satisfied must be as well.
However, if is zero then second clause is satisfied but the first one is not. In that case 
must be so must be 
.
For inequality (or binary negation) we have the following:
|
1 2 |
a b 0 -a -b 0 |
When is then we need to have set to in second clause so is . When is then must be in the first clause.
Conjunction
We have clauses and , and we want to have clause 
being conjunction of and :
|
1 2 3 4 |
-a -b c 0 -a b -c 0 a -b -c 0 a b -c 0 |
For 
we have last clause make being .
For 
third clause makes being .
For 
we have second clause doing the same.
Finally, for 
we have first clause which makes equal to .
Disjunction
Goes this way:
|
1 2 3 4 |
a b -c 0 -a b c 0 a -b c 0 -a -b c 0 |
For we have first clause making equal to . All other clauses cover other permutations.
XOR
For exclusive or we can use:
|
1 2 3 4 |
-a b c 0 a -b c 0 a b -c 0 -a -b -c 0 |
For third clause makes 
. For fourth clause does the same. Similarly, for 
and 
we have first clause which makes 
.
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 
. We add one clause for each bit with the following constraints:
|
1 2 3 |
a_0 0 -a_1 0 a_2 0 |
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.