From dd20a8c21da480debe4633b043d51f765940bdba Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Fri, 9 Jun 2023 00:55:41 -0700 Subject: [PATCH 1/8] More # optional --- src/sage/sat/solvers/sat_lp.py | 1 + 1 file changed, 1 insertion(+) diff --git a/src/sage/sat/solvers/sat_lp.py b/src/sage/sat/solvers/sat_lp.py index d96ed62b125..dc1ff30d4b7 100644 --- a/src/sage/sat/solvers/sat_lp.py +++ b/src/sage/sat/solvers/sat_lp.py @@ -1,3 +1,4 @@ +# sage.doctest: optional - sage.numerical.mip r""" Solve SAT problems Integer Linear Programming From c9717a3cc1a726384a87368cd23f447b179f0988 Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Sat, 10 Jun 2023 17:49:17 -0700 Subject: [PATCH 2/8] Modularization fixes for imports --- src/sage/sat/converters/__init__.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/sage/sat/converters/__init__.py b/src/sage/sat/converters/__init__.py index 70e0cdfdfaa..bb7b60bbb9c 100644 --- a/src/sage/sat/converters/__init__.py +++ b/src/sage/sat/converters/__init__.py @@ -1,2 +1,5 @@ +from sage.misc.lazy_import import lazy_import + from .anf2cnf import ANF2CNFConverter -from sage.rings.polynomial.pbori.cnf import CNFEncoder as PolyBoRiCNFEncoder + +lazy_import('sage.rings.polynomial.pbori.cnf', 'CNFEncoder', as_='PolyBoRiCNFEncoder') From cc1307b9a7ae98c60fee9faf59a773ca2d0828b2 Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Sat, 10 Jun 2023 17:49:30 -0700 Subject: [PATCH 3/8] More # optional --- src/sage/sat/boolean_polynomials.py | 77 +++++++++++++++-------------- src/sage/sat/converters/polybori.py | 1 + src/sage/sat/solvers/satsolver.pyx | 12 ++--- 3 files changed, 47 insertions(+), 43 deletions(-) diff --git a/src/sage/sat/boolean_polynomials.py b/src/sage/sat/boolean_polynomials.py index 80b1a13d89c..2c5075d6251 100644 --- a/src/sage/sat/boolean_polynomials.py +++ b/src/sage/sat/boolean_polynomials.py @@ -71,8 +71,8 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): We construct a very small-scale AES system of equations:: - sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True) - sage: while True: # workaround (see :trac:`31891`) + sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True) # optional - sage.modules + sage: while True: # workaround (see :trac:`31891`) # optional - sage.modules ....: try: ....: F, s = sr.polynomial_system() ....: break @@ -81,66 +81,69 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): and pass it to a SAT solver:: - sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat - sage: s = solve_sat(F) # optional - pycryptosat - sage: F.subs(s[0]) # optional - pycryptosat + sage: from sage.sat.boolean_polynomials import solve as solve_sat + sage: s = solve_sat(F) # optional - pycryptosat sage.modules + sage: F.subs(s[0]) # optional - pycryptosat sage.modules Polynomial Sequence with 36 Polynomials in 0 Variables This time we pass a few options through to the converter and the solver:: - sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat - sage: F.subs(s[0]) # optional - pycryptosat + sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat sage.modules + sage: F.subs(s[0]) # optional - pycryptosat sage.modules Polynomial Sequence with 36 Polynomials in 0 Variables - We construct a very simple system with three solutions and ask for a specific number of solutions:: + We construct a very simple system with three solutions + and ask for a specific number of solutions:: - sage: B. = BooleanPolynomialRing() # optional - pycryptosat - sage: f = a*b # optional - pycryptosat - sage: l = solve_sat([f],n=1) # optional - pycryptosat - sage: len(l) == 1, f.subs(l[0]) # optional - pycryptosat + sage: B. = BooleanPolynomialRing() # optional - pycryptosat sage.modules + sage: f = a*b # optional - pycryptosat sage.modules + sage: l = solve_sat([f],n=1) # optional - pycryptosat sage.modules + sage: len(l) == 1, f.subs(l[0]) # optional - pycryptosat sage.modules (True, 0) - sage: l = solve_sat([a*b],n=2) # optional - pycryptosat - sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat + sage: l = solve_sat([a*b],n=2) # optional - pycryptosat sage.modules + sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat sage.modules (True, 0, 0) - sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=3)) # optional - pycryptosat + sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=3)) # optional - pycryptosat sage.modules [(0, 0), (0, 1), (1, 0)] - sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=4)) # optional - pycryptosat + sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=4)) # optional - pycryptosat sage.modules [(0, 0), (0, 1), (1, 0)] - sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=infinity)) # optional - pycryptosat + sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=infinity)) # optional - pycryptosat sage.modules [(0, 0), (0, 1), (1, 0)] In the next example we see how the ``target_variables`` parameter works:: - sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat - sage: R. = BooleanPolynomialRing() # optional - pycryptosat - sage: F = [a+b,a+c+d] # optional - pycryptosat + sage: from sage.sat.boolean_polynomials import solve as solve_sat + sage: R. = BooleanPolynomialRing() # optional - pycryptosat sage.modules + sage: F = [a + b, a + c + d] # optional - pycryptosat sage.modules First the normal use case:: - sage: sorted((D[a], D[b], D[c], D[d]) for D in solve_sat(F,n=infinity)) # optional - pycryptosat + sage: sorted((D[a], D[b], D[c], D[d]) # optional - pycryptosat sage.modules + ....: for D in solve_sat(F, n=infinity)) [(0, 0, 0, 0), (0, 0, 1, 1), (1, 1, 0, 1), (1, 1, 1, 0)] Now we are only interested in the solutions of the variables a and b:: - sage: solve_sat(F,n=infinity,target_variables=[a,b]) # optional - pycryptosat + sage: solve_sat(F,n=infinity,target_variables=[a,b]) # optional - pycryptosat sage.modules [{b: 0, a: 0}, {b: 1, a: 1}] Here, we generate and solve the cubic equations of the AES SBox (see :trac:`26676`):: - sage: from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence # optional - pycryptosat, long time - sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat, long time - sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, allow_zero_inversions = True) # optional - pycryptosat, long time - sage: sb = sr.sbox() # optional - pycryptosat, long time - sage: eqs = sb.polynomials(degree = 3) # optional - pycryptosat, long time - sage: eqs = PolynomialSequence(eqs) # optional - pycryptosat, long time - sage: variables = map(str, eqs.variables()) # optional - pycryptosat, long time - sage: variables = ",".join(variables) # optional - pycryptosat, long time - sage: R = BooleanPolynomialRing(16, variables) # optional - pycryptosat, long time - sage: eqs = [R(eq) for eq in eqs] # optional - pycryptosat, long time - sage: sls_aes = solve_sat(eqs, n = infinity) # optional - pycryptosat, long time - sage: len(sls_aes) # optional - pycryptosat, long time + sage: from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence + sage: from sage.sat.boolean_polynomials import solve as solve_sat + sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, # long time, optional - pycryptosat sage.modules + ....: allow_zero_inversions=True) + sage: sb = sr.sbox() # long time, optional - pycryptosat sage.modules + sage: eqs = sb.polynomials(degree = 3) # long time, optional - pycryptosat sage.modules + sage: eqs = PolynomialSequence(eqs) # long time, optional - pycryptosat sage.modules + sage: variables = map(str, eqs.variables()) # long time, optional - pycryptosat sage.modules + sage: variables = ",".join(variables) # long time, optional - pycryptosat sage.modules + sage: R = BooleanPolynomialRing(16, variables) # long time, optional - pycryptosat sage.modules + sage: eqs = [R(eq) for eq in eqs] # long time, optional - pycryptosat sage.modules + sage: sls_aes = solve_sat(eqs, n = infinity) # long time, optional - pycryptosat sage.modules + sage: len(sls_aes) # long time, optional - pycryptosat sage.modules 256 TESTS: @@ -148,7 +151,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): Test that :trac:`26676` is fixed:: sage: varl = ['k{0}'.format(p) for p in range(29)] - sage: B = BooleanPolynomialRing(names = varl) + sage: B = BooleanPolynomialRing(names=varl) sage: B.inject_variables(verbose=False) sage: keqs = [ ....: k0 + k6 + 1, @@ -162,7 +165,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): ....: k9 + k28, ....: k11 + k20] sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: solve_sat(keqs, n=1, solver=SAT('cryptominisat')) # optional - pycryptosat + sage: solve_sat(keqs, n=1, solver=SAT('cryptominisat')) # optional - pycryptosat [{k28: 0, k26: 1, k24: 0, @@ -187,7 +190,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): k2: 0, k1: 0, k0: 0}] - sage: solve_sat(keqs, n=1, solver=SAT('picosat')) # optional - pycosat + sage: solve_sat(keqs, n=1, solver=SAT('picosat')) # optional - pycosat [{k28: 0, k26: 1, k24: 0, diff --git a/src/sage/sat/converters/polybori.py b/src/sage/sat/converters/polybori.py index ca39def12c1..cbf46d4faa2 100644 --- a/src/sage/sat/converters/polybori.py +++ b/src/sage/sat/converters/polybori.py @@ -1,3 +1,4 @@ +# sage.doctest: optional - sage.rings.polynomial.pbori """ An ANF to CNF Converter using a Dense/Sparse Strategy diff --git a/src/sage/sat/solvers/satsolver.pyx b/src/sage/sat/solvers/satsolver.pyx index 1c4ac400cb6..0ed7041c608 100644 --- a/src/sage/sat/solvers/satsolver.pyx +++ b/src/sage/sat/solvers/satsolver.pyx @@ -139,9 +139,9 @@ cdef class SatSolver: sage: from io import StringIO sage: file_object = StringIO("c A sample .cnf file with xor clauses.\np cnf 3 3\n1 2 0\n3 0\nx1 2 3 0") - sage: from sage.sat.solvers.sat_lp import SatLP - sage: solver = SatLP() - sage: solver.read(file_object) + sage: from sage.sat.solvers.sat_lp import SatLP # optional - sage.numerical.mip + sage: solver = SatLP() # optional - sage.numerical.mip + sage: solver.read(file_object) # optional - sage.numerical.mip Traceback (most recent call last): ... NotImplementedError: the solver "an ILP-based SAT Solver" does not support xor clauses @@ -339,7 +339,7 @@ def SAT(solver=None, *args, **kwds): EXAMPLES:: - sage: SAT(solver="LP") + sage: SAT(solver="LP") # optional - sage.numerical.mip an ILP-based SAT Solver TESTS:: @@ -351,12 +351,12 @@ def SAT(solver=None, *args, **kwds): Forcing CryptoMiniSat:: - sage: SAT(solver="cryptominisat") # optional - pycryptosat + sage: SAT(solver="cryptominisat") # optional - pycryptosat CryptoMiniSat solver: 0 variables, 0 clauses. Forcing PicoSat:: - sage: SAT(solver="picosat") # optional - pycosat + sage: SAT(solver="picosat") # optional - pycosat PicoSAT solver: 0 variables, 0 clauses. Forcing Glucose:: From a37b456669e71fbaf06e357fae373c87c576bdc1 Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Sun, 11 Jun 2023 14:37:23 -0700 Subject: [PATCH 4/8] More # optional --- src/sage/sat/boolean_polynomials.py | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/src/sage/sat/boolean_polynomials.py b/src/sage/sat/boolean_polynomials.py index 2c5075d6251..6d84171b95d 100644 --- a/src/sage/sat/boolean_polynomials.py +++ b/src/sage/sat/boolean_polynomials.py @@ -1,3 +1,4 @@ +# sage.doctest: optional - sage.rings.polynomial.pbori """ SAT Functions for Boolean Polynomials @@ -71,8 +72,8 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): We construct a very small-scale AES system of equations:: - sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True) # optional - sage.modules - sage: while True: # workaround (see :trac:`31891`) # optional - sage.modules + sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # optional - sage.modules sage.rings.finite_rings + sage: while True: # workaround (see :trac:`31891`) # optional - sage.modules sage.rings.finite_rings ....: try: ....: F, s = sr.polynomial_system() ....: break @@ -82,14 +83,14 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): and pass it to a SAT solver:: sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: s = solve_sat(F) # optional - pycryptosat sage.modules - sage: F.subs(s[0]) # optional - pycryptosat sage.modules + sage: s = solve_sat(F) # optional - pycryptosat sage.modules sage.rings.finite_rings + sage: F.subs(s[0]) # optional - pycryptosat sage.modules sage.rings.finite_rings Polynomial Sequence with 36 Polynomials in 0 Variables This time we pass a few options through to the converter and the solver:: - sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat sage.modules - sage: F.subs(s[0]) # optional - pycryptosat sage.modules + sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat sage.modules sage.rings.finite_rings + sage: F.subs(s[0]) # optional - pycryptosat sage.modules sage.rings.finite_rings Polynomial Sequence with 36 Polynomials in 0 Variables We construct a very simple system with three solutions @@ -126,7 +127,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): Now we are only interested in the solutions of the variables a and b:: - sage: solve_sat(F,n=infinity,target_variables=[a,b]) # optional - pycryptosat sage.modules + sage: solve_sat(F, n=infinity, target_variables=[a,b]) # optional - pycryptosat sage.modules [{b: 0, a: 0}, {b: 1, a: 1}] Here, we generate and solve the cubic equations of the AES SBox (see :trac:`26676`):: @@ -136,7 +137,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, # long time, optional - pycryptosat sage.modules ....: allow_zero_inversions=True) sage: sb = sr.sbox() # long time, optional - pycryptosat sage.modules - sage: eqs = sb.polynomials(degree = 3) # long time, optional - pycryptosat sage.modules + sage: eqs = sb.polynomials(degree=3) # long time, optional - pycryptosat sage.modules sage: eqs = PolynomialSequence(eqs) # long time, optional - pycryptosat sage.modules sage: variables = map(str, eqs.variables()) # long time, optional - pycryptosat sage.modules sage: variables = ",".join(variables) # long time, optional - pycryptosat sage.modules @@ -343,11 +344,11 @@ def learn(F, converter=None, solver=None, max_learnt_length=3, interreduction=Fa We construct a simple system and solve it:: - sage: set_random_seed(2300) # optional - pycryptosat - sage: sr = mq.SR(1,2,2,4,gf2=True,polybori=True) # optional - pycryptosat - sage: F,s = sr.polynomial_system() # optional - pycryptosat - sage: H = learn_sat(F) # optional - pycryptosat - sage: H[-1] # optional - pycryptosat + sage: set_random_seed(2300) + sage: sr = mq.SR(1, 2, 2, 4, gf2=True, polybori=True) # optional - pycryptosat sage.modules sage.rings.finite_rings + sage: F,s = sr.polynomial_system() # optional - pycryptosat sage.modules sage.rings.finite_rings + sage: H = learn_sat(F) # optional - pycryptosat sage.modules sage.rings.finite_rings + sage: H[-1] # optional - pycryptosat sage.modules sage.rings.finite_rings k033 + 1 """ try: From a12c38c19c82b032d752279e8b5e1076bd58fd41 Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Sun, 11 Jun 2023 23:47:37 -0700 Subject: [PATCH 5/8] More # optional --- src/sage/sat/solvers/dimacs.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sage/sat/solvers/dimacs.py b/src/sage/sat/solvers/dimacs.py index cfe3c7cd4ed..51cffd27402 100644 --- a/src/sage/sat/solvers/dimacs.py +++ b/src/sage/sat/solvers/dimacs.py @@ -490,14 +490,14 @@ def __call__(self, assumptions=None): TESTS:: sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True) - sage: while True: # workaround (see :trac:`31891`) + sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # optional - sage.rings.finite_rings sage.rings.polynomial.pbori + sage: while True: # workaround (see :trac:`31891`) # optional - sage.rings.finite_rings sage.rings.polynomial.pbori ....: try: ....: F, s = sr.polynomial_system() ....: break ....: except ZeroDivisionError: ....: pass - sage: solve_sat(F, solver=sage.sat.solvers.RSat) # optional - RSat + sage: solve_sat(F, solver=sage.sat.solvers.RSat) # optional - RSat # optional - sage.rings.finite_rings sage.rings.polynomial.pbori """ if assumptions is not None: From e43e09ad70c8d960f6686fc8095e72578a1d631a Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Sun, 6 Aug 2023 20:45:14 -0700 Subject: [PATCH 6/8] src/sage/sat: Update file-level doctest tag --- src/sage/sat/boolean_polynomials.py | 2 +- src/sage/sat/converters/polybori.py | 2 +- src/sage/sat/solvers/sat_lp.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sage/sat/boolean_polynomials.py b/src/sage/sat/boolean_polynomials.py index 6d84171b95d..c47cae945d6 100644 --- a/src/sage/sat/boolean_polynomials.py +++ b/src/sage/sat/boolean_polynomials.py @@ -1,4 +1,4 @@ -# sage.doctest: optional - sage.rings.polynomial.pbori +# sage.doctest: needs sage.rings.polynomial.pbori """ SAT Functions for Boolean Polynomials diff --git a/src/sage/sat/converters/polybori.py b/src/sage/sat/converters/polybori.py index cbf46d4faa2..49da6f1819c 100644 --- a/src/sage/sat/converters/polybori.py +++ b/src/sage/sat/converters/polybori.py @@ -1,4 +1,4 @@ -# sage.doctest: optional - sage.rings.polynomial.pbori +# sage.doctest: needs sage.rings.polynomial.pbori """ An ANF to CNF Converter using a Dense/Sparse Strategy diff --git a/src/sage/sat/solvers/sat_lp.py b/src/sage/sat/solvers/sat_lp.py index dc1ff30d4b7..9b65b1d241d 100644 --- a/src/sage/sat/solvers/sat_lp.py +++ b/src/sage/sat/solvers/sat_lp.py @@ -1,4 +1,4 @@ -# sage.doctest: optional - sage.numerical.mip +# sage.doctest: needs sage.numerical.mip r""" Solve SAT problems Integer Linear Programming From 417429f000f0c237b4216c86635b2933f5927b59 Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Mon, 7 Aug 2023 22:44:22 -0700 Subject: [PATCH 7/8] src/sage/sat: sage -fixdoctests --only-tags --- src/sage/sat/boolean_polynomials.py | 68 ++++++++++++++------------- src/sage/sat/solvers/cryptominisat.py | 33 +++++++------ src/sage/sat/solvers/dimacs.py | 6 +-- src/sage/sat/solvers/picosat.py | 24 +++++----- src/sage/sat/solvers/satsolver.pyx | 8 ++-- 5 files changed, 73 insertions(+), 66 deletions(-) diff --git a/src/sage/sat/boolean_polynomials.py b/src/sage/sat/boolean_polynomials.py index c47cae945d6..dc5fdb69ff0 100644 --- a/src/sage/sat/boolean_polynomials.py +++ b/src/sage/sat/boolean_polynomials.py @@ -72,8 +72,8 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): We construct a very small-scale AES system of equations:: - sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # optional - sage.modules sage.rings.finite_rings - sage: while True: # workaround (see :trac:`31891`) # optional - sage.modules sage.rings.finite_rings + sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # needs sage.modules sage.rings.finite_rings + sage: while True: # workaround (see :trac:`31891`) # needs sage.modules sage.rings.finite_rings ....: try: ....: F, s = sr.polynomial_system() ....: break @@ -83,68 +83,70 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): and pass it to a SAT solver:: sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: s = solve_sat(F) # optional - pycryptosat sage.modules sage.rings.finite_rings - sage: F.subs(s[0]) # optional - pycryptosat sage.modules sage.rings.finite_rings + sage: s = solve_sat(F) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings + sage: F.subs(s[0]) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings Polynomial Sequence with 36 Polynomials in 0 Variables This time we pass a few options through to the converter and the solver:: - sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat sage.modules sage.rings.finite_rings - sage: F.subs(s[0]) # optional - pycryptosat sage.modules sage.rings.finite_rings + sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat, needs sage.modules sage.rings.finite_rings + sage: F.subs(s[0]) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings Polynomial Sequence with 36 Polynomials in 0 Variables We construct a very simple system with three solutions and ask for a specific number of solutions:: - sage: B. = BooleanPolynomialRing() # optional - pycryptosat sage.modules - sage: f = a*b # optional - pycryptosat sage.modules - sage: l = solve_sat([f],n=1) # optional - pycryptosat sage.modules - sage: len(l) == 1, f.subs(l[0]) # optional - pycryptosat sage.modules + sage: # optional - pycryptosat, needs sage.modules + sage: B. = BooleanPolynomialRing() + sage: f = a*b + sage: l = solve_sat([f],n=1) + sage: len(l) == 1, f.subs(l[0]) (True, 0) - sage: l = solve_sat([a*b],n=2) # optional - pycryptosat sage.modules - sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat sage.modules + sage: l = solve_sat([a*b],n=2) # optional - pycryptosat # needs sage.modules + sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat # needs sage.modules (True, 0, 0) - sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=3)) # optional - pycryptosat sage.modules + sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=3)) # optional - pycryptosat, needs sage.modules [(0, 0), (0, 1), (1, 0)] - sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=4)) # optional - pycryptosat sage.modules + sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=4)) # optional - pycryptosat, needs sage.modules [(0, 0), (0, 1), (1, 0)] - sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=infinity)) # optional - pycryptosat sage.modules + sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=infinity)) # optional - pycryptosat, needs sage.modules [(0, 0), (0, 1), (1, 0)] In the next example we see how the ``target_variables`` parameter works:: sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: R. = BooleanPolynomialRing() # optional - pycryptosat sage.modules - sage: F = [a + b, a + c + d] # optional - pycryptosat sage.modules + sage: R. = BooleanPolynomialRing() # optional - pycryptosat # needs sage.modules + sage: F = [a + b, a + c + d] # optional - pycryptosat # needs sage.modules First the normal use case:: - sage: sorted((D[a], D[b], D[c], D[d]) # optional - pycryptosat sage.modules + sage: sorted((D[a], D[b], D[c], D[d]) # optional - pycryptosat # needs sage.modules ....: for D in solve_sat(F, n=infinity)) [(0, 0, 0, 0), (0, 0, 1, 1), (1, 1, 0, 1), (1, 1, 1, 0)] Now we are only interested in the solutions of the variables a and b:: - sage: solve_sat(F, n=infinity, target_variables=[a,b]) # optional - pycryptosat sage.modules + sage: solve_sat(F, n=infinity, target_variables=[a,b]) # optional - pycryptosat, needs sage.modules [{b: 0, a: 0}, {b: 1, a: 1}] Here, we generate and solve the cubic equations of the AES SBox (see :trac:`26676`):: + sage: # long time, optional - pycryptosat, needs sage.modules sage: from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, # long time, optional - pycryptosat sage.modules + sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, ....: allow_zero_inversions=True) - sage: sb = sr.sbox() # long time, optional - pycryptosat sage.modules - sage: eqs = sb.polynomials(degree=3) # long time, optional - pycryptosat sage.modules - sage: eqs = PolynomialSequence(eqs) # long time, optional - pycryptosat sage.modules - sage: variables = map(str, eqs.variables()) # long time, optional - pycryptosat sage.modules - sage: variables = ",".join(variables) # long time, optional - pycryptosat sage.modules - sage: R = BooleanPolynomialRing(16, variables) # long time, optional - pycryptosat sage.modules - sage: eqs = [R(eq) for eq in eqs] # long time, optional - pycryptosat sage.modules - sage: sls_aes = solve_sat(eqs, n = infinity) # long time, optional - pycryptosat sage.modules - sage: len(sls_aes) # long time, optional - pycryptosat sage.modules + sage: sb = sr.sbox() + sage: eqs = sb.polynomials(degree=3) + sage: eqs = PolynomialSequence(eqs) + sage: variables = map(str, eqs.variables()) + sage: variables = ",".join(variables) + sage: R = BooleanPolynomialRing(16, variables) + sage: eqs = [R(eq) for eq in eqs] + sage: sls_aes = solve_sat(eqs, n = infinity) + sage: len(sls_aes) 256 TESTS: @@ -345,10 +347,10 @@ def learn(F, converter=None, solver=None, max_learnt_length=3, interreduction=Fa We construct a simple system and solve it:: sage: set_random_seed(2300) - sage: sr = mq.SR(1, 2, 2, 4, gf2=True, polybori=True) # optional - pycryptosat sage.modules sage.rings.finite_rings - sage: F,s = sr.polynomial_system() # optional - pycryptosat sage.modules sage.rings.finite_rings - sage: H = learn_sat(F) # optional - pycryptosat sage.modules sage.rings.finite_rings - sage: H[-1] # optional - pycryptosat sage.modules sage.rings.finite_rings + sage: sr = mq.SR(1, 2, 2, 4, gf2=True, polybori=True) # optional - pycryptosat, needs sage.modules sage.rings.finite_rings + sage: F,s = sr.polynomial_system() # optional - pycryptosat # needs sage.modules sage.rings.finite_rings + sage: H = learn_sat(F) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings + sage: H[-1] # optional - pycryptosat # needs sage.modules sage.rings.finite_rings k033 + 1 """ try: diff --git a/src/sage/sat/solvers/cryptominisat.py b/src/sage/sat/solvers/cryptominisat.py index d2a8ae9e5a6..82f1ffd9086 100644 --- a/src/sage/sat/solvers/cryptominisat.py +++ b/src/sage/sat/solvers/cryptominisat.py @@ -182,12 +182,13 @@ def __call__(self, assumptions=None): EXAMPLES:: + sage: # optional - pycryptosat sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - pycryptosat - sage: solver.add_clause((1,2)) # optional - pycryptosat - sage: solver.add_clause((-1,2)) # optional - pycryptosat - sage: solver.add_clause((-1,-2)) # optional - pycryptosat - sage: solver() # optional - pycryptosat + sage: solver = CryptoMiniSat() + sage: solver.add_clause((1,2)) + sage: solver.add_clause((-1,2)) + sage: solver.add_clause((-1,-2)) + sage: solver() (None, False, True) sage: solver.add_clause((1,-2)) # optional - pycryptosat @@ -231,23 +232,25 @@ def clauses(self, filename=None): EXAMPLES:: + sage: # optional - pycryptosat sage: from sage.sat.solvers import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - pycryptosat - sage: solver.add_clause((1,2,3,4,5,6,7,8,-9)) # optional - pycryptosat - sage: solver.add_xor_clause((1,2,3,4,5,6,7,8,9), rhs=True) # optional - pycryptosat - sage: solver.clauses() # optional - pycryptosat + sage: solver = CryptoMiniSat() + sage: solver.add_clause((1,2,3,4,5,6,7,8,-9)) + sage: solver.add_xor_clause((1,2,3,4,5,6,7,8,9), rhs=True) + sage: solver.clauses() [((1, 2, 3, 4, 5, 6, 7, 8, -9), False, None), ((1, 2, 3, 4, 5, 6, 7, 8, 9), True, True)] DIMACS format output:: + sage: # optional - pycryptosat sage: from sage.sat.solvers import CryptoMiniSat - sage: solver = CryptoMiniSat() # optional - pycryptosat - sage: solver.add_clause((1, 2, 4)) # optional - pycryptosat - sage: solver.add_clause((1, 2, -4)) # optional - pycryptosat - sage: fn = tmp_filename() # optional - pycryptosat - sage: solver.clauses(fn) # optional - pycryptosat - sage: print(open(fn).read()) # optional - pycryptosat + sage: solver = CryptoMiniSat() + sage: solver.add_clause((1, 2, 4)) + sage: solver.add_clause((1, 2, -4)) + sage: fn = tmp_filename() + sage: solver.clauses(fn) + sage: print(open(fn).read()) p cnf 4 2 1 2 4 0 1 2 -4 0 diff --git a/src/sage/sat/solvers/dimacs.py b/src/sage/sat/solvers/dimacs.py index 51cffd27402..51e81a925a1 100644 --- a/src/sage/sat/solvers/dimacs.py +++ b/src/sage/sat/solvers/dimacs.py @@ -490,14 +490,14 @@ def __call__(self, assumptions=None): TESTS:: sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # optional - sage.rings.finite_rings sage.rings.polynomial.pbori - sage: while True: # workaround (see :trac:`31891`) # optional - sage.rings.finite_rings sage.rings.polynomial.pbori + sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # needs sage.rings.finite_rings sage.rings.polynomial.pbori + sage: while True: # workaround (see :trac:`31891`) # needs sage.rings.finite_rings sage.rings.polynomial.pbori ....: try: ....: F, s = sr.polynomial_system() ....: break ....: except ZeroDivisionError: ....: pass - sage: solve_sat(F, solver=sage.sat.solvers.RSat) # optional - RSat # optional - sage.rings.finite_rings sage.rings.polynomial.pbori + sage: solve_sat(F, solver=sage.sat.solvers.RSat) # optional - rsat, needs sage.rings.finite_rings sage.rings.polynomial.pbori """ if assumptions is not None: diff --git a/src/sage/sat/solvers/picosat.py b/src/sage/sat/solvers/picosat.py index a1a80e71794..a88f69da883 100644 --- a/src/sage/sat/solvers/picosat.py +++ b/src/sage/sat/solvers/picosat.py @@ -147,12 +147,13 @@ def __call__(self, assumptions=None): EXAMPLES:: + sage: # optional - pycosat sage: from sage.sat.solvers.picosat import PicoSAT - sage: solver = PicoSAT() # optional - pycosat - sage: solver.add_clause((1,2)) # optional - pycosat - sage: solver.add_clause((-1,2)) # optional - pycosat - sage: solver.add_clause((-1,-2)) # optional - pycosat - sage: solver() # optional - pycosat + sage: solver = PicoSAT() + sage: solver.add_clause((1,2)) + sage: solver.add_clause((-1,2)) + sage: solver.add_clause((-1,-2)) + sage: solver() (None, False, True) sage: solver.add_clause((1,-2)) # optional - pycosat @@ -207,13 +208,14 @@ def clauses(self, filename=None): DIMACS format output:: + sage: # optional - pycosat sage: from sage.sat.solvers.picosat import PicoSAT - sage: solver = PicoSAT() # optional - pycosat - sage: solver.add_clause((1, 2, 4)) # optional - pycosat - sage: solver.add_clause((1, 2, -4)) # optional - pycosat - sage: fn = tmp_filename() # optional - pycosat - sage: solver.clauses(fn) # optional - pycosat - sage: print(open(fn).read()) # optional - pycosat + sage: solver = PicoSAT() + sage: solver.add_clause((1, 2, 4)) + sage: solver.add_clause((1, 2, -4)) + sage: fn = tmp_filename() + sage: solver.clauses(fn) + sage: print(open(fn).read()) p cnf 4 2 1 2 4 0 1 2 -4 0 diff --git a/src/sage/sat/solvers/satsolver.pyx b/src/sage/sat/solvers/satsolver.pyx index 0ed7041c608..83735c86989 100644 --- a/src/sage/sat/solvers/satsolver.pyx +++ b/src/sage/sat/solvers/satsolver.pyx @@ -139,9 +139,9 @@ cdef class SatSolver: sage: from io import StringIO sage: file_object = StringIO("c A sample .cnf file with xor clauses.\np cnf 3 3\n1 2 0\n3 0\nx1 2 3 0") - sage: from sage.sat.solvers.sat_lp import SatLP # optional - sage.numerical.mip - sage: solver = SatLP() # optional - sage.numerical.mip - sage: solver.read(file_object) # optional - sage.numerical.mip + sage: from sage.sat.solvers.sat_lp import SatLP # needs sage.numerical.mip + sage: solver = SatLP() # needs sage.numerical.mip + sage: solver.read(file_object) # needs sage.numerical.mip Traceback (most recent call last): ... NotImplementedError: the solver "an ILP-based SAT Solver" does not support xor clauses @@ -339,7 +339,7 @@ def SAT(solver=None, *args, **kwds): EXAMPLES:: - sage: SAT(solver="LP") # optional - sage.numerical.mip + sage: SAT(solver="LP") # needs sage.numerical.mip an ILP-based SAT Solver TESTS:: From d1c66423cf61be17b69dea107df2bf071c3923fd Mon Sep 17 00:00:00 2001 From: Matthias Koeppe Date: Mon, 6 Nov 2023 08:09:38 -0800 Subject: [PATCH 8/8] src/sage/sat/boolean_polynomials.py: Use file-level # optional/needs --- src/sage/sat/boolean_polynomials.py | 53 ++++++++++++++--------------- 1 file changed, 26 insertions(+), 27 deletions(-) diff --git a/src/sage/sat/boolean_polynomials.py b/src/sage/sat/boolean_polynomials.py index dc5fdb69ff0..32753175384 100644 --- a/src/sage/sat/boolean_polynomials.py +++ b/src/sage/sat/boolean_polynomials.py @@ -1,4 +1,4 @@ -# sage.doctest: needs sage.rings.polynomial.pbori +# sage.doctest: optional - pycryptosat, needs sage.modules sage.rings.polynomial.pbori """ SAT Functions for Boolean Polynomials @@ -72,8 +72,8 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): We construct a very small-scale AES system of equations:: - sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) # needs sage.modules sage.rings.finite_rings - sage: while True: # workaround (see :trac:`31891`) # needs sage.modules sage.rings.finite_rings + sage: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) + sage: while True: # workaround (see :trac:`31891`) ....: try: ....: F, s = sr.polynomial_system() ....: break @@ -83,57 +83,56 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): and pass it to a SAT solver:: sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: s = solve_sat(F) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings - sage: F.subs(s[0]) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings + sage: s = solve_sat(F) + sage: F.subs(s[0]) Polynomial Sequence with 36 Polynomials in 0 Variables This time we pass a few options through to the converter and the solver:: - sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat, needs sage.modules sage.rings.finite_rings - sage: F.subs(s[0]) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings + sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) + sage: F.subs(s[0]) Polynomial Sequence with 36 Polynomials in 0 Variables We construct a very simple system with three solutions and ask for a specific number of solutions:: - sage: # optional - pycryptosat, needs sage.modules sage: B. = BooleanPolynomialRing() sage: f = a*b sage: l = solve_sat([f],n=1) sage: len(l) == 1, f.subs(l[0]) (True, 0) - sage: l = solve_sat([a*b],n=2) # optional - pycryptosat # needs sage.modules - sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat # needs sage.modules + sage: l = solve_sat([a*b],n=2) + sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) (True, 0, 0) - sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=3)) # optional - pycryptosat, needs sage.modules + sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=3)) [(0, 0), (0, 1), (1, 0)] - sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=4)) # optional - pycryptosat, needs sage.modules + sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=4)) [(0, 0), (0, 1), (1, 0)] - sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=infinity)) # optional - pycryptosat, needs sage.modules + sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=infinity)) [(0, 0), (0, 1), (1, 0)] In the next example we see how the ``target_variables`` parameter works:: sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: R. = BooleanPolynomialRing() # optional - pycryptosat # needs sage.modules - sage: F = [a + b, a + c + d] # optional - pycryptosat # needs sage.modules + sage: R. = BooleanPolynomialRing() + sage: F = [a + b, a + c + d] First the normal use case:: - sage: sorted((D[a], D[b], D[c], D[d]) # optional - pycryptosat # needs sage.modules + sage: sorted((D[a], D[b], D[c], D[d]) ....: for D in solve_sat(F, n=infinity)) [(0, 0, 0, 0), (0, 0, 1, 1), (1, 1, 0, 1), (1, 1, 1, 0)] Now we are only interested in the solutions of the variables a and b:: - sage: solve_sat(F, n=infinity, target_variables=[a,b]) # optional - pycryptosat, needs sage.modules + sage: solve_sat(F, n=infinity, target_variables=[a,b]) [{b: 0, a: 0}, {b: 1, a: 1}] Here, we generate and solve the cubic equations of the AES SBox (see :trac:`26676`):: - sage: # long time, optional - pycryptosat, needs sage.modules + sage: # long time sage: from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence sage: from sage.sat.boolean_polynomials import solve as solve_sat sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, @@ -145,7 +144,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): sage: variables = ",".join(variables) sage: R = BooleanPolynomialRing(16, variables) sage: eqs = [R(eq) for eq in eqs] - sage: sls_aes = solve_sat(eqs, n = infinity) + sage: sls_aes = solve_sat(eqs, n=infinity) sage: len(sls_aes) 256 @@ -168,7 +167,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds): ....: k9 + k28, ....: k11 + k20] sage: from sage.sat.boolean_polynomials import solve as solve_sat - sage: solve_sat(keqs, n=1, solver=SAT('cryptominisat')) # optional - pycryptosat + sage: solve_sat(keqs, n=1, solver=SAT('cryptominisat')) [{k28: 0, k26: 1, k24: 0, @@ -342,16 +341,16 @@ def learn(F, converter=None, solver=None, max_learnt_length=3, interreduction=Fa EXAMPLES:: - sage: from sage.sat.boolean_polynomials import learn as learn_sat # optional - pycryptosat + sage: from sage.sat.boolean_polynomials import learn as learn_sat We construct a simple system and solve it:: - sage: set_random_seed(2300) - sage: sr = mq.SR(1, 2, 2, 4, gf2=True, polybori=True) # optional - pycryptosat, needs sage.modules sage.rings.finite_rings - sage: F,s = sr.polynomial_system() # optional - pycryptosat # needs sage.modules sage.rings.finite_rings - sage: H = learn_sat(F) # optional - pycryptosat # needs sage.modules sage.rings.finite_rings - sage: H[-1] # optional - pycryptosat # needs sage.modules sage.rings.finite_rings - k033 + 1 + sage: set_random_seed(2300) + sage: sr = mq.SR(1, 2, 2, 4, gf2=True, polybori=True) + sage: F,s = sr.polynomial_system() + sage: H = learn_sat(F) + sage: H[-1] + k033 + 1 """ try: len(F)