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 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.