OK, so I need to understand this a bit more and need a bit of hand-holding.
The issue as far as I understand is the following:
1) If the equations are entered in one way, the solution is found. Solution
is SATISFIABLE and the solution is output to console.
2) If the equations are entered in a different way, the system runs
forever, and cannot find a solution within some cutoff.
Is this correct? If it is, this could be caused by a number of issues, most
notably, the solver can get "lost" in the search space. The newer version
5.6.3+ are *significantly* better at this, but it still happens and will
always happen until we do some more research into variable branching
heuristics. Essentially, solving is kind of random -- if you give the same
seed and the same set of inputs, it will do the same thing. Otherwise, it
will do something different, and it might get lost in the bushes. This is
not just true of CryptoMinSat, this is true for all solvers.
Now, for the good news. I have been working *really* hard (damn, years...),
along with a bunch of very talented, and even harder working people from
DSO National Laboratories Singapore and Kuldeep Meel from National
University of Singapore to create an ANF solver that is quite amazing, and
should beat everything out there. It uses a SAT solver at the bottom, but
also adds a million other things to make sure we solve instances faster (we
are talking thousands of lines of code). The paper will be presented at
DATE 2019. I will give an update to this thread in the next week with all
the details, including code and paper PDF. I am not saying this will solve
this particular instance faster (though I sincerely hope it will). But it
will certainly improve solving problems like this by a good margin. The
input to this solver is basically:
x1+x2*x3 =1
x3*x1*x3 =1
[etc]
which unexpectedly corresponds to how polybori will output equations for
you when you ask it to dump to text :)
Mate
On Wednesday, 12 December 2018 22:24:20 UTC+1, Steven Craighead wrote:
>
> Mate Soos, I have Sage installed in both Linux Mint 19 and also installed
> on a Mac Book.
>
> My Linux install wouldn’t install cryptominisat, but I was able to install
> it on my Mac book with no issues. So I was able to duplicate the error
> raised by
>
> Jörg-Volker below.
>>>
>>
> I was curious why the equation order led to different situations and think
> that this due to a need to place a partial order on the equations before
> attempting to solve them.
>
> Is that true, Mate?
> Sent from my iPad
>
> On Dec 12, 2018, at 12:05 PM, Mate Soos <soos...@gmail.com <javascript:>>
> wrote:
>
> Hey,
>
> I'm the author of CryptoMinISat :) Let me know what the issue is and I
> will debug :) Please explain what you tried doing, what failed and what you
> think the problem might be. I'll try to help to the best of my ability and
> time!
>
> Cheers,
>
> Mate
>
> On Monday, 10 December 2018 02:52:45 UTC+1, Steven Craighead wrote:
>>
>> I'm trying to install cryptominisat for SAGEMATH 8.4. I'm hitting a
>> wall. Any advice?
>>
>> On Sun, Dec 9, 2018 at 10:20 AM Steven Craighead <steven.c...@gmail.com>
>> wrote:
>>
>>> Equations three through six in keqs are nonlinear. I would expect if
>>> you left the var1 order alone and permuted the order of the equations you
>>> might even get different answers.
>>>
>>> For instance if you swapped equation one with equation nine, you might
>>> get the same answer with the standard order on var1 that you are getting
>>> with your reversed order on var1.
>>>
>>> Sent from my iPad
>>>
>>> On Dec 9, 2018, at 8:46 AM, Jörg-Volker <jvp...@gmail.com> wrote:
>>>
>>> Just a reminder that there's still a bug in the communication with the
>>> experimental package CryptoMiniSat 5.0.1 when used via the function
>>> sage.sat.boolean_polynomials.solve().
>>> In the following example no solution of the boolean equation system is
>>> not found:
>>>
>>> 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
>>>
>>> kpsol = solve_sat(keqs, n=1)
>>>
>>> print type(kpsol)
>>> print len(kpsol)
>>>
>>> Changing the first statement to
>>>
>>> varl = ['k{0}'.format(p) for p in range(28, -1, -1)]
>>>
>>> which just re-orders the generators, a solution can be found.
>>> Any ideas?
>>>
>>> Jörg-Volker.
>>>
>>> --
>>> 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+...@googlegroups.com.
>>> To post to this group, send email to sage-...@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+...@googlegroups.com <javascript:>.
> To post to this group, send email to sage-...@googlegroups.com
> <javascript:>.
> 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.
