This is the second part of the SAT series. For your convenience you can find other parts in the table of contents in Part 1 — Boolean logic

Today we’re going to implement some basic arithmetic in SAT.

# Addition

We assume numbers are represented using U2 scheme. All we need to do is to implement a full-adder. We can use the following code (it comes from my custom SAT solver for MilpManager wrapper):

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 |
protected override IVariable InternalSumVariables(IVariable first, IVariable second, Domain domain) { var variable = CreateAnonymous(domain).Typed(); int previousCarryIndex = ++VariablesCount; Unset(previousCarryIndex); for (int i = 0; i < Settings.BitsCount; ++i) { int a = first.Typed().SourceVariables[i]; int b = second.Typed().SourceVariables[i]; int halfCarryIndex = ++VariablesCount; And(a, b, halfCarryIndex); int halfSumIndex = ++VariablesCount; Xor(a, b, halfSumIndex); int fullSumIndex = variable.Typed().SourceVariables[i]; Xor(halfSumIndex, previousCarryIndex, fullSumIndex); int secondCarryIndex = ++VariablesCount; And(halfSumIndex, previousCarryIndex, secondCarryIndex); int fullCarryIndex = ++VariablesCount; Or(halfCarryIndex, secondCarryIndex, fullCarryIndex); previousCarryIndex = fullCarryIndex; } return variable; } |

Let’s unwrap this magic one by one.

First, in line 3 we create a variable for holding the result. We assume it creates enough clauses for integer.

Next, we clear previous carry index (the input to the full adder).

In lines 8-29 we implement a loop which adds bits one by one. We create a new carry in line 13 and then calculate it by using conjunction.

Next, in line 17 we calculate the half-add by xoring bits.

Next, we need to propagate carry properly. In lines 23-26 we do the math.

# Negation

Negation is very simple. First, we negate all bits, and then we add one (using the addition scheme from previous section).

# Subtraction

Super simple, just add negated number.

# Multiplication

We’re going to cheat a little. Since we represent numbers with fixed number of bits, we can ignore the overflow and just do the long multiplication, like this:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 |
protected override IVariable InternalMultiplyVariableByConstant(IVariable variable, IVariable constant, Domain domain) { var variableTyped = variable.Typed(); var constantTyped = constant.Typed(); List<IVariable> partialSums = new List<IVariable>(); for (int i = 0; i < Settings.BitsCount; ++i) { var partialSum = variable.MilpManager.CreateAnonymous(Domain.AnyInteger).Typed(); for (int j = 0; j < i; ++j) { constraints.Add(string.Format("-{0} 0", partialSum.SourceVariables[j])); } for (int j = 0; i + j < Settings.BitsCount; ++j) { And(constantTyped.SourceVariables[i], variableTyped.SourceVariables[j], partialSum.SourceVariables[i + j]); } partialSums.Add(partialSum); } var total = variable.MilpManager.Operation<Addition>(partialSums.ToArray()); return total; } |