How do I convert a series of mathematical constraints into a SAT or a SMT problem and get an answer?

Question

I have an arbitrary set of constraints. For example:

A, B, C and D are 8-bit integers.

A + B + C + D = 50
(A + B) = 25
(C + D) = 30
A < 10

I can convert this to a SAT problem that can be solved by picosat (I can't get minisat to compile on my Mac), or to a SMT problem that can be solved by CVC4. To do that I need to:

1. Map these equations into a Boolean circuit.
2. Apply Tseitin's transformation to the circuit and convert it into DIMACS format.

My questions:

1. What tools do I use to do the conversion to the circuit?
2. What are the file formats for circuits and which ones are commonly used?
3. What tools do I use to transform the circuit to DIMACS format?

Answer 1

In MiniZinc, you could just write a constraint programming model:

set of int: I8 = 0..255;

var I8: A;
var I8: B;
var I8: C;
var I8: D;

constraint A + B + C + D == 50;

constraint (A + B) = 25;

constraint (C + D) = 30;

constraint A < 10;

solve satisfy;

The example constraints cannot be satisfied, because of 25 + 30 > 50.

---

The Python interface of Z3 would allow the following:

from z3 import *
A, B, C, D = Ints('A B C D')
s = Solver()
s.add(A >= 0, A < 256)
s.add(B >= 0, B < 256)
s.add(C >= 0, C < 256)
s.add(A+B+C+D == 50)
s.add((A+B) == 25)
s.add((C+D) == 30)
s.add(A < 10)
print(s.check())
print(s.model())

Answer 2

So I have an answer. There's a program called Sugar: a SAT-based Constraint Solver which takes a series of constraints as S-expressions, converts the whole thing into a DIMACS file, runs the SAT solver, and then converts the results of the SAT solver back to the results of your constraitns.

Sugar was developed by Naoyuki Tamura to solve math puzzles like Sudoku puzzles. I found that it make it extremely simple to code complex constraints and run them.

For example, to find the square-root of 625, one could do this:

(int X 0 625)
(= (* X X) 625)

The first line says that X ranges from 0 to 625. The second line says that X*X is 625.

This may not be as simple and elegant as Z3, but it worked really well.

Answer 3

Conceptually

Build a circuit, then apply Tseitin's transform.

You'll need to express the addition and comparison operators as boolean logic. There are standard ways to build a circuit for twos-complement addition and for twos-complement comparison.

Then, use Tseitin's transform to convert this to a SAT instance.

In practice

Use a SAT front-end that will do this conversion for you. Z3 will take care of this for you. So will STP. (The conversion is sometimes known as "bit-blasting".)