Skip to content

Commit

Permalink
gh-36658: sage.sat: Update # needs
Browse files Browse the repository at this point in the history 
    
<!-- ^^^^^
Please provide a concise, informative and self-explanatory title.
Don't put issue numbers in there, do this in the PR body below.
For example, instead of "Fixes #1234" use "Introduce new method to
calculate 1+1"
-->
<!-- Describe your changes here in detail -->

<!-- Why is this change required? What problem does it solve? -->
<!-- If this PR resolves an open issue, please link to it here. For
example "Fixes #12345". -->
Cherry-picked from #35095.
<!-- If your change requires a documentation PR, please link it
appropriately. -->

### 📝 Checklist

<!-- Put an `x` in all the boxes that apply. -->
<!-- If your change requires a documentation PR, please link it
appropriately -->
<!-- If you're unsure about any of these, don't hesitate to ask. We're
here to help! -->
<!-- Feel free to remove irrelevant items. -->

- [x] The title is concise, informative, and self-explanatory.
- [ ] The description explains in detail what this PR is about.
- [ ] I have linked a relevant issue or discussion.
- [ ] I have created tests covering the changes.
- [ ] I have updated the documentation accordingly.

### ⌛ Dependencies

<!-- List all open PRs that this PR logically depends on
- #12345: short description why this is a dependency
- #34567: ...
-->

<!-- If you're unsure about any of these, don't hesitate to ask. We're
here to help! -->
    
URL: #36658
Reported by: Matthias Köppe
Reviewer(s): David Coudert, Matthias Köppe
  • Loading branch information
Release Manager committed Dec 4, 2023
2 parents b707b29 + d1c6642 commit 3253ed9
Show file tree
Hide file tree
Showing 8 changed files with 94 additions and 79 deletions.
91 changes: 48 additions & 43 deletions src/sage/sat/boolean_polynomials.py
View file
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
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
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
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
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
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
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
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

0 comments on commit 3253ed9

Please sign in to comment.