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.