Ticket #13851: trac_13851.patch

File trac_13851.patch, 19.4 KB (added by malb, 8 years ago)
  • doc/en/reference/index.rst

    # HG changeset patch
    # User Nathann Cohen <nathann.cohen@gmail.com>
    # Date 1355939247 -3600
    # Node ID 2087c1f53269de3bd104ad19106bcc201b542981
    # Parent  6e1d4bad3c1b2786c2f3b5fd25e872cf6ed96576
    #13851 SAT solving in reference manual
    
    diff --git a/doc/en/reference/index.rst b/doc/en/reference/index.rst
    a b  
    5858   libs
    5959   cryptography
    6060   logic
     61   sat
    6162   combinat/index
    6263   numerical
    6364   probability
  • new file doc/en/reference/sat.rst

    diff --git a/doc/en/reference/sat.rst b/doc/en/reference/sat.rst
    new file mode 100644
    - +  
     1Sat
     2===
     3
     4Sage supports solving clauses in Conjunctive Normal Form (see :wikipedia:`Conjunctive_normal_form`),
     5i.e., SAT solving, via an interface inspired by the usual DIMACS format used in SAT solving
     6[SG09]_. For example, to express that::
     7
     8   x1 OR x2 OR (NOT x3)
     9
     10should be true, we write::
     11
     12   (1, 2, -3)
     13
     14.. WARNING::
     15
     16    Variable indices **must** start at one.
     17
     18Solvers
     19-------
     20
     21Any SAT solver supporting the DIMACS input format is easily interfaced using the
     22:class:`sage.sat.solvers.dimacs.DIMACS` blueprint. Sage ships with pre-written interfaces for *RSat*
     23[RS]_ and *Glucose* [GL]_. Furthermore, Sage provides a C++ interface to the *CryptoMiniSat* [CMS]_ SAT
     24solver which can be used interchangably with DIMACS-based solvers, but also provides advanced
     25features. For this, the optional CryptoMiniSat package must be installed, this can be accomplished
     26by typing::
     27
     28    sage: install_package('cryptominisat') # not tested
     29
     30and by running ``sage -b`` from the shell afterwards to build Sage's CryptoMiniSat extension module.
     31
     32Since by default Sage does not include any SAT solver, we demonstrate key features by instantiating
     33a fake DIMACS-based solver. We start with a trivial example::
     34
     35    (x1 OR x2 OR x3) AND (x1 OR x2 OR (NOT x3))
     36
     37In Sage's notation::
     38
     39    sage: from sage.sat.solvers.dimacs import DIMACS
     40    sage: solver = DIMACS(command="sat-solver")
     41    sage: solver.add_clause( ( 1,  2,  3) )
     42    sage: solver.add_clause( ( 1,  2, -3) )
     43
     44.. NOTE::
     45
     46    :meth:`sage.sat.solvers.dimacs.DIMACS.add_clause` creates new variables when necessary. In
     47    particular, it creates *all* variables up to the given index. Hence, adding a literal involving
     48    the variable 1000 creates up to 1000 internal variables.
     49
     50DIMACS-base solvers can also be used to write DIMACS files::
     51
     52    sage: from sage.sat.solvers.dimacs import DIMACS
     53    sage: fn = tmp_filename()
     54    sage: solver = DIMACS(filename=fn)
     55    sage: solver.add_clause( ( 1,  2,  3) )
     56    sage: solver.add_clause( ( 1,  2, -3) )
     57    sage: _ = solver.write()
     58    sage: for line in open(fn).readlines():
     59    ...      print line,
     60    p cnf 3 2
     61    1 2 3 0
     62    1 2 -3 0
     63
     64These files can then be passed external SAT solvers.
     65
     66We demonstrate solving using CryptoMiniSat::
     67
     68    sage: from sage.sat.solvers import CryptoMiniSat # optional - cryptominisat
     69    sage: cms = CryptoMiniSat()                      # optional - cryptominisat
     70    sage: cms.add_clause((1,2,-3))                   # optional - cryptominisat
     71    sage: cms()                                      # optional - cryptominisat
     72    (None, True, True, False)
     73
     74Details on Specific Solvers
     75^^^^^^^^^^^^^^^^^^^^^^^^^^^
     76
     77.. toctree::
     78   :maxdepth: 1
     79
     80   sage/sat/solvers/dimacs
     81
     82Converters
     83----------
     84
     85Sage supports conversion from Boolean polynomials (also known as Algebraic Normal Form) to
     86Conjunctive Normal Form::
     87
     88    sage: B.<a,b,c> = BooleanPolynomialRing()
     89    sage: from sage.sat.converters.polybori import CNFEncoder
     90    sage: from sage.sat.solvers.dimacs import DIMACS
     91    sage: fn = tmp_filename()
     92    sage: solver = DIMACS(filename=fn)
     93    sage: e = CNFEncoder(solver, B)
     94    sage: e.clauses_sparse(a*b + a + 1)
     95    sage: _ = solver.write()
     96    sage: print open(fn).read()
     97    p cnf 3 2
     98    1 0
     99    -2 0
     100    <BLANKLINE>
     101
     102Details on Specific Converterts
     103^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     104.. toctree::
     105   :maxdepth: 1
     106
     107   sage/sat/converters/polybori
     108
     109Highlevel Interfaces
     110--------------------
     111
     112Sage provides various highlevel functions which make working with Boolean polynomials easier. We
     113construct a very small-scale AES system of equations and pass it to a SAT solver::
     114
     115    sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True)
     116    sage: F,s = sr.polynomial_system()
     117    sage: from sage.sat.boolean_polynomials import solve as solve_sat # optional - cryptominisat
     118    sage: s = solve_sat(F)                                            # optional - cryptominisat
     119    sage: F.subs(s[0])                                                # optional - cryptominisat
     120    Polynomial Sequence with 36 Polynomials in 0 Variables
     121
     122Details on Specific Highlevel Interfaces
     123^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     124.. toctree::
     125   :maxdepth: 1
     126
     127   sage/sat/boolean_polynomials
     128
     129
     130REFERENCES:
     131
     132.. [RS] http://reasoning.cs.ucla.edu/rsat/
     133
     134.. [GL] http://www.lri.fr/~simon/?page=glucose
     135
     136.. [CMS] http://www.msoos.org/cryptominisat2/
     137
     138.. [SG09] http://www.satcompetition.org/2009/format-benchmarks2009.html
  • sage/misc/classcall_metaclass.pyx

    diff --git a/sage/misc/classcall_metaclass.pyx b/sage/misc/classcall_metaclass.pyx
    a b  
    5454     - ``.__classget__`` for customizing the binding behavior in
    5555       ``foo.cls`` (analogue of ``.__get__``).
    5656
    57     See the documentation of :meth:`.__call__` and of :meth:`.__get__`
    58     and :meth:`.__contains__` for the description of the respective
     57    See the documentation of :meth:`__call__` and of :meth:`__get__`
     58    and :meth:`__contains__` for the description of the respective
    5959    protocols.
    6060
    6161    .. warning:: for technical reasons, ``__classcall__``,
  • sage/sat/boolean_polynomials.py

    diff --git a/sage/sat/boolean_polynomials.py b/sage/sat/boolean_polynomials.py
    a b  
    11"""
    2 SAT Functions for Boolean Polynomials.
     2SAT Functions for Boolean Polynomials
     3
     4These highlevel functions support solving and learning from Boolean polynomial systems. In this
     5context, "learning" means the construction of new polynomials in the ideal spanned by the original
     6polynomials.
    37
    48AUTHOR:
    59
    610- Martin Albrecht (2012): initial version
     11
     12Functions
     13^^^^^^^^^
    714"""
    815##############################################################################
    916#  Copyright (C) 2012 Martin Albrecht <martinralbrecht@googlemail.com>
     
    3542
    3643    - ``converter`` - an ANF to CNF converter class or object.  If
    3744      ``converter`` is ``None`` then
    38       :cls:`sage.sat.converters.polybori.CNFEncoder` is used to
     45      :class:`sage.sat.converters.polybori.CNFEncoder` is used to
    3946      construct a new converter. (default: ``None``)
    4047
    4148    - ``solver`` - a SAT-solver class or object. If ``solver`` is
    42       ``None`` then cls:`sage.sat.solvers.cryptominisat.CryptoMiniSat`
     49      ``None`` then :class:`sage.sat.solvers.cryptominisat.CryptoMiniSat`
    4350      is used to construct a new converter.  (default: ``None``)
    4451
    4552    - ``target_variables`` - a list of variables. The elements of the list are
     
    5158      (default: ``None``)
    5259
    5360    - ``**kwds`` - parameters can be passed to the converter and the
    54        solver by prefixing them with 'c_' and 's_' respectively. For
     61       solver by prefixing them with ``c_`` and ``s_`` respectively. For
    5562       example, to increase CryptoMiniSat's verbosity level, pass
    5663       ``s_verbosity=1``.
    5764
     
    7784    This time we pass a few options through to the converter and the solver::
    7885
    7986        sage: s = solve_sat(F, s_verbosity=1, c_max_vars_sparse=4, c_cutting_number=8) # optional - cryptominisat
    80         sage: F.subs(s[0])                                                           # optional - cryptominisat
     87        sage: F.subs(s[0])                                                             # optional - cryptominisat
    8188        Polynomial Sequence with 36 Polynomials in 0 Variables
    8289
    8390    We construct a very simple system with three solutions and ask for a specific number of solutions::
     
    116123        sage: solve_sat(F,n=infinity,target_variables=[a,b])              # optional - cryptominisat
    117124        [{b: 0, a: 0}, {b: 1, a: 1}]
    118125
    119     .. note::
     126    .. NOTE::
    120127
    121128       Although supported, passing converter and solver objects
    122129       instead of classes is discouraged because these objects are
     
    213220
    214221    - ``F`` - a sequence of Boolean polynomials
    215222
    216     - ``converter`` - an ANF to CNF converter class or object.  If
    217       ``converter`` is ``None`` then
    218       :cls:`sage.sat.converters.polybori.CNFEncoder` is used to
    219       construct a new converter. (default: ``None``)
     223    - ``converter`` - an ANF to CNF converter class or object.  If ``converter`` is ``None`` then
     224      :class:`sage.sat.converters.polybori.CNFEncoder` is used to construct a new
     225      converter. (default: ``None``)
    220226
    221     - ``solver`` - a SAT-solver class or object. If ``solver`` is
    222       ``None`` then cls:`sage.sat.solvers.cryptominisat.CryptoMiniSat`
    223       is used to construct a new converter.  (default: ``None``)
     227    - ``solver`` - a SAT-solver class or object. If ``solver`` is ``None`` then
     228      :class:`sage.sat.solvers.cryptominisat.CryptoMiniSat` is used to construct a new converter.
     229      (default: ``None``)
    224230
    225     - ``max_learnt_length`` - only clauses of length <=
    226       ``max_length_learnt`` are considered and converted to
    227       polynomials. (default: ``3``)
     231    - ``max_learnt_length`` - only clauses of length <= ``max_length_learnt`` are considered and
     232      converted to polynomials. (default: ``3``)
    228233
    229     - ``interreduction`` - inter-reduce the resulting polynomials
    230       (default: ``False``)
     234    - ``interreduction`` - inter-reduce the resulting polynomials (default: ``False``)
    231235
    232     - ``**kwds`` - parameters can be passed to the converter and the
    233        solver by prefixing them with 'c_' and 's_' respectively. For
    234        example, to increase CryptoMiniSat's verbosity level, pass
     236    .. NOTE::
     237
     238       More parameters can be passed to the converter and the solver by prefixing them with ``c_`` and
     239       ``s_`` respectively. For example, to increase CryptoMiniSat's verbosity level, pass
    235240       ``s_verbosity=1``.
    236241
    237242    OUTPUT:
     
    259264       sage: F,s = sr.polynomial_system()                 # optional - cryptominisat
    260265       sage: from sage.sat.boolean_polynomials import learn as learn_sat # optional - cryptominisat
    261266       sage: H = learn_sat(F, s_maxrestarts=20, interreduction=True)     # optional - cryptominisat
    262        sage: H[-1]                                        # optional - cryptominisat
     267       sage: H[-1]                                        # optional - cryptominisat, output random
    263268       k001200*s031*x011201 + k001200*x011201
    264269
    265     .. note::
     270    .. NOTE::
    266271
    267272       This function is meant to be called with some parameter such
    268273       that the SAT-solver is interrupted. For CryptoMiniSat this is
  • sage/sat/converters/polybori.py

    diff --git a/sage/sat/converters/polybori.py b/sage/sat/converters/polybori.py
    a b  
    11"""
    2 ANF to CNF Converter.
     2An ANF to CNF Converter using a Dense/Sparse Strategy
     3
     4This converter is based on two converters. The first one, by Martin Albrecht, was based on [CB07]_,
     5this is the basis of the "dense" part of the converter. It was later improved by Mate Soos. The
     6second one, by Michael Brickenstein, uses a reduced truth table based approach and forms the
     7"sparse" part of the converter.
    38
    49AUTHORS:
    510
     
    712- Michael Brickenstein - (2009) 'cnf.py' for PolyBoRi
    813- Mate Soos - (2010) improved version of 'anf2cnf.py'
    914- Martin Albrecht - (2012) unified and added to Sage
     15
     16REFERENCES:
     17
     18.. [CB07] Nicolas Courtois, Gregory V. Bard: Algebraic Cryptanalysis of the Data Encryption
     19   Standard, In 11-th IMA Conference, Cirencester, UK, 18-20 December 2007, Springer LNCS 4887. See
     20   also http://eprint.iacr.org/2006/402/.
     21
     22Classes and Methods
     23-------------------
    1024"""
    1125
    1226##############################################################################
     
    2943
    3044class CNFEncoder(ANF2CNFConverter):
    3145    """
    32     ANF to CNF Converter.
     46    ANF to CNF Converter using a Dense/Sparse Strategy. This converter distinguishes two classes of
     47    polynomials.
     48
     49    1. Sparse polynomials are those with at most ``max_vars_sparse`` variables. Those are converted
     50    using reduced truth-tables based on PolyBoRi's internal representation.
     51
     52    2. Polynomials with more variables are converted by introducing new variables for monomials and
     53    by converting these linearised polynomials.
     54
     55    Linearised polynomials are converted either by splitting XOR chains -- into chunks of length
     56    ``cutting_number`` -- or by constructing XOR clauses if the underlying solver supports it. This
     57    behaviour is disabled by passing ``use_xor_clauses=False``.
     58
     59    .. automethod:: __init__
     60    .. automethod:: __call__
    3361    """
    3462    def __init__(self, solver, ring, max_vars_sparse=6, use_xor_clauses=None, cutting_number=6, random_seed=16):
    3563        """
    3664        Construct ANF to CNF converter over ``ring`` passing clauses to ``solver``.
    3765
    38         This converter distinguishes two classes of
    39         polynomials.
    40 
    41         1. Sparse polynomials are those with at most ``max_vars_sparse``
    42         variables. Those are converted using reduced truth-tables
    43         based on PolyBoRi's internal representation.
    44 
    45         2. Polynomials with more variables are converted by
    46         introducing new variables for monomials and by converting
    47         these linearised polynomials.
    48 
    49         Linearised polynomials are converted either by splitting XOR
    50         chains -- into chunks of length ``cutting_number`` -- or by
    51         constructing XOR clauses if the underlying solver supports
    52         it. This behaviour is disabled by passing
    53         ``use_xor_clauses=False``.
    54 
    5566        INPUT:
    5667
    5768        - ``solver`` - a SAT-solver instance
    5869
    59         - ``ring`` - a :cls:`BooleanPolynomialRing`
     70        - ``ring`` - a :class:`sage.rins.polynomial.pbori.BooleanPolynomialRing`
    6071
    6172        - ``max_vars_sparse`` - maximum number of variables for direct conversion
    6273
     
    108119            sage: e.phi
    109120            [None, a, b, c, a*b]
    110121
    111         .. note::
     122        .. NOTE::
    112123
    113             This constructer generates SAT variables for each Boolean
    114             polynomial variable.
    115 
     124            This constructer generates SAT variables for each Boolean polynomial variable.
    116125        """
    117126        self.random_generator = Random(random_seed)
    118127        self.one_set = ring.one().set()
     
    250259
    251260        INPUT:
    252261
    253         - ``f`` - a :cls:`BooleanPolynomial`
     262        - ``f`` - a :class:`sage.rings.polynomial.pbori.BooleanPolynomial`
    254263
    255264
    256265        EXAMPLE::
     
    296305
    297306        INPUT:
    298307
    299         - ``f`` - a :cls:`BooleanPolynomial`
     308        - ``f`` - a :class:`sage.rings.polynomial.pbori.BooleanPolynomial`
    300309
    301310        EXAMPLE::
    302311
     
    434443
    435444    def split_xor(self, monomial_list, equal_zero):
    436445        """
     446        Split XOR chains into subchains.
     447
    437448        INPUT:
    438449
    439450        - ``monomial_list`` - a list of monomials
     
    478489
    479490    def clauses(self, f):
    480491        """
    481         Convert ``f`` using the sparse strategy if f.nvariables() is
     492        Convert ``f`` using the sparse strategy if ``f.nvariables()`` is
    482493        at most ``max_vars_sparse`` and the dense strategy otherwise.
    483494
    484495        INPUT:
    485496
    486         - ``f`` - a :cls:`BooleanPolynomial`
     497        - ``f`` - a :class:`sage.rings.polynomial.pbori.BooleanPolynomial`
    487498
    488499        EXAMPLE::
    489500
     
    534545
    535546        INPUT:
    536547
    537         - ``F`` - an iterable of Boolean polynomials
     548        - ``F`` - an iterable of :class:`sage.rings.polynomial.pbori.BooleanPolynomial`
    538549
    539550        OUTPUT: An inverse map int -> variable
    540551
     
    576587
    577588    def to_polynomial(self, c):
    578589        """
    579         Convert clause to :cls:`BooleanPolynomial`
     590        Convert clause to :class:`sage.rings.polynomial.pbori.BooleanPolynomial`
    580591
    581592        INPUT:
    582593
  • sage/sat/solvers/cryptominisat/cryptominisat.pyx

    diff --git a/sage/sat/solvers/cryptominisat/cryptominisat.pyx b/sage/sat/solvers/cryptominisat/cryptominisat.pyx
    a b  
    354354            sage: F,s = sr.polynomial_system()                        # optional - cryptominisat
    355355            sage: cms = CryptoMiniSat()                               # optional - cryptominisat
    356356            sage: phi = CNFEncoder(cms, F.ring())(F)                  # optional - cryptominisat
    357             sage: cms( range(1,80) )                                  # optional - cryptominisat
     357            sage: cms( range(1,120) )                                 # optional - cryptominisat
    358358            False
    359359
    360360        This guess was wrong and we need to flip one of the following variables::
    361361
    362             sage: cms.conflict_clause()                                    # optional - cryptominisat
    363             (-72, -71, -70, -69)
     362            sage: cms.conflict_clause()                               # optional - cryptominisat
     363            (-119, -118, -117, -116, -114, -113, -112, -110, -109, -100, -98, -97, -96, -94, -93, -92, -91, -76, -75, -71, -70, -69)
    364364        """
    365365        cdef Lit l
    366366        r = []
     
    387387            sage: cms = CryptoMiniSat(maxrestarts=10,verbosity=0)     # optional - cryptominisat
    388388            sage: phi = CNFEncoder(cms, F.ring())(F)                  # optional - cryptominisat
    389389            sage: cms()                                               # optional - cryptominisat
    390             sage: sorted(cms.learnt_clauses())[0]                     # optional - cryptominisat
     390            sage: sorted(cms.learnt_clauses())[0]                     # optional - cryptominisat, output random
    391391            (-592, -578, -68, 588, 94, 579, 584, 583)
    392392
    393393
  • sage/sat/solvers/dimacs.py

    diff --git a/sage/sat/solvers/dimacs.py b/sage/sat/solvers/dimacs.py
    a b  
    11"""
    2 SAT-Solvers via DIMACS Files.
     2SAT-Solvers via DIMACS Files
    33
    4 Sage supports calling SAT solvers using the popular DIMACS
    5 format. This module implements infrastructure to make it easy to add
    6 new such interfaces and some example interfaces.
     4Sage supports calling SAT solvers using the popular DIMACS format. This module implements
     5infrastructure to make it easy to add new such interfaces and some example interfaces.
    76
    8 Currently, RSat and Glucose are included.
     7Currently, interfaces to **RSat** [RS]_ and **Glucose** [GL]_ are included by default.
    98
    109.. note::
    1110
    12     Our SAT solver interfaces are 1-based, i.e., literals start at
    13     1. This is consistent with the popular DIMACS format for SAT
    14     solving but not with Pythion's 0-based convention. However, this
     11    Our SAT solver interfaces are 1-based, i.e., literals start at 1. This is consistent with the
     12    popular DIMACS format for SAT solving but not with Pythion's 0-based convention. However, this
    1513    also allows to construct clauses using simple integers.
    1614
    1715AUTHORS:
    1816
    1917- Martin Albrecht (2012): first version
     18
     19Classes and Methods
     20-------------------
    2021"""
    2122##############################################################################
    2223#  Copyright (C) 2012 Martin Albrecht <martinralbrecht@googlemail.com>
     
    3839    .. note::
    3940
    4041        Usually, users won't have to use this class directly but some
    41         class which inherits from thsi class.
     42        class which inherits from this class.
     43
     44    .. automethod:: __init__
     45    .. automethod:: __call__
    4246    """
    4347
    4448    command = ""