From bfc58b8eb6f7977527cbcdd6de5268a8573ce79f Mon Sep 17 00:00:00 2001 From: Aaron Windsor Date: Sat, 11 Jan 2025 10:28:05 -0500 Subject: [PATCH] Make cardinality generators iterative so we don't get RecursionErrors --- TODO | 2 -- cnfc/cardinality.py | 14 ++++++-------- tests/test_cardinality.py | 10 ++++++++++ 3 files changed, 16 insertions(+), 10 deletions(-) diff --git a/TODO b/TODO index 20122af..76ce459 100644 --- a/TODO +++ b/TODO @@ -8,7 +8,5 @@ * 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 cardinality.py generators iterative instead of recursive to avoid RecursionLimit with large formulas * Make NumTrue auto-convert to NumFalse and vise-versa when appropriate * Add a Formula.WriteBlocker method to write a blocking solution extractor \ No newline at end of file diff --git a/cnfc/cardinality.py b/cnfc/cardinality.py index c16690b..9bae40d 100644 --- a/cnfc/cardinality.py +++ b/cnfc/cardinality.py @@ -4,25 +4,23 @@ # Generates clauses satisfiable iff at most one of the variables in vs is false. # Uses Heule's encoding, see TAOCP 7.2.2.2 exercise 12. def at_most_one_false(formula, vs): - if len(vs) <= 4: - yield from at_most_one_false_exhaustive(vs) - else: + while len(vs) > 4: head, tail = vs[:3], vs[3:] v = formula.AddVar() yield from at_most_one_false_exhaustive(head + [v]) - yield from at_most_one_false(formula, [~v] + tail) + vs = [~v] + tail + yield from at_most_one_false_exhaustive(vs) def at_most_one_false_exhaustive(vs): yield from combinations(vs, 2) def at_most_one_true(formula, vs): - if len(vs) <= 4: - yield from at_most_one_true_exhaustive(vs) - else: + while len(vs) > 4: head, tail = vs[:3], vs[3:] v = formula.AddVar() yield from at_most_one_true_exhaustive(head + [v]) - yield from at_most_one_true(formula, [~v] + tail) + vs = [~v] + tail + yield from at_most_one_true_exhaustive(vs) def at_most_one_true_exhaustive(vs): for x,y in combinations(vs, 2): diff --git a/tests/test_cardinality.py b/tests/test_cardinality.py index 0fbacb4..280013c 100644 --- a/tests/test_cardinality.py +++ b/tests/test_cardinality.py @@ -316,3 +316,13 @@ def test_eq_boundary(self): self.assertSat(f) # At most n true is a tautology, no way to create an unsat formula. + + # at_most_one_{true,false} used to be implemented recursively, which meant that + # you'd need to adjust the recursion limit with sys.setrecursionlimit() to make + # larger cardinality constraints work. This test used to generate a RecursionError. + def test_many_vars(self): + f = Formula() + import sys + limit = sys.getrecursionlimit() * 2 + varz = [f.AddVar() for i in range(2 * limit)] + f.Add(NumTrue(*varz) >= limit)