This is the third 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 are going to reduce ILP to SAT.

Introduction

Depending on the solver, typical ILP supports the following operations:

1. Adding two variables
2. Negating variable
3. Subtracting variables
4. Multiplying variable by constant
5. Dividing variable by constant
6. Adding equality constraint
7. Adding greater or equal constraint
8. Adding less or equal constraint
9. Adding goal function
10. Marking variable as integer

Some operations are obviously represented in SAT while others cannot be easily reduced.

If we assume that integers are of a specific width – which is not a crazy assumption as we use computers anyway and they do use fixed width numbers for increased performance – then we can implement operations 1-3 easily.

Operation 4 can be easily implemented as well assuming we work with integers only.

Operation 5 is tricky as the result may not be an integer so we can’t represent it properly.

Operation 6 is straightforward. So are operations 7 and 8 when we use slack variables.

Operation 9 is something we cannot implement in pure SAT. There is MAXSAT where we can optimize for a goal function, though.

Operation 10 is obvious.

Reduction

First we reduce the ILP problem to its canonical form. We replace all constraints with where . Same for – we change it to . We can stay with negative variables or replace them with subtraction and a slack variable.

Next, we reduce the canonical form to 0-1 ILP. We take every integer and replace it with bits.

Then, we remove the goal function. Ultimately we end up with a matrix of equalities of integer variables.

Now, we implement operations 1-4 and 6 using the approach from previous parts of this series.

Analysis

How slow is this going to be? For each integer we effectively introduce 32 clauses. For multiplication we need to add additional 32 partial sums which we then add together to get the result.

So, when we reduce the ILP model multiplying two integers with 27 bits width we end up with 2260029 clauses and 8409792 conjunctions. The model can be then solved in less than 2 minutes on my personal laptop. The DIMACS model has 210 MBs. For exponentiation it’s even bigger – 25375974 variables, 94454003 conjunctions, and 2.5 GBs.

Similarly, Nondeterministic Turing Machine for palindromes (the one we implemented in ILP) has 22123252 variables, 79175097 conjunctions, and 2.1 GBs.

That’s big. But it works and now we can use plenty of SAT solvers to calculate ILP models.

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

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

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:

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:

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 :

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

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:

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

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.