Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

sage.sat: Update # needs #36658

Merged
merged 8 commits into from
Dec 6, 2023
Merged

sage.sat: Update # needs #36658

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
dd20a8c
More # optional
mkoeppe Jun 9, 2023
c9717a3
Modularization fixes for imports
mkoeppe Jun 11, 2023
cc1307b
More # optional
mkoeppe Jun 11, 2023
a37b456
More # optional
mkoeppe Jun 11, 2023
a12c38c
More # optional
mkoeppe Jun 12, 2023
e43e09a
src/sage/sat: Update file-level doctest tag
mkoeppe Aug 7, 2023
417429f
src/sage/sat: sage -fixdoctests --only-tags
mkoeppe Aug 8, 2023
d1c6642
src/sage/sat/boolean_polynomials.py: Use file-level # optional/needs
mkoeppe Nov 6, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
91 changes: 48 additions & 43 deletions src/sage/sat/boolean_polynomials.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
# sage.doctest: optional - pycryptosat, needs sage.modules sage.rings.polynomial.pbori
"""
SAT Functions for Boolean Polynomials

Expand Down Expand Up @@ -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()
Expand All @@ -81,74 +82,78 @@ 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.<a,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.<a,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.<a,b,c,d> = 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.<a,b,c,d> = 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:

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,
Expand All @@ -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,
Expand All @@ -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,
Expand Down Expand Up @@ -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)
Expand Down
5 changes: 4 additions & 1 deletion src/sage/sat/converters/__init__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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')
1 change: 1 addition & 0 deletions src/sage/sat/converters/polybori.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
# sage.doctest: needs sage.rings.polynomial.pbori
"""
An ANF to CNF Converter using a Dense/Sparse Strategy

Expand Down
33 changes: 18 additions & 15 deletions src/sage/sat/solvers/cryptominisat.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions src/sage/sat/solvers/dimacs.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
24 changes: 13 additions & 11 deletions src/sage/sat/solvers/picosat.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/sage/sat/solvers/sat_lp.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
# sage.doctest: needs sage.numerical.mip
r"""
Solve SAT problems Integer Linear Programming

Expand Down
12 changes: 6 additions & 6 deletions src/sage/sat/solvers/satsolver.pyx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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::
Expand All @@ -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::
Expand Down
Loading