Once I got cryptominisat installed, I was able to replicate the bug. I also rearranged the equations and got it to solve as well, without rearranging the order of the variables.
Sent from my iPhone > On Dec 13, 2018, at 11:58 AM, Sébastien Labbé <sla...@gmail.com> wrote: > > I tested cryptominisat, picosat and glucose. Glucose (added as a optional or > experimental package in https://trac.sagemath.org/ticket/26361) finds a > solution in the first case. In the second case (variables in reverse order), > all of them finds something. > > My experiments are copied below. > > sage: varl = ['k{0}'.format(p) for p in range(29)] > ....: > ....: B = BooleanPolynomialRing(names = varl) > ....: B.inject_variables(verbose=False) > ....: > ....: keqs = [ > ....: k0 + k6 + 1, > ....: k3 + k9 + 1, > ....: k5*k18 + k6*k18 + k7*k16 + k7*k10, > ....: k9*k17 + k8*k24 + k11*k17, > ....: k1*k13 + k1*k15 + k2*k12 + k3*k15 + k4*k14, > ....: k5*k18 + k6*k16 + k7*k18, > ....: k3 + k26, > ....: k0 + k19, > ....: k9 + k28, > ....: k11 + k20] > ....: > ....: from sage.sat.boolean_polynomials import solve as solve_sat > ....: > sage: solve_sat(keqs, n=1) > False > sage: solve_sat(keqs, n=1, solver=SAT('picosat')) > False > sage: solve_sat(keqs, n=1, solver=SAT('glucose')) > [{k28: 1, > k26: 0, > k24: 0, > k20: 0, > k19: 1, > k18: 0, > k17: 0, > k16: 0, > k15: 1, > k14: 1, > k13: 0, > k12: 1, > k11: 0, > k10: 0, > k9: 1, > k8: 0, > k7: 0, > k6: 0, > k5: 0, > k4: 0, > k3: 0, > k2: 0, > k1: 0, > k0: 1}] > > > > > sage: varl = ['k{0}'.format(p) for p in range(28, -1, -1)] > sage: B = BooleanPolynomialRing(names = varl) > ....: B.inject_variables(verbose=False) > ....: > ....: keqs = [ > ....: k0 + k6 + 1, > ....: k3 + k9 + 1, > ....: k5*k18 + k6*k18 + k7*k16 + k7*k10, > ....: k9*k17 + k8*k24 + k11*k17, > ....: k1*k13 + k1*k15 + k2*k12 + k3*k15 + k4*k14, > ....: k5*k18 + k6*k16 + k7*k18, > ....: k3 + k26, > ....: k0 + k19, > ....: k9 + k28, > ....: k11 + k20] > ....: > sage: > sage: solve_sat(keqs, n=1, solver=SAT('cryptominisat')) > [{k0: 1, > k1: 0, > k2: 0, > k3: 0, > k4: 0, > k5: 0, > k6: 0, > k7: 0, > k8: 0, > k9: 1, > k10: 0, > k11: 0, > k12: 0, > k13: 0, > k14: 0, > k15: 0, > k16: 0, > k17: 0, > k18: 0, > k19: 1, > k20: 0, > k24: 0, > k26: 0, > k28: 1}] > sage: solve_sat(keqs, n=1, solver=SAT('picosat')) > [{k0: 0, > k1: 0, > k2: 0, > k3: 1, > k4: 1, > k5: 0, > k6: 1, > k7: 0, > k8: 0, > k9: 0, > k10: 0, > k11: 0, > k12: 1, > k13: 1, > k14: 1, > k15: 1, > k16: 0, > k17: 0, > k18: 0, > k19: 0, > k20: 0, > k24: 0, > k26: 1, > k28: 0}] > sage: solve_sat(keqs, n=1, solver=SAT('glucose')) > [{k0: 1, > k1: 1, > k2: 1, > k3: 1, > k4: 0, > k5: 0, > k6: 0, > k7: 0, > k8: 0, > k9: 0, > k10: 0, > k11: 0, > k12: 0, > k13: 0, > k14: 1, > k15: 1, > k16: 0, > k17: 0, > k18: 0, > k19: 1, > k20: 0, > k24: 0, > k26: 1, > k28: 0}] > > > -- > You received this message because you are subscribed to the Google Groups > "sage-devel" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sage-devel+unsubscr...@googlegroups.com. > To post to this group, send email to sage-devel@googlegroups.com. > Visit this group at https://groups.google.com/group/sage-devel. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at https://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
