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 by converter from F.

INPUT:

  • F – a sequence of Boolean polynomials

  • converter – an ANF to CNF converter class or object. If converter is None then sage.sat.converters.polybori.CNFEncoder is used to construct a new converter. (default: None)

  • solver – a SAT-solver class or object. If solver is None then sage.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_ and s_ respectively. For example, to increase CryptoMiniSat’s verbosity level, pass s_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 by converter – using solver.

INPUT:

  • F – a sequence of Boolean polynomials

  • n – number of solutions to return. If n is +infinity then all solutions are returned. If n <infinity then n solutions are returned if F has at least n solutions. Otherwise, all solutions of F are returned. (default: 1)

  • converter – an ANF to CNF converter class or object. If converter is None then sage.sat.converters.polybori.CNFEncoder is used to construct a new converter. (default: None)

  • solver – a SAT-solver class or object. If solver is None then sage.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. Furthermore target_variables denotes which variable-value pairs appear in the solutions. If target_variables is None all variables appearing in the polynomials of F are used to construct exclusion clauses. (default: None)

  • **kwds – parameters can be passed to the converter and the

    solver by prefixing them with c_ and s_ respectively. For example, to increase CryptoMiniSat’s verbosity level, pass s_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.