Skip to content

Commit

Permalink
allow NumTrue/NumFalse to be used in more complicated expressions
Browse files Browse the repository at this point in the history
  • Loading branch information
@aaw
aaw committed Jan 18, 2025
1 parent bfc58b8 commit bb29f79
Show file tree
Hide file tree
Showing 3 changed files with 269 additions and 102 deletions.
12 changes: 8 additions & 4 deletions TODO
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,14 @@
* Rename generate_var, generate_cnf to evaluate*
* Implement very simple clause caching/suppressing duplicate clauses
* Support integer division/subtraction by re-arranging parse tree into addition/multiplication
* Support cardinality constraints compared to one another:
NumTrue(x,y,z) >= NumFalse(w,v). And to Integer: NumTrue(x,y,z) > Integer(1)
* Generate a bash script for sat generation/solving/extracting
* Implement IsPrime predicate using Pratt certificates, drop into jane st. number cross 4
* Implement Formula.WriteCubedCnf(fd, vars)
* Make NumTrue auto-convert to NumFalse and vise-versa when appropriate
* Add a Formula.WriteBlocker method to write a blocking solution extractor
* Make NumTrue auto-convert to NumFalse and vise-versa when appropriate with fixed integers
* Add a Formula.WriteBlocker method to write a blocking solution extractor
* NumTrue/NumFalse are specialized for comparisons with int so that "NumTrue(*varz) >= Integer(1)"
sums up all the variables in varz that are true and compares it to the binary representation of 1,
but "NumTrue(*varz) >= 1" generates something simpler like an OR of varz. For larger int, we will
generate a selection network, but it's not clear if that's more efficient that just computing the
sum of the varz. Test and remove all the selection network code if it isn't dramatically more
efficient.
231 changes: 133 additions & 98 deletions cnfc/model.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,18 +89,6 @@ def generate_var(self, formula):
def generate_cnf(self, formula):
yield (self,)

class CardinalityConstraint(NumExpr):
def __init__(self, *exprs):
self.exprs = exprs
for expr in self.exprs:
assert issubclass(type(expr), BoolExpr), "{} needs boolean expressions, got {}".format(self.__class__.__name__, expr)

def __repr__(self):
return '{}({})'.format(self.__class__.__name__, ','.join(repr(e) for e in self.exprs))

class NumTrue(CardinalityConstraint): pass
class NumFalse(CardinalityConstraint): pass

class MultiBoolExpr(BoolExpr):
def __init__(self, *exprs):
self.exprs = exprs
Expand Down Expand Up @@ -209,92 +197,6 @@ def generate_cnf(self, formula):
yield (fv, sv)
yield (~fv, ~sv)

