SAT Functions for Boolean Polynomials#
These highlevel functions support solving and learning from Boolean polynomial systems. In this context, “learning” means the construction of new polynomials in the ideal spanned by the original polynomials.
AUTHOR:
Martin Albrecht (2012): initial version
Functions#
- sage.sat.boolean_polynomials.learn(F, converter=None, solver=None, max_learnt_length=3, interreduction=False, **kwds)[source]#
Learn new polynomials by running SAT-solver
solver
on SAT-instance produced byconverter
fromF
.INPUT:
F
– a sequence of Boolean polynomialsconverter
– an ANF to CNF converter class or object. Ifconverter
isNone
thensage.sat.converters.polybori.CNFEncoder
is used to construct a new converter. (default:None
)solver
– a SAT-solver class or object. Ifsolver
isNone
thensage.sat.solvers.cryptominisat.CryptoMiniSat
is used to construct a new converter. (default:None
)max_learnt_length
– only clauses of length <=max_length_learnt
are considered and converted to polynomials. (default:3
)interreduction
– inter-reduce the resulting polynomials (default:False
)
Note
More parameters can be passed to the converter and the solver by prefixing them with
c_
ands_
respectively. For example, to increase CryptoMiniSat’s verbosity level, passs_verbosity=1
.OUTPUT:
A sequence of Boolean polynomials.
EXAMPLES:
sage: from sage.sat.boolean_polynomials import learn as learn_sat
>>> from sage.all import * >>> 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) sage: F,s = sr.polynomial_system() sage: H = learn_sat(F) sage: H[-1] k033 + 1
>>> from sage.all import * >>> set_random_seed(Integer(2300)) >>> sr = mq.SR(Integer(1), Integer(2), Integer(2), Integer(4), gf2=True, polybori=True) >>> F,s = sr.polynomial_system() >>> H = learn_sat(F) >>> H[-Integer(1)] k033 + 1
- sage.sat.boolean_polynomials.solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds)[source]#
Solve system of Boolean polynomials
F
by solving the SAT-problem – produced byconverter
– usingsolver
.INPUT:
F
– a sequence of Boolean polynomialsn
– number of solutions to return. Ifn
is +infinity then all solutions are returned. Ifn <infinity
thenn
solutions are returned ifF
has at leastn
solutions. Otherwise, all solutions ofF
are returned. (default:1
)converter
– an ANF to CNF converter class or object. Ifconverter
isNone
thensage.sat.converters.polybori.CNFEncoder
is used to construct a new converter. (default:None
)solver
– a SAT-solver class or object. Ifsolver
isNone
thensage.sat.solvers.cryptominisat.CryptoMiniSat
is used to construct a new converter. (default:None
)target_variables
– a list of variables. The elements of the list are used to exclude a particular combination of variable assignments of a solution from any further solution. Furthermoretarget_variables
denotes which variable-value pairs appear in the solutions. Iftarget_variables
isNone
all variables appearing in the polynomials ofF
are used to construct exclusion clauses. (default:None
)**kwds
– parameters can be passed to the converter and thesolver by prefixing them with
c_
ands_
respectively. For example, to increase CryptoMiniSat’s verbosity level, passs_verbosity=1
.
OUTPUT:
A list of dictionaries, each of which contains a variable assignment solving
F
.EXAMPLES:
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 :issue:`31891`) ....: try: ....: F, s = sr.polynomial_system() ....: break ....: except ZeroDivisionError: ....: pass
>>> from sage.all import * >>> sr = mq.SR(Integer(1), Integer(1), Integer(1), Integer(4), gf2=True, polybori=True) >>> while True: # workaround (see :issue:`31891`) ... try: ... F, s = sr.polynomial_system() ... break ... except ZeroDivisionError: ... pass
and pass it to a SAT solver:
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
>>> from sage.all import * >>> from sage.sat.boolean_polynomials import solve as solve_sat >>> s = solve_sat(F) >>> F.subs(s[Integer(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) sage: F.subs(s[0]) Polynomial Sequence with 36 Polynomials in 0 Variables
>>> from sage.all import * >>> s = solve_sat(F, c_max_vars_sparse=Integer(4), c_cutting_number=Integer(8)) >>> F.subs(s[Integer(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: 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) 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)) [(0, 0), (0, 1), (1, 0)] 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)) [(0, 0), (0, 1), (1, 0)]
>>> from sage.all import * >>> B = BooleanPolynomialRing(names=('a', 'b',)); (a, b,) = B._first_ngens(2) >>> f = a*b >>> l = solve_sat([f],n=Integer(1)) >>> len(l) == Integer(1), f.subs(l[Integer(0)]) (True, 0) >>> l = solve_sat([a*b],n=Integer(2)) >>> len(l) == Integer(2), f.subs(l[Integer(0)]), f.subs(l[Integer(1)]) (True, 0, 0) >>> sorted((d[a], d[b]) for d in solve_sat([a*b], n=Integer(3))) [(0, 0), (0, 1), (1, 0)] >>> sorted((d[a], d[b]) for d in solve_sat([a*b], n=Integer(4))) [(0, 0), (0, 1), (1, 0)] >>> 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.<a,b,c,d> = BooleanPolynomialRing() sage: F = [a + b, a + c + d]
>>> from sage.all import * >>> from sage.sat.boolean_polynomials import solve as solve_sat >>> R = BooleanPolynomialRing(names=('a', 'b', 'c', 'd',)); (a, b, c, d,) = R._first_ngens(4) >>> 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)) [(0, 0, 0, 0), (0, 0, 1, 1), (1, 1, 0, 1), (1, 1, 1, 0)]
>>> from sage.all import * >>> 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]) [{b: 0, a: 0}, {b: 1, a: 1}]
>>> from sage.all import * >>> 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 Issue #26676):
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
>>> from sage.all import * >>> # long time >>> from sage.rings.polynomial.multi_polynomial_sequence import PolynomialSequence >>> from sage.sat.boolean_polynomials import solve as solve_sat >>> sr = sage.crypto.mq.SR(Integer(1), Integer(4), Integer(4), Integer(8), ... allow_zero_inversions=True) >>> sb = sr.sbox() >>> eqs = sb.polynomials(degree=Integer(3)) >>> eqs = PolynomialSequence(eqs) >>> variables = map(str, eqs.variables()) >>> variables = ",".join(variables) >>> R = BooleanPolynomialRing(Integer(16), variables) >>> eqs = [R(eq) for eq in eqs] >>> sls_aes = solve_sat(eqs, n=infinity) >>> len(sls_aes) 256
Note
Although supported, passing converter and solver objects instead of classes is discouraged because these objects are stateful.