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:
Learn new polynomials by running SAT-solver solver on SAT-instance produced by converter from F.
INPUT:
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.
EXAMPLE:
sage: from sage.sat.boolean_polynomials import learn as learn_sat # optional - cryptominisat
We construct a simple system and solve it:
sage: set_random_seed(2300) # optional - cryptominisat
sage: sr = mq.SR(1,2,2,4,gf2=True,polybori=True) # optional - cryptominisat
sage: F,s = sr.polynomial_system() # optional - cryptominisat
sage: H = learn_sat(F) # optional - cryptominisat
sage: H[-1] # optional - cryptominisat
k033 + 1
We construct a slightly larger equation system and recover some equations after 20 restarts:
sage: set_random_seed(2300) # optional - cryptominisat
sage: sr = mq.SR(1,4,4,4,gf2=True,polybori=True) # optional - cryptominisat
sage: F,s = sr.polynomial_system() # optional - cryptominisat
sage: from sage.sat.boolean_polynomials import learn as learn_sat # optional - cryptominisat
sage: H = learn_sat(F, s_maxrestarts=20, interreduction=True) # optional - cryptominisat
sage: H[-1] # optional - cryptominisat, output random
k001200*s031*x011201 + k001200*x011201
Note
This function is meant to be called with some parameter such that the SAT-solver is interrupted. For CryptoMiniSat this is max_restarts, so pass ‘c_max_restarts’ to limit the number of restarts CryptoMiniSat will attempt. If no such parameter is passed, then this function behaves essentially like solve() except that this function does not support n>1.
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)
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.
EXAMPLE:
We construct a very small-scale AES system of equations:
sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True)
sage: F,s = sr.polynomial_system()
and pass it to a SAT solver:
sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - cryptominisat
sage: s = solve_sat(F) # optional - cryptominisat
sage: F.subs(s[0]) # optional - cryptominisat
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, s_verbosity=1, c_max_vars_sparse=4, c_cutting_number=8) # optional - cryptominisat
sage: F.subs(s[0]) # optional - cryptominisat
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 - cryptominisat
sage: f = a*b # optional - cryptominisat
sage: l = solve_sat([f],n=1) # optional - cryptominisat
sage: len(l) == 1, f.subs(l[0]) # optional - cryptominisat
(True, 0)
sage: l = sorted(solve_sat([a*b],n=2)) # optional - cryptominisat
sage: len(l) == 2, f.subs(l[0]), f.subs(l[1]) # optional - cryptominisat
(True, 0, 0)
sage: sorted(solve_sat([a*b],n=3)) # optional - cryptominisat
[{b: 0, a: 0}, {b: 0, a: 1}, {b: 1, a: 0}]
sage: sorted(solve_sat([a*b],n=4)) # optional - cryptominisat
[{b: 0, a: 0}, {b: 0, a: 1}, {b: 1, a: 0}]
sage: sorted(solve_sat([a*b],n=infinity)) # optional - cryptominisat
[{b: 0, a: 0}, {b: 0, a: 1}, {b: 1, a: 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 - cryptominisat
sage: R.<a,b,c,d> = BooleanPolynomialRing() # optional - cryptominisat
sage: F = [a+b,a+c+d] # optional - cryptominisat
First the normal use case:
sage: solve_sat(F,n=infinity) # optional - cryptominisat
[{d: 0, b: 0, c: 0, a: 0}, {d: 1, b: 1, c: 0, a: 1},
{d: 1, b: 0, c: 1, a: 0}, {d: 0, b: 1, c: 1, a: 1}]
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 - cryptominisat
[{b: 0, a: 0}, {b: 1, a: 1}]
Note
Although supported, passing converter and solver objects instead of classes is discouraged because these objects are stateful.