An ANF to CNF Converter using a Dense/Sparse Strategy

This converter is based on two converters. The first one, by Martin Albrecht, was based on [CB2007], 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:

  • Martin Albrecht - (2008-09) initial version of ‘anf2cnf.py’

  • Michael Brickenstein - (2009) ‘cnf.py’ for PolyBoRi

  • Mate Soos - (2010) improved version of ‘anf2cnf.py’

  • Martin Albrecht - (2012) unified and added to Sage

Classes and Methods

class sage.sat.converters.polybori.CNFEncoder(solver, ring, max_vars_sparse=6, use_xor_clauses=None, cutting_number=6, random_seed=16)[source]

Bases: 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.

__init__(solver, ring, max_vars_sparse=6, use_xor_clauses=None, cutting_number=6, random_seed=16)[source]

Construct ANF to CNF converter over ring passing clauses to solver.

INPUT:

  • solver – a SAT-solver instance

  • ring – a sage.rings.polynomial.pbori.BooleanPolynomialRing

  • max_vars_sparse – maximum number of variables for direct conversion

  • use_xor_clauses – use XOR clauses; if None use if solver supports it. (default: None)

  • cutting_number – maximum length of XOR chains after splitting if XOR clauses are not supported (default: 6)

  • random_seed – the direct conversion method uses randomness, this sets the seed (default: 16)

EXAMPLES:

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
-2 0
1 0
sage: e.phi
[None, a, b, c]

>>> from sage.all import *
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> e = CNFEncoder(solver, B)
>>> e.clauses_sparse(a*b + a + Integer(1))
>>> _ = solver.write()
>>> print(open(fn).read())
p cnf 3 2
-2 0
1 0
>>> e.phi
[None, a, b, c]

B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B)
e.clauses_sparse(a*b + a + 1)
_ = solver.write()
print(open(fn).read())
e.phi

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]

>>> from sage.all import *
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> e = CNFEncoder(solver, B)
>>> e.clauses_dense(a*b + a + Integer(1))
>>> _ = solver.write()
>>> print(open(fn).read())
p cnf 4 5
1 -4 0
2 -4 0
4 -1 -2 0
-4 -1 0
4 1 0
>>> e.phi
[None, a, b, c, a*b]

B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B)
e.clauses_dense(a*b + a + 1)
_ = solver.write()
print(open(fn).read())
e.phi

Note

This constructor generates SAT variables for each Boolean polynomial variable.

__call__(F)[source]

Encode the boolean polynomials in F .

INPUT:

  • F – an iterable of sage.rings.polynomial.pbori.BooleanPolynomial

OUTPUT: an inverse map int -> variable

EXAMPLES:

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
-2 0
1 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]

>>> from sage.all import *
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> e = CNFEncoder(solver, B, max_vars_sparse=Integer(2))
>>> e([a*b + a + Integer(1), a*b+ a + c])
[None, a, b, c, a*b]
>>> _ = solver.write()
>>> print(open(fn).read())
p cnf 4 9
-2 0
1 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

>>> e.phi
[None, a, b, c, a*b]

B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B, max_vars_sparse=2)
e([a*b + a + 1, a*b+ a + c])
_ = solver.write()
print(open(fn).read())
e.phi
clauses(f)[source]

Convert f using the sparse strategy if f.nvariables() is at most max_vars_sparse and the dense strategy otherwise.

INPUT:

  • f – a sage.rings.polynomial.pbori.BooleanPolynomial

EXAMPLES:

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
-2 0
1 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]

>>> from sage.all import *
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> e = CNFEncoder(solver, B, max_vars_sparse=Integer(2))
>>> e.clauses(a*b + a + Integer(1))
>>> _ = solver.write()
>>> print(open(fn).read())
p cnf 3 2
-2 0
1 0
>>> e.phi
[None, a, b, c]

>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> e = CNFEncoder(solver, B, max_vars_sparse=Integer(2))
>>> e.clauses(a*b + a + c)
>>> _ = solver.write()
>>> 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

>>> e.phi
[None, a, b, c, a*b]

B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B, max_vars_sparse=2)
e.clauses(a*b + a + 1)
_ = solver.write()
print(open(fn).read())
e.phi
B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B, max_vars_sparse=2)
e.clauses(a*b + a + c)
_ = solver.write()
print(open(fn).read())
e.phi
clauses_dense(f)[source]

Convert f using the dense strategy.

INPUT:

  • f – a sage.rings.polynomial.pbori.BooleanPolynomial

EXAMPLES:

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]

>>> from sage.all import *
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> e = CNFEncoder(solver, B)
>>> e.clauses_dense(a*b + a + Integer(1))
>>> _ = solver.write()
>>> print(open(fn).read())
p cnf 4 5
1 -4 0
2 -4 0
4 -1 -2 0
-4 -1 0
4 1 0
>>> e.phi
[None, a, b, c, a*b]

B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B)
e.clauses_dense(a*b + a + 1)
_ = solver.write()
print(open(fn).read())
e.phi
clauses_sparse(f)[source]

Convert f using the sparse strategy.

INPUT:

  • f – a sage.rings.polynomial.pbori.BooleanPolynomial

EXAMPLES:

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
-2 0
1 0
sage: e.phi
[None, a, b, c]

>>> from sage.all import *
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> e = CNFEncoder(solver, B)
>>> e.clauses_sparse(a*b + a + Integer(1))
>>> _ = solver.write()
>>> print(open(fn).read())
p cnf 3 2
-2 0
1 0
>>> e.phi
[None, a, b, c]

B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B)
e.clauses_sparse(a*b + a + 1)
_ = solver.write()
print(open(fn).read())
e.phi
monomial(m)[source]

Return SAT variable for m.

INPUT:

  • m – a monomial

OUTPUT: an index for a SAT variable corresponding to m

EXAMPLES:

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]

>>> from sage.all import *
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> e = CNFEncoder(solver, B)
>>> e.clauses_dense(a*b + a + Integer(1))
>>> e.phi
[None, a, b, c, a*b]

B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B)
e.clauses_dense(a*b + a + 1)
e.phi

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]

>>> from sage.all import *
>>> e.monomial(a*b*c)
5
>>> e.phi
[None, a, b, c, a*b, a*b*c]

e.monomial(a*b*c)
e.phi

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]

>>> from sage.all import *
>>> e.monomial(a*b)
4
>>> e.phi
[None, a, b, c, a*b, a*b*c]

e.monomial(a*b)
e.phi

Note

For correctness, this function is cached.

permutations = Cached version of <function CNFEncoder.permutations>[source]
property phi

Map SAT variables to polynomial variables.

EXAMPLES:

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]

>>> from sage.all import *
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> ce = CNFEncoder(DIMACS(), B)
>>> ce.var()
4
>>> ce.phi
[None, a, b, c, None]

from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
B.<a,b,c> = BooleanPolynomialRing()
ce = CNFEncoder(DIMACS(), B)
ce.var()
ce.phi
split_xor(monomial_list, equal_zero)[source]

Split XOR chains into subchains.

INPUT:

  • monomial_list – list of monomials

  • equal_zero – is the constant coefficient zero?

EXAMPLES:

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]]

>>> from sage.all import *
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c', 'd', 'e', 'f',)); (a, b, c, d, e, f,) = B._first_ngens(6)
>>> ce = CNFEncoder(DIMACS(), B, cutting_number=Integer(3))
>>> ce.split_xor([Integer(1),Integer(2),Integer(3),Integer(4),Integer(5),Integer(6)], False)
[[[1, 7], False], [[7, 2, 8], True], [[8, 3, 9], True], [[9, 4, 10], True], [[10, 5, 11], True], [[11, 6], True]]

>>> ce = CNFEncoder(DIMACS(), B, cutting_number=Integer(4))
>>> ce.split_xor([Integer(1),Integer(2),Integer(3),Integer(4),Integer(5),Integer(6)], False)
[[[1, 2, 7], False], [[7, 3, 4, 8], True], [[8, 5, 6], True]]

>>> ce = CNFEncoder(DIMACS(), B, cutting_number=Integer(5))
>>> ce.split_xor([Integer(1),Integer(2),Integer(3),Integer(4),Integer(5),Integer(6)], False)
[[[1, 2, 3, 7], False], [[7, 4, 5, 6], True]]

from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
B.<a,b,c,d,e,f> = BooleanPolynomialRing()
ce = CNFEncoder(DIMACS(), B, cutting_number=3)
ce.split_xor([1,2,3,4,5,6], False)
ce = CNFEncoder(DIMACS(), B, cutting_number=4)
ce.split_xor([1,2,3,4,5,6], False)
ce = CNFEncoder(DIMACS(), B, cutting_number=5)
ce.split_xor([1,2,3,4,5,6], False)
to_polynomial(c)[source]

Convert clause to sage.rings.polynomial.pbori.BooleanPolynomial.

INPUT:

  • c – a clause

EXAMPLES:

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

>>> from sage.all import *
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> fn = tmp_filename()
>>> solver = DIMACS(filename=fn)
>>> e = CNFEncoder(solver, B, max_vars_sparse=Integer(2))
>>> _ = e([a*b + a + Integer(1), a*b+ a + c])
>>> e.to_polynomial( (Integer(1),-Integer(2),Integer(3)) )
a*b*c + a*b + b*c + b

B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B, max_vars_sparse=2)
_ = e([a*b + a + 1, a*b+ a + c])
e.to_polynomial( (1,-2,3) )
var(m=None, decision=None)[source]

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:

  • m – something the new variables maps to, usually a monomial

  • decision – is this variable a decision variable?

EXAMPLES:

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

>>> from sage.all import *
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> ce = CNFEncoder(DIMACS(), B)
>>> ce.var()
4

from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
B.<a,b,c> = BooleanPolynomialRing()
ce = CNFEncoder(DIMACS(), B)
ce.var()
zero_blocks(f)[source]

Divide the zero set of f into blocks.

EXAMPLES:

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(sorted(d.items()) for d in e.zero_blocks(a*b*c))
[[(c, 0)], [(b, 0)], [(a, 0)]]

>>> from sage.all import *
>>> B = BooleanPolynomialRing(names=('a', 'b', 'c',)); (a, b, c,) = B._first_ngens(3)
>>> from sage.sat.converters.polybori import CNFEncoder
>>> from sage.sat.solvers.dimacs import DIMACS
>>> e = CNFEncoder(DIMACS(), B)
>>> sorted(sorted(d.items()) for d in e.zero_blocks(a*b*c))
[[(c, 0)], [(b, 0)], [(a, 0)]]

B.<a,b,c> = BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
e = CNFEncoder(DIMACS(), B)
sorted(sorted(d.items()) for d in e.zero_blocks(a*b*c))

Note

This function is randomised.