Ticket #13850: 13850_boolean_solve.patch

File 13850_boolean_solve.patch, 8.8 KB (added by Bouillaguet, 7 years ago)
  • sage/rings/polynomial/multi_polynomial_sequence.py

    # HG changeset patch
    # User Charles Bouillaguet <charles.bouillaguet@lifl.fr>
    # Date 1358721706 -3600
    # Node ID 197a347c4f3d9d338be97a2a9cf6cb66c5706f4b
    # Parent  6e750a54fb1e8897880c642d7743689a49c7791c
    Trac #13850: implement a generic interface for boolean polynomial solving
    
    diff --git a/sage/rings/polynomial/multi_polynomial_sequence.py b/sage/rings/polynomial/multi_polynomial_sequence.py
    a b  
    1717- Martin Albrecht (2009): refactoring, clean-up, new functions
    1818- Martin Albrecht (2011): refactoring, moved to sage.rings.polynomial
    1919- Alex Raichev (2011-06): added algebraic_dependence()
     20- Charles Bouillaguet (2013-1): added solve()
    2021
    2122EXAMPLES:
    2223
     
    140141    sage: loads(dumps(F)) == F
    141142    True
    142143
    143 .. note::
     144.. NOTE::
    144145
    145146   In many other computer algebra systems (cf. Singular) this class
    146147   would be called ``Ideal`` but an ideal is a very distinct object
     
    156157"""
    157158
    158159from types import GeneratorType
     160from sage.misc.package import is_package_installed
    159161
    160 from sage.structure.sequence import Sequence_generic
     162from sage.structure.sequence import Sequence, Sequence_generic
    161163
    162164from sage.rings.infinity import Infinity
     165from sage.rings.finite_rings.constructor import FiniteField as GF
    163166from sage.rings.polynomial.multi_polynomial_ring import is_MPolynomialRing
    164167from sage.rings.quotient_ring import is_QuotientRing
    165168from sage.rings.quotient_ring_element import QuotientRingElement
    166169from sage.rings.polynomial.multi_polynomial_ideal import MPolynomialIdeal
    167170from sage.rings.polynomial.multi_polynomial import is_MPolynomial
    168171from sage.rings.polynomial.polynomial_ring_constructor import PolynomialRing
     172from sage.rings.polynomial.pbori import BooleanPolynomialRing
    169173
    170174from sage.interfaces.singular import singular
    171175
     
    10231027        """
    10241028        from polybori import gauss_on_polys
    10251029        from polybori.ll import eliminate,ll_encode,ll_red_nf_redsb
    1026         from sage.rings.polynomial.pbori import BooleanPolynomialRing
    1027        
     1030
    10281031        R = self.ring()
    10291032
    10301033        if not isinstance(R, BooleanPolynomialRing):
     
    11021105        """
    11031106        R = self.ring()
    11041107
    1105         from sage.rings.polynomial.pbori import BooleanPolynomialRing
    1106 
    11071108        if not isinstance(R, BooleanPolynomialRing):
    11081109            from sage.libs.singular.groebner_strategy import GroebnerStrategy
    11091110            return GroebnerStrategy(self.ideal())
     
    11151116            g.reduction_strategy.opt_red_tail=True
    11161117            return g
    11171118
     1119    def solve(self, algorithm='polybori', n=1,  eliminate_linear_variables=True, verbose=False, **kwds):
     1120        r"""
     1121        Find solutions of this boolean polynomial system.
     1122
     1123        This function provide a unified interface to several algorithms
     1124        dedicated to solving systems of boolean equations. Depending on
     1125        the particular nature of the system, some might be much faster
     1126        than some others.
     1127
     1128        INPUT:
     1129
     1130        * ``self`` - a sequence of boolean polynomials
     1131
     1132        * ``algorithm`` - the method to use. Possible values are
     1133          ``polybori``, ``sat`` and ``exhaustive_search``. (default:
     1134          ``polybori``, since it is always available)
     1135
     1136        * ``n`` - number of solutions to return. If ``n == +Infinity``
     1137          then all solutions are returned. If `n < \infty` then `n`
     1138          solutions are returned if the equations have at least `n`
     1139          solutions. Otherwise, all the solutions are
     1140          returned. (default: ``1``)
     1141
     1142        * ``eliminate_linear_variables`` - whether to eliminate
     1143          variables that appear linearly. This reduces the number of
     1144          variables (makes solving faster a priori), but is likely to
     1145          make the equations denser (may make solving slower depending
     1146          on the method).
     1147
     1148        * ``verbose`` - whether to display progress and (potentially)
     1149          useful information while the computation runs. (default:
     1150          ``False``)
     1151
     1152        EXAMPLES:
     1153
     1154        Without argument, a single arbitrary solution is returned::
     1155
     1156            sage: R.<x,y,z> = BooleanPolynomialRing()
     1157            sage: S = Sequence([x*y+z, y*z+x, x+y+z+1])
     1158            sage: sol = S.solve(); sol                       # random
     1159            [{y: 1, z: 0, x: 0}]
     1160
     1161        We check that it is actually a solution::
     1162
     1163            sage: S.subs( sol[0] )
     1164            [0, 0, 0]
     1165
     1166        We obtain all solutions::
     1167
     1168            sage: sols = S.solve(n=Infinity); sols           # random
     1169            [{x: 0, y: 1, z: 0}, {x: 1, y: 1, z: 1}]
     1170            sage: map( lambda x: S.subs(x), sols)
     1171            [[0, 0, 0], [0, 0, 0]]
     1172
     1173        We can force the use of exhaustive search if the optional
     1174        package ``FES`` is present::
     1175
     1176            sage: sol = S.solve(algorithm='exhaustive_search'); sol  # random, optional - needs FES
     1177            [{x: 1, y: 1, z: 1}]
     1178            sage: S.subs( sol[0] )
     1179            [0, 0, 0]
     1180
     1181        And we may use SAT-solvers if they are available::
     1182
     1183            sage: sol = S.solve(algorithm='sat'); sol                     # random, optional - needs CryptoMiniSat
     1184            [{y: 1, z: 0, x: 0}]
     1185            sage: S.subs( sol[0] )
     1186            [0, 0, 0]
     1187
     1188        TESTS:
     1189
     1190        Make sure that variables not occuring in the equations are no problem::
     1191
     1192            sage: R.<x,y,z,t> = BooleanPolynomialRing()
     1193            sage: S = Sequence([x*y+z, y*z+x, x+y+z+1])
     1194            sage: sols = S.solve(n=Infinity)
     1195            sage: map( lambda x: S.subs(x), sols)
     1196            [[0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0]]
     1197
     1198        Not eliminating linear variables::
     1199
     1200            sage: sols = S.solve(n=Infinity, eliminate_linear_variables=False)
     1201            sage: map( lambda x: S.subs(x), sols)
     1202            [[0, 0, 0], [0, 0, 0], [0, 0, 0], [0, 0, 0]]
     1203
     1204        A tricky case where the linear equations are insatisfiable::
     1205
     1206            sage: R.<x,y,z> = BooleanPolynomialRing()
     1207            sage: S = Sequence([x*y*z+x*y+z*y+x*z, x+y+z+1, x+y+z])
     1208            sage: S.solve()
     1209            []
     1210
     1211        """
     1212        from sage.modules.free_module import VectorSpace
     1213
     1214        S = self
     1215        R_origin = R_solving = self.ring()
     1216        reductors = []
     1217
     1218        if eliminate_linear_variables:
     1219            T, reductors = self.eliminate_linear_variables(return_reductors=True)
     1220            if T.variables() != ():
     1221                R_solving = BooleanPolynomialRing( T.nvariables(), map(str, list(T.variables())) )
     1222            S = PolynomialSequence( R_solving, [ R_solving(f) for f in T] )
     1223
     1224        if S != []:
     1225            if algorithm == "exhaustive_search":
     1226                if not is_package_installed('fes'):
     1227                    raise ValueError('algorithm=exhaustive_search requires the optional library FES. Run "install_package(\'fes\')" to install it.')
     1228                from sage.libs.fes import exhaustive_search
     1229                solutions = exhaustive_search(S, max_sols=n, verbose=verbose, **kwds)
     1230
     1231            elif algorithm == "polybori":
     1232                I = S.ideal()
     1233                if verbose:
     1234                    I.groebner_basis(full_prot=True, **kwds)
     1235                else:
     1236                    I.groebner_basis(**kwds)
     1237                solutions = I.variety()
     1238                if len(solutions) >= n:
     1239                    solutions = solutions[:n]
     1240
     1241            elif algorithm == "sat":
     1242                from sage.sat.boolean_polynomials import solve as solve_sat
     1243                if verbose:
     1244                    solutions = solve_sat(S, n=n, s_verbosity=1, **kwds)
     1245                else:
     1246                    solutions = solve_sat(S, n=n, **kwds)
     1247            else:
     1248                raise ValueError("unknown 'algorithm' value")
     1249        else:
     1250            solutions = []
     1251
     1252        if S.variables() == ():
     1253            solved_variables = set()
     1254        else:
     1255            solved_variables = { R_origin(x).lm() for x in R_solving.gens() }
     1256        eliminated_variables = { f.lex_lead() for f in reductors }
     1257        leftover_variables = { x.lm() for x in R_origin.gens() } - solved_variables - eliminated_variables
     1258
     1259        if leftover_variables != set():
     1260            partial_solutions = solutions
     1261            solutions = []
     1262            for sol in partial_solutions:
     1263                for v in VectorSpace( GF(2), len(leftover_variables) ):
     1264                    new_solution = sol.copy()
     1265                    for var,val in zip(leftover_variables, v):
     1266                        new_solution[ var ] = val
     1267                    solutions.append( new_solution )
     1268
     1269        for r in reductors:
     1270            for sol in solutions:
     1271                sol[ r.lm() ] = r.subs(sol).constant_coefficient()
     1272
     1273        return solutions
     1274
     1275
     1276
     1277
    11181278class PolynomialSequence_gf2e(PolynomialSequence_generic):
    11191279    """
    11201280    PolynomialSequence over `\mathbb{F}_{2^e}`, i.e extensions over