Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Encoding cardinality constraints for CryptoMiniSat from Python interface
from pycryptosat import Solver
class Encoder():
def __init__(self, solver, n = 1):
self._solver = solver
self._n = n
self._ite_cache = {}
self._true = None
def newvar(self):
n = self._n
self._n += 1
return n
def true(self):
if self._true is None:
self._true = self.newvar()
self._solver.add_clause([self._true])
#print("%d = TRUE" % self._true)
return self._true
def false(self):
return - self.true()
def ite_pos(self, condlit, thenlit, elselit):
if thenlit == elselit:
return thenlit
if condlit < 0:
condlit = - condlit
thenlit, elselit = elselit, thenlit
ret = self._ite_cache.get((condlit, thenlit, elselit))
if ret is None:
ret = self.newvar()
self._solver.add_clause([- ret, - condlit, thenlit]) # ret & condlit -> thenlit
self._solver.add_clause([- ret, condlit, elselit]) # ret & !condlit -> elselit
self._solver.add_clause([thenlit, elselit, - ret]) # ret -> thenlit | elselit
# self._solver.add_clause([ret, - condlit, - thenlit]) # condlit & thenlit -> ret
# self._solver.add_clause([ret, condlit, - elselit]) # !condlit & elselit -> ret
# self._solver.add_clause([- thenlit, - elselit, ret]) # thenlit & elselit -> ret
self._ite_cache[(condlit, thenlit, elselit)] = ret
#print("%d = IF %d THEN %d ELSE %d" % (ret, condlit, thenlit, elselit))
return ret
def add_atleast(self, lits, rhs):
#print("add_atleast: %s %d" % (lits, rhs))
conj_cache = {}
def conj(i):
if i >= len(lits):
return self.true()
elif i == len(lits) - 1:
return lits[i]
elif i in conj_cache:
return conj_cache[i]
else:
ret = self.newvar()
self._solver.add_clause([-ret, lits[i]]) # ret -> lits[i]
self._solver.add_clause([-ret, conj(i+1)]) # ret -> conj(i+1)
conj_cache[i] = ret
return ret
cache = {}
def f(i, rhs):
if rhs <= 0:
return self.true()
elif not (i < len(lits)):
return self.false()
elif (i,rhs) in cache:
return cache[(i,rhs)]
elif len(lits) - i == rhs:
ret = conj(i)
cache[(i,rhs)] = ret
return ret
else:
thenlit = f(i+1, rhs-1)
elselit = f(i+1, rhs)
ret = self.ite_pos(lits[i], thenlit, elselit)
cache[(i,rhs)] = ret
return ret
self._solver.add_clause([f(0, rhs)])
def add_atmost(self, lits, rhs):
#print("add_atmost: %s %d" % (lits, rhs))
return self.add_atleast([- l for l in lits], len(lits) - rhs)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment