diff --git a/src/sage/sat/boolean_polynomials.py b/src/sage/sat/boolean_polynomials.py index 80b1a13d89c..32753175384 100644 --- a/src/sage/sat/boolean_polynomials.py +++ b/src/sage/sat/boolean_polynomials.py @@ -1,3 +1,4 @@ +# sage.doctest: optional - pycryptosat, needs sage.modules sage.rings.polynomial.pbori """ SAT Functions for Boolean Polynomials @@ -71,7 +72,7 @@ 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: sr = mq.SR(1, 1, 1, 4, gf2=True, polybori=True) sage: while True: # workaround (see :trac:`31891`) ....: try: ....: F, s = sr.polynomial_system() @@ -81,66 +82,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 # 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) + 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 - sage: F.subs(s[0]) # optional - pycryptosat + 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:: + 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() + 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: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat + 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 + 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 + 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 + 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 # 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() + sage: F = [a + b, a + c + d] 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]) + ....: 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]) [{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: # 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, + ....: allow_zero_inversions=True) + 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: @@ -148,7 +153,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 +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, @@ -187,7 +192,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, @@ -336,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) # 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 - 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) 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') diff --git a/src/sage/sat/converters/polybori.py b/src/sage/sat/converters/polybori.py index ca39def12c1..49da6f1819c 100644 --- a/src/sage/sat/converters/polybori.py +++ b/src/sage/sat/converters/polybori.py @@ -1,3 +1,4 @@ +# sage.doctest: needs sage.rings.polynomial.pbori """ An ANF to CNF Converter using a Dense/Sparse Strategy 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 cfe3c7cd4ed..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) - sage: while True: # workaround (see :trac:`31891`) + 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 + 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/sat_lp.py b/src/sage/sat/solvers/sat_lp.py index d96ed62b125..9b65b1d241d 100644 --- a/src/sage/sat/solvers/sat_lp.py +++ b/src/sage/sat/solvers/sat_lp.py @@ -1,3 +1,4 @@ +# sage.doctest: needs sage.numerical.mip r""" Solve SAT problems Integer Linear Programming diff --git a/src/sage/sat/solvers/satsolver.pyx b/src/sage/sat/solvers/satsolver.pyx index 1c4ac400cb6..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 - sage: solver = SatLP() - sage: solver.read(file_object) + 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") + sage: SAT(solver="LP") # needs 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::