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.

Table of Contents

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):

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;
}

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:

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;
}

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;

}