Skip to content

Commit cc1307b

Browse files
author
Matthias Koeppe
committed
More # optional
1 parent c9717a3 commit cc1307b

File tree

3 files changed

+47
-43
lines changed

3 files changed

+47
-43
lines changed

‎src/sage/sat/boolean_polynomials.py

Lines changed: 40 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -71,8 +71,8 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds):
7171
7272
We construct a very small-scale AES system of equations::
7373
74-
sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True)
75-
sage: while True: # workaround (see :trac:`31891`)
74+
sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True) # optional - sage.modules
75+
sage: while True: # workaround (see :trac:`31891`) # optional - sage.modules
7676
....: try:
7777
....: F, s = sr.polynomial_system()
7878
....: break
@@ -81,74 +81,77 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds):
8181
8282
and pass it to a SAT solver::
8383
84-
sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat
85-
sage: s = solve_sat(F) # optional - pycryptosat
86-
sage: F.subs(s[0]) # optional - pycryptosat
84+
sage: from sage.sat.boolean_polynomials import solve as solve_sat
85+
sage: s = solve_sat(F) # optional - pycryptosat sage.modules
86+
sage: F.subs(s[0]) # optional - pycryptosat sage.modules
8787
Polynomial Sequence with 36 Polynomials in 0 Variables
8888
8989
This time we pass a few options through to the converter and the solver::
9090
91-
sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat
92-
sage: F.subs(s[0]) # optional - pycryptosat
91+
sage: s = solve_sat(F, c_max_vars_sparse=4, c_cutting_number=8) # optional - pycryptosat sage.modules
92+
sage: F.subs(s[0]) # optional - pycryptosat sage.modules
9393
Polynomial Sequence with 36 Polynomials in 0 Variables
9494
95-
We construct a very simple system with three solutions and ask for a specific number of solutions::
95+
We construct a very simple system with three solutions
96+
and ask for a specific number of solutions::
9697
97-
sage: B.<a,b> = BooleanPolynomialRing() # optional - pycryptosat
98-
sage: f = a*b # optional - pycryptosat
99-
sage: l = solve_sat([f],n=1) # optional - pycryptosat
100-
sage: len(l) == 1, f.subs(l[0]) # optional - pycryptosat
98+
sage: B.<a,b> = BooleanPolynomialRing() # optional - pycryptosat sage.modules
99+
sage: f = a*b # optional - pycryptosat sage.modules
100+
sage: l = solve_sat([f],n=1) # optional - pycryptosat sage.modules
101+
sage: len(l) == 1, f.subs(l[0]) # optional - pycryptosat sage.modules
101102
(True, 0)
102103
103-
sage: l = solve_sat([a*b],n=2) # optional - pycryptosat
104-
sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat
104+
sage: l = solve_sat([a*b],n=2) # optional - pycryptosat sage.modules
105+
sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - pycryptosat sage.modules
105106
(True, 0, 0)
106107
107-
sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=3)) # optional - pycryptosat
108+
sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=3)) # optional - pycryptosat sage.modules
108109
[(0, 0), (0, 1), (1, 0)]
109-
sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=4)) # optional - pycryptosat
110+
sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=4)) # optional - pycryptosat sage.modules
110111
[(0, 0), (0, 1), (1, 0)]
111-
sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=infinity)) # optional - pycryptosat
112+
sage: sorted((d[a], d[b]) for d in solve_sat([a*b], n=infinity)) # optional - pycryptosat sage.modules
112113
[(0, 0), (0, 1), (1, 0)]
113114
114115
In the next example we see how the ``target_variables`` parameter works::
115116
116-
sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat
117-
sage: R.<a,b,c,d> = BooleanPolynomialRing() # optional - pycryptosat
118-
sage: F = [a+b,a+c+d] # optional - pycryptosat
117+
sage: from sage.sat.boolean_polynomials import solve as solve_sat
118+
sage: R.<a,b,c,d> = BooleanPolynomialRing() # optional - pycryptosat sage.modules
119+
sage: F = [a + b, a + c + d] # optional - pycryptosat sage.modules
119120
120121
First the normal use case::
121122
122-
sage: sorted((D[a], D[b], D[c], D[d]) for D in solve_sat(F,n=infinity)) # optional - pycryptosat
123+
sage: sorted((D[a], D[b], D[c], D[d]) # optional - pycryptosat sage.modules
124+
....: for D in solve_sat(F, n=infinity))
123125
[(0, 0, 0, 0), (0, 0, 1, 1), (1, 1, 0, 1), (1, 1, 1, 0)]
124126
125127
Now we are only interested in the solutions of the variables a and b::
126128
127-
sage: solve_sat(F,n=infinity,target_variables=[a,b]) # optional - pycryptosat
129+
sage: solve_sat(F,n=infinity,target_variables=[a,b]) # optional - pycryptosat sage.modules
128130
[{b: 0, a: 0}, {b: 1, a: 1}]
129131
130132
Here, we generate and solve the cubic equations of the AES SBox (see :trac:`26676`)::
131133
132-
sage: from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence # optional - pycryptosat, long time
133-
sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - pycryptosat, long time
134-
sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, allow_zero_inversions = True) # optional - pycryptosat, long time
135-
sage: sb = sr.sbox() # optional - pycryptosat, long time
136-
sage: eqs = sb.polynomials(degree = 3) # optional - pycryptosat, long time
137-
sage: eqs = PolynomialSequence(eqs) # optional - pycryptosat, long time
138-
sage: variables = map(str, eqs.variables()) # optional - pycryptosat, long time
139-
sage: variables = ",".join(variables) # optional - pycryptosat, long time
140-
sage: R = BooleanPolynomialRing(16, variables) # optional - pycryptosat, long time
141-
sage: eqs = [R(eq) for eq in eqs] # optional - pycryptosat, long time
142-
sage: sls_aes = solve_sat(eqs, n = infinity) # optional - pycryptosat, long time
143-
sage: len(sls_aes) # optional - pycryptosat, long time
134+
sage: from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence
135+
sage: from sage.sat.boolean_polynomials import solve as solve_sat
136+
sage: sr = sage.crypto.mq.SR(1, 4, 4, 8, # long time, optional - pycryptosat sage.modules
137+
....: allow_zero_inversions=True)
138+
sage: sb = sr.sbox() # long time, optional - pycryptosat sage.modules
139+
sage: eqs = sb.polynomials(degree = 3) # long time, optional - pycryptosat sage.modules
140+
sage: eqs = PolynomialSequence(eqs) # long time, optional - pycryptosat sage.modules
141+
sage: variables = map(str, eqs.variables()) # long time, optional - pycryptosat sage.modules
142+
sage: variables = ",".join(variables) # long time, optional - pycryptosat sage.modules
143+
sage: R = BooleanPolynomialRing(16, variables) # long time, optional - pycryptosat sage.modules
144+
sage: eqs = [R(eq) for eq in eqs] # long time, optional - pycryptosat sage.modules
145+
sage: sls_aes = solve_sat(eqs, n = infinity) # long time, optional - pycryptosat sage.modules
146+
sage: len(sls_aes) # long time, optional - pycryptosat sage.modules
144147
256
145148
146149
TESTS:
147150
148151
Test that :trac:`26676` is fixed::
149152
150153
sage: varl = ['k{0}'.format(p) for p in range(29)]
151-
sage: B = BooleanPolynomialRing(names = varl)
154+
sage: B = BooleanPolynomialRing(names=varl)
152155
sage: B.inject_variables(verbose=False)
153156
sage: keqs = [
154157
....: k0 + k6 + 1,
@@ -162,7 +165,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds):
162165
....: k9 + k28,
163166
....: k11 + k20]
164167
sage: from sage.sat.boolean_polynomials import solve as solve_sat
165-
sage: solve_sat(keqs, n=1, solver=SAT('cryptominisat')) # optional - pycryptosat
168+
sage: solve_sat(keqs, n=1, solver=SAT('cryptominisat')) # optional - pycryptosat
166169
[{k28: 0,
167170
k26: 1,
168171
k24: 0,
@@ -187,7 +190,7 @@ def solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds):
187190
k2: 0,
188191
k1: 0,
189192
k0: 0}]
190-
sage: solve_sat(keqs, n=1, solver=SAT('picosat')) # optional - pycosat
193+
sage: solve_sat(keqs, n=1, solver=SAT('picosat')) # optional - pycosat
191194
[{k28: 0,
192195
k26: 1,
193196
k24: 0,

‎src/sage/sat/converters/polybori.py

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
# sage.doctest: optional - sage.rings.polynomial.pbori
12
"""
23
An ANF to CNF Converter using a Dense/Sparse Strategy
34

‎src/sage/sat/solvers/satsolver.pyx

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -139,9 +139,9 @@ cdef class SatSolver:
139139
140140
sage: from io import StringIO
141141
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")
142-
sage: from sage.sat.solvers.sat_lp import SatLP
143-
sage: solver = SatLP()
144-
sage: solver.read(file_object)
142+
sage: from sage.sat.solvers.sat_lp import SatLP # optional - sage.numerical.mip
143+
sage: solver = SatLP() # optional - sage.numerical.mip
144+
sage: solver.read(file_object) # optional - sage.numerical.mip
145145
Traceback (most recent call last):
146146
...
147147
NotImplementedError: the solver "an ILP-based SAT Solver" does not support xor clauses
@@ -339,7 +339,7 @@ def SAT(solver=None, *args, **kwds):
339339
340340
EXAMPLES::
341341
342-
sage: SAT(solver="LP")
342+
sage: SAT(solver="LP") # optional - sage.numerical.mip
343343
an ILP-based SAT Solver
344344
345345
TESTS::
@@ -351,12 +351,12 @@ def SAT(solver=None, *args, **kwds):
351351
352352
Forcing CryptoMiniSat::
353353
354-
sage: SAT(solver="cryptominisat") # optional - pycryptosat
354+
sage: SAT(solver="cryptominisat") # optional - pycryptosat
355355
CryptoMiniSat solver: 0 variables, 0 clauses.
356356
357357
Forcing PicoSat::
358358
359-
sage: SAT(solver="picosat") # optional - pycosat
359+
sage: SAT(solver="picosat") # optional - pycosat
360360
PicoSAT solver: 0 variables, 0 clauses.
361361
362362
Forcing Glucose::

0 commit comments

Comments
 (0)