This converter is based on two converters. The first one, by Martin Albrecht, was based on [CB07], this is the basis of the “dense” part of the converter. It was later improved by Mate Soos. The second one, by Michael Brickenstein, uses a reduced truth table based approach and forms the “sparse” part of the converter.
AUTHORS:
REFERENCES:
[CB07] | Nicolas Courtois, Gregory V. Bard: Algebraic Cryptanalysis of the Data Encryption Standard, In 11-th IMA Conference, Cirencester, UK, 18-20 December 2007, Springer LNCS 4887. See also http://eprint.iacr.org/2006/402/. |
Bases: sage.sat.converters.anf2cnf.ANF2CNFConverter
ANF to CNF Converter using a Dense/Sparse Strategy. This converter distinguishes two classes of polynomials.
1. Sparse polynomials are those with at most max_vars_sparse variables. Those are converted using reduced truth-tables based on PolyBoRi’s internal representation.
2. Polynomials with more variables are converted by introducing new variables for monomials and by converting these linearised polynomials.
Linearised polynomials are converted either by splitting XOR chains – into chunks of length cutting_number – or by constructing XOR clauses if the underlying solver supports it. This behaviour is disabled by passing use_xor_clauses=False.
Construct ANF to CNF converter over ring passing clauses to solver.
INPUT:
EXAMPLE:
We compare the sparse and the dense strategies, sparse first:
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: e = CNFEncoder(solver, B)
sage: e.clauses_sparse(a*b + a + 1)
sage: _ = solver.write()
sage: print open(fn).read()
p cnf 3 2
1 0
-2 0
sage: e.phi
[None, a, b, c]
Now, we convert using the dense strategy:
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: e = CNFEncoder(solver, B)
sage: e.clauses_dense(a*b + a + 1)
sage: _ = solver.write()
sage: print open(fn).read()
p cnf 4 5
1 -4 0
2 -4 0
4 -1 -2 0
-4 -1 0
4 1 0
sage: e.phi
[None, a, b, c, a*b]
Note
This constructer generates SAT variables for each Boolean polynomial variable.
Encode the boolean polynomials in F .
INPUT:
OUTPUT: An inverse map int -> variable
EXAMPLE:
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: e = CNFEncoder(solver, B, max_vars_sparse=2)
sage: e([a*b + a + 1, a*b+ a + c])
[None, a, b, c, a*b]
sage: _ = solver.write()
sage: print open(fn).read()
p cnf 4 9
1 0
-2 0
1 -4 0
2 -4 0
4 -1 -2 0
-4 -1 -3 0
4 1 -3 0
4 -1 3 0
-4 1 3 0
sage: e.phi
[None, a, b, c, a*b]
Convert f using the sparse strategy if f.nvariables() is at most max_vars_sparse and the dense strategy otherwise.
INPUT:
EXAMPLE:
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: e = CNFEncoder(solver, B, max_vars_sparse=2)
sage: e.clauses(a*b + a + 1)
sage: _ = solver.write()
sage: print open(fn).read()
p cnf 3 2
1 0
-2 0
sage: e.phi
[None, a, b, c]
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: e = CNFEncoder(solver, B, max_vars_sparse=2)
sage: e.clauses(a*b + a + c)
sage: _ = solver.write()
sage: print open(fn).read()
p cnf 4 7
1 -4 0
2 -4 0
4 -1 -2 0
-4 -1 -3 0
4 1 -3 0
4 -1 3 0
-4 1 3 0
sage: e.phi
[None, a, b, c, a*b]
Convert f using the dense strategy.
INPUT:
EXAMPLE:
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: e = CNFEncoder(solver, B)
sage: e.clauses_dense(a*b + a + 1)
sage: _ = solver.write()
sage: print open(fn).read()
p cnf 4 5
1 -4 0
2 -4 0
4 -1 -2 0
-4 -1 0
4 1 0
sage: e.phi
[None, a, b, c, a*b]
Convert f using the sparse strategy.
INPUT:
EXAMPLE:
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: e = CNFEncoder(solver, B)
sage: e.clauses_sparse(a*b + a + 1)
sage: _ = solver.write()
sage: print open(fn).read()
p cnf 3 2
1 0
-2 0
sage: e.phi
[None, a, b, c]
Return SAT variable for m
INPUT:
- m - a monomial.
OUTPUT: An index for a SAT variable corresponding to m.
EXAMPLE:
sage: B.<a,b,c> = BooleanPolynomialRing() sage: from sage.sat.converters.polybori import CNFEncoder sage: from sage.sat.solvers.dimacs import DIMACS sage: fn = tmp_filename() sage: solver = DIMACS(filename=fn) sage: e = CNFEncoder(solver, B) sage: e.clauses_dense(a*b + a + 1) sage: e.phi [None, a, b, c, a*b]
If monomial is called on a new monomial, a new variable is created:
sage: e.monomial(a*b*c)
5
sage: e.phi
[None, a, b, c, a*b, a*b*c]
If monomial is called on a monomial that was queried before, the index of the old variable is returned and no new variable is created:
sage: e.monomial(a*b)
4
sage: e.phi
[None, a, b, c, a*b, a*b*c]
.. note::
For correctness, this function is cached.
Return permutations of length length which are equal to zero if equal_zero and equal to one otherwise.
A variable is false if the integer in its position is smaller than zero and true otherwise.
INPUT:
EXAMPLE:
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: ce = CNFEncoder(DIMACS(), B)
sage: ce.permutations(3, True)
[[-1, -1, -1], [1, 1, -1], [1, -1, 1], [-1, 1, 1]]
sage: ce.permutations(3, False)
[[1, -1, -1], [-1, 1, -1], [-1, -1, 1], [1, 1, 1]]
Map SAT variables to polynomial variables.
EXAMPLE:
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: ce = CNFEncoder(DIMACS(), B)
sage: ce.var()
4
sage: ce.phi
[None, a, b, c, None]
Split XOR chains into subchains.
INPUT:
EXAMPLE:
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: B.<a,b,c,d,e,f> = BooleanPolynomialRing()
sage: ce = CNFEncoder(DIMACS(), B, cutting_number=3)
sage: ce.split_xor([1,2,3,4,5,6], False)
[[[1, 7], False], [[7, 2, 8], True], [[8, 3, 9], True], [[9, 4, 10], True], [[10, 5, 11], True], [[11, 6], True]]
sage: ce = CNFEncoder(DIMACS(), B, cutting_number=4)
sage: ce.split_xor([1,2,3,4,5,6], False)
[[[1, 2, 7], False], [[7, 3, 4, 8], True], [[8, 5, 6], True]]
sage: ce = CNFEncoder(DIMACS(), B, cutting_number=5)
sage: ce.split_xor([1,2,3,4,5,6], False)
[[[1, 2, 3, 7], False], [[7, 4, 5, 6], True]]
Convert clause to sage.rings.polynomial.pbori.BooleanPolynomial
INPUT:
EXAMPLE:
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: fn = tmp_filename()
sage: solver = DIMACS(filename=fn)
sage: e = CNFEncoder(solver, B, max_vars_sparse=2)
sage: _ = e([a*b + a + 1, a*b+ a + c])
sage: e.to_polynomial( (1,-2,3) )
a*b*c + a*b + b*c + b
Return a new variable.
This is a thin wrapper around the SAT-solvers function where we keep track of which SAT variable corresponds to which monomial.
INPUT:
EXAMPLE:
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: ce = CNFEncoder(DIMACS(), B)
sage: ce.var()
4
Divides the zero set of f into blocks.
EXAMPLE:
sage: B.<a,b,c> = BooleanPolynomialRing()
sage: from sage.sat.converters.polybori import CNFEncoder
sage: from sage.sat.solvers.dimacs import DIMACS
sage: e = CNFEncoder(DIMACS(), B)
sage: sorted(e.zero_blocks(a*b*c))
[{c: 0}, {b: 0}, {a: 0}]
Note
This function is randomised.