SAT for developers 1: What is SAT?

Most guides on satisfiability (SAT) modeling are aimed at students or academics. In this post, I provide information that I hope will be useful to developers considering whether a SAT approach is right for their problem. 

What is SAT?

SAT means encoding your problem as a boolean formula which is handed off to a solver, that either returns an assignment to the variables that makes the formula true (a satisfying assignment), or the solver returns "unsat", meaning that there is no satisfying assignment. 

Boolean formula

What is a boolean formula? It is an expression consisting of boolean variables and AND, OR, and NOT statements. Example:

Formula 1: x1 AND x2 (satisfied when both x1 and x2 are true)

Formula 2: (NOT x1) OR x2 (satisfied except if x1 true and x2 is false) 

Formula 3: x1 => x2 (shorthand for the above!)

CNF

By far the most dominant format of the formula is the CNF (conjunctive normal form). It means "AND of ORs":

(x1 OR x2 OR x3) AND (x4 OR x5 OR x6) AND (x7 OR x8 OR (NOT x9)) 

Why is this a good format? Real world problems typically have a set of requirements for their solution. All requirements must be fulfilled for an acceptable solution. The CNF reflects this reality: all OR-clauses must be fulfilled for the formula to be satisfied. 

Representation

How is this represented in the computer? Here I have good news: the only data structure needed is a list of lists of integers. Each variable gets a signed integer. Minus means negation. The above formula:

[[1, 2, 3], [4, 5, 6], [7, 8, -9]]

Order between lists does not matter. Order between integers within a list does not matter. Adding new constraints just means appending to the CNF. Getting a new variable just means keeping track of the smallest unused integer. Most solvers accept the DIMACS CNF format. The above as a DIMACS CNF:

p cnf 9 3

1 2 3 0

4 5 6 0

7 8 -9 0

The first number after "p cnf" is the number of variables, the second is the number of clauses. Note that 0 is not allowed as a variable (because of the negation). 

The Work: Problem -> CNF

Now we see the work we have cut out for us: convert our problem to a list of list of integers so that we can hand it off to a solver, and then interpret the results. The last step if usually no problem in absence of model bugs. The big work lies in crafting a correct and efficient model. 

SAT: Some Constraints

In this post, I present four constraints that I have implemented for my satisfiability package SugarRush. It is based on PySAT [1]. 

Parity

	from sugarrush.solver import SugarRush
	solver = SugarRush()
	x = [solver.var() for _ in range(10)]
	t, cnf = solver.parity(x)
	solver.add(cnf)
	solver.add([t]) # if you want the sum of x to be odd
	# solver.add([-t]) # if you want the sum of x to be even

view raw parity.py hosted with ❤ by GitHub

This constraint is much much better to use than the method used in sat: disjunction operator. 

Naive / general way, with disjunction (for 10 elements):

Nof variables: 1096

Nof clauses: 3195

Special purpose encoding of parity constraint (for 10 elements):

Nof variables: 19

Nof clauses: 36

And of course it solves much faster.

Less / Leq

	from sugarrush.solver import SugarRush
	""" Constrain
	a < b or
	a <= b
	where a and b are N-bit binary numbers.
	The leftmost bit is the highest.
	"""
	solver = SugarRush()
	N = 8
	a = [solver.var() for _ in range(N)]
	b = [solver.var() for _ in range(N)]
	t, cnf = solver.less(a, b) # a < b
	# t, cnf = solver.leq(a, b) # a <= b
	solver.add(cnf)
	solver.add([t]) # t <=> a < b

view raw less.py hosted with ❤ by GitHub

A natural question is: why is the t returned separately from the rest of the constraint? The reason is that this way, one can easily encode such constraints as "a is either less than b, or less than c", or "a is less than either b or c, but not both". An example usage here is to constrain two intervals to be non-overlapping:

	from sugarrush.solver import SugarRush
	""" Given two intervals [a0, a1], [b0, b1],
	constrain that they have no overlap.
	"""
	solver = SugarRush()
	N = 8
	a0 = [solver.var() for _ in range(N)]
	a1 = [solver.var() for _ in range(N)]
	b0 = [solver.var() for _ in range(N)]
	b1 = [solver.var() for _ in range(N)]
	a0_less_a1, cnfa = solver.leq(a0, a1) # a0 <= a1
	b0_less_b1, cnfb = solver.leq(b0, b1) # b0 <= b1
	a1_less_b0, cnf0 = solver.less(a1, b0)
	b1_less_a1, cnf1 = solver.less(b1, a1)
	b1_less_a0, cnf2 = solver.less(b1, a0)
	a1_less_b1, cnf3 = solver.less(a1, b1)
	# add the bindings
	solver.add(cnf0 + cnf1 + cnf2 + cnf3 + cnfa + cnfb)
	# constrain the order of a0,a1 and b0,b1
	solver.add([a0_less_a1])
	solver.add([b0_less_b1])
	# the main constraint:
	# (a1 must not be inside [b0, b1]) AND (b1 must not be inside [a0, a1])
	solver.add([[b1_less_a1, a1_less_b0], [a1_less_b1, b1_less_a0]])

view raw non_overlapping.py hosted with ❤ by GitHub

Plus

	from sugarrush.solver import SugarRush
	"""Given three N-bit binary numbers a, b, z
	constrain so that
	a + b = z % 2**N
	(unsigned N-bit integer addition)
	"""
	solver = SugarRush()
	N = 8
	a = [solver.var() for _ in range(N)]
	b = [solver.var() for _ in range(N)]
	z = [solver.var() for _ in range(N)]
	cnf = solver.plus(a, b, z)
	# cnf = solver.plus(a, z, b) # to get b - a!
	solver.add(cnf)

view raw plus.py hosted with ❤ by GitHub

Element

	from sugarrush.solver import SugarRush
	"""Constrain
	z = v[a]
	where a is uintK,
	z is uintN,
	v is a vector of at most 2**K uintN
	"""
	def to_binary(N, n, a):
	n = n % 2**N
	b = "{1:0{0:d}b}".format(N, n)
	return [ap if bp == '1' else -ap for bp, ap in zip(b, a)]
	solver = SugarRush()
	N = 8
	K = 4
	a = [solver.var() for _ in range(K)]
	z = [solver.var() for _ in range(N)]
	v = [[solver.var() for _ in range(N)] for _ in range(2**K)]
	# v[i] = 2 + 3*i
	v0_assumptions = to_binary(N, 2, v[0])
	for v0, v1 in zip(v, v[1:]):
	solver.add(solver.plus(v0, 3, v1))
	solver.add(solver.element(v, a, z))
	a_int = 3
	a_assumptions = to_binary(K, a_int, a)
	solver.solve(assumptions= v0_assumptions + a_assumptions)
	z_solve = [(solver.solution_value(zp) > 0)*1 for zp in z]
	z_int = sum([2**i * zp for i, zp in enumerate(z_solve[::-1])])
	print("v[{0:d}] = {1:d}".format(a_int, z_int))

view raw element.py hosted with ❤ by GitHub

[1] Ignatiev, Alexey, Antonio Morgado, and Joao Marques-Silva. "PySAT: A Python toolkit for prototyping with SAT oracles." International Conference on Theory and Applications of Satisfiability Testing. Springer, Cham, 2018.