Hot-keys on this page
r m x p toggle line displays
j k next/prev highlighted chunk
0 (zero) top of page
1 (one) first highlighted chunk
""" 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 ------------------- """
############################################################################## # Copyright (C) 2008-2009 Martin Albrecht <martinralbrecht@googlemail.com> # Copyright (C) 2009 Michael Brickenstein <brickenstein@mfo.de> # Copyright (C) 2010 Mate Soos # Copyright (C) 2012 Martin Albrecht <martinralbrecht@googlemail.com> # Distributed under the terms of the GNU General Public License (GPL) # The full text of the GPL is available at: # http://www.gnu.org/licenses/ ##############################################################################
""" 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``.
.. automethod:: __init__ .. automethod:: __call__ """ """ Construct ANF to CNF converter over ``ring`` passing clauses to ``solver``.
INPUT:
- ``solver`` - a SAT-solver instance
- ``ring`` - a :class:`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 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 constructor generates SAT variables for each Boolean polynomial variable. """
# If you change this, make sure we are calling m.index() # below, as this relies on phi being sorted like this.
""" 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 """
def phi(self): """ 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] """
################################################## # Encoding based on polynomial roots ##################################################
""" Divides 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(e.zero_blocks(a*b*c)) [{c: 0}, {b: 0}, {a: 0}]
.. note::
This function is randomised. """
else:
else:
""" Convert ``f`` using the sparse strategy.
INPUT:
- ``f`` - a :class:`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 1 0 -2 0 sage: e.phi [None, a, b, c] """ # we form an expression for a var configuration *not* lying in # the block it is evaluated to 0 by f, iff it is not lying in # any zero block of f+1
################################################### # Indirect conversion, may add new variables ###################################################
""" Convert ``f`` using the dense strategy.
INPUT:
- ``f`` - a :class:`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] """
self.solver.add_xor_clause(f, rhs=not equal_zero) else: ll = len(f) for p in self.permutations(ll, equal_zero): self.solver.add_clause([ p[i]*f[i] for i in range(ll) ])
def monomial(self, m): """ 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]
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. """ else: # we need to encode the relationship between the monomial # and its variables
# (a | -w) & (b | -w) & (w | -a | -b) <=> w == a*b
def permutations(length, equal_zero): """ 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:
- ``length`` - the number of variables - ``equal_zero`` - should the sum be equal to zero?
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.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]] """
""" Split XOR chains into subchains.
INPUT:
- ``monomial_list`` - a 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]] """
################################################### # Highlevel Functions ###################################################
""" Convert ``f`` using the sparse strategy if ``f.nvariables()`` is at most ``max_vars_sparse`` and the dense strategy otherwise.
INPUT:
- ``f`` - a :class:`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 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] """ else:
""" Encode the boolean polynomials in ``F`` .
INPUT:
- ``F`` - an iterable of :class:`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 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] """
#################################################### # Highlevel Functions ###################################################
""" Convert clause to :class:`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 """ # order of these multiplications for performance res = l[0] for p in l[1:]: res = res*p return res
raise ValueError("clause contains an XOR glueing variable") |