Hi Mate, On Wednesday, December 12, 2018 at 10:39:02 PM UTC+1, Mate Soos wrote: > > 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. > Yes, the function solve_sat() returns a list of python dictionaries, each containing a solution. In the example I explicitly asked for only one solution so the list contains just one dictionary.
2) If the equations are entered in a different way, the system runs > forever, and cannot find a solution within some cutoff. > No the equations are exactly the same but the list with the variables implictly handed over to the function solve_sat() have another order. The strings in list varl are used to define the generators of the Boolean polynomial ring B. The re-ordering of the generators makes the function solve_sat() failing to return a solution. It returns False. I don't think this is the fault of CryptoMiniSat. There may be a failure in the integration into sagemath which has changed since version 8 of sagemath. It now uses the Python interface of CMS and is implemented in sage.git-8.4/src/sage/sat/solvers/cryptominisat.py. > 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. > See my answer to point 2). 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 > I hope to see it soon in sagemath ;-) Regards, 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+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.
