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.