class NumEq(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
assert type(self.second) is int, "Cardinality comparisons require integers"
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
n = self.second
elif isinstance(self.first, NumFalse):
n = len(vars) - self.second
else:
raise ValueError("Only NumTrue and NumFalse are supported.")
yield from exactly_n_true(formula, vars, n)

class NumNeq(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
assert type(self.second) is int, "Cardinality comparisons require integers"
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
n = self.second
elif isinstance(self.first, NumFalse):
n = len(vars) - self.second
else:
raise ValueError("Only NumTrue and NumFalse are supported.")
yield from not_exactly_n_true(formula, vars, n)

class NumLt(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
assert type(self.second) is int, "Cardinality comparisons require integers"
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
yield from at_most_n_true(formula, vars, self.second-1)
elif isinstance(self.first, NumFalse):
yield from at_least_n_true(formula, vars, len(vars) - self.second + 1)
else:
raise ValueError("Only NumTrue and NumFalse are supported.")

class NumLe(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
assert type(self.second) is int, "Cardinality comparisons require integers"
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
yield from at_most_n_true(formula, vars, self.second)
elif isinstance(self.first, NumFalse):
yield from at_least_n_true(formula, vars, len(vars) - self.second)
else:
raise ValueError("Only NumTrue and NumFalse are supported.")

class NumGt(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
assert type(self.second) is int, "Cardinality comparisons require integers"
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
yield from at_least_n_true(formula, vars, self.second+1)
elif isinstance(self.first, NumFalse):
yield from at_most_n_true(formula, vars, len(vars) - self.second - 1)
else:
raise ValueError("Only NumTrue and NumFalse are supported.")

class NumGe(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
assert type(self.second) is int, "Cardinality comparisons require integers"
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
yield from at_least_n_true(formula, vars, self.second)
elif isinstance(self.first, NumFalse):
yield from at_most_n_true(formula, vars, len(vars) - self.second)
else:
raise ValueError("Only NumTrue and NumFalse are supported.")

class OrderedBinaryTupleBoolExpr(BoolExpr):
def __init__(self, first, second):
self.first, self.second = first, second
Expand Down Expand Up @@ -566,6 +468,139 @@ def evaluate(self, formula):
t2 = lpad(t2, len(t1) - len(t2))
return [Or(And(self.cond, t1[i]), And(~self.cond, t2[i])).generate_var(formula) for i in range(len(t1))]

class CardinalityConstraint(NumExpr):
def __init__(self, *exprs):
self.exprs = exprs

def __repr__(self):
return '{}({})'.format(self.__class__.__name__, ','.join(repr(e) for e in self.exprs))

class NumTrue(CardinalityConstraint, TupleExpr):
def evaluate(self, formula):
if len(self.exprs) == 0:
return Integer(0)
indicators = [If(v, Integer(1), Integer(0)) for v in self.exprs]
while len(indicators) > 1:
reduced = []
for a,b in zip(indicators[::2], indicators[1::2]):
reduced.append(a + b)
if len(indicators) % 2 == 1:
reduced.append(indicators[-1])
indicators = reduced
return indicators[0].evaluate(formula)

class NumFalse(CardinalityConstraint, TupleExpr):
def evaluate(self, formula):
if len(self.exprs) == 0:
return Integer(0)
indicators = [If(v, Integer(0), Integer(1)) for v in self.exprs]
while len(indicators) > 1:
reduced = []
for a,b in zip(indicators[::2], indicators[1::2]):
reduced.append(a + b)
if len(indicators) % 2 == 1:
reduced.append(indicators[-1])
indicators = reduced
return indicators[0].evaluate(formula)

class NumEq(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
if not type(self.second) is int:
yield from TupleEq(self.first, self.second).generate_cnf(formula)
return
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
n = self.second
elif isinstance(self.first, NumFalse):
n = len(vars) - self.second
else:
raise ValueError("Only NumTrue and NumFalse are supported.")
yield from exactly_n_true(formula, vars, n)

class NumNeq(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
if not type(self.second) is int:
yield from TupleNeq(self.first, self.second).generate_cnf(formula)
return
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
n = self.second
elif isinstance(self.first, NumFalse):
n = len(vars) - self.second
else:
raise ValueError("Only NumTrue and NumFalse are supported.")
yield from not_exactly_n_true(formula, vars, n)

class NumLt(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
if not type(self.second) is int:
yield from TupleLt(self.first, self.second).generate_cnf(formula)
return
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
yield from at_most_n_true(formula, vars, self.second-1)
elif isinstance(self.first, NumFalse):
yield from at_least_n_true(formula, vars, len(vars) - self.second + 1)
else:
raise ValueError("Only NumTrue and NumFalse are supported.")

class NumLe(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
if not type(self.second) is int:
yield from TupleLe(self.first, self.second).generate_cnf(formula)
return
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
yield from at_most_n_true(formula, vars, self.second)
elif isinstance(self.first, NumFalse):
yield from at_least_n_true(formula, vars, len(vars) - self.second)
else:
raise ValueError("Only NumTrue and NumFalse are supported.")

class NumGt(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
if not type(self.second) is int:
yield from TupleGt(self.first, self.second).generate_cnf(formula)
return
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
yield from at_least_n_true(formula, vars, self.second+1)
elif isinstance(self.first, NumFalse):
yield from at_most_n_true(formula, vars, len(vars) - self.second - 1)
else:
raise ValueError("Only NumTrue and NumFalse are supported.")

class NumGe(OrderedBinaryBoolExpr):
def generate_var(self, formula):
return generate_var_from_cnf(self, formula)

def generate_cnf(self, formula):
if not type(self.second) is int:
yield from TupleGe(self.first, self.second).generate_cnf(formula)
return
vars = [expr.generate_var(formula) for expr in self.first.exprs]
if isinstance(self.first, NumTrue):
yield from at_least_n_true(formula, vars, self.second)
elif isinstance(self.first, NumFalse):
yield from at_most_n_true(formula, vars, len(vars) - self.second)
else:
raise ValueError("Only NumTrue and NumFalse are supported.")

# Polymorphic If:
# - With two params, this is boolean implication.
# - With three params, this is a ternary operator that evaluates the condition and returns one of the last two args.
Expand Down
Loading

0 comments on commit bb29f79

Please sign in to comment.