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