# 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)#

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 # optional - pycryptosat
```

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.sat.boolean_polynomials.solve(F, converter=None, solver=None, n=1, target_variables=None, **kwds)#

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 :trac:`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 # optional - pycryptosat
sage: s = solve_sat(F)                                            # optional - pycryptosat
sage: F.subs(s[0])                                                # optional - pycryptosat
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
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() # 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
(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
(True, 0, 0)

sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=3))  # optional - pycryptosat
[(0, 0), (0, 1), (1, 0)]
sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=4))   # optional - pycryptosat
[(0, 0), (0, 1), (1, 0)]
sage: sorted((d[a], d[b]) for d in solve_sat([a*b],n=infinity))  # optional - pycryptosat
[(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
```

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
[(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
[{b: 0, a: 0}, {b: 1, a: 1}]
```

Here, we generate and solve the cubic equations of the AES SBox (see trac ticket #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
256
```

Note

Although supported, passing converter and solver objects instead of classes is discouraged because these objects are stateful.