Hi, Oh, thanks for that ticket. I put it on my backlog to fix. The issue is, I have no idea how many people use this thing and it takes time to fix :S In the meanwhile, I am interested in your feedback on this (not yet publicized) ANF simplifier and ANF-to-CNF converter:
https://github.com/meelgroup/bosphorus It takes in an ANF, spits out a simplified ANF and a simplified CNF, plus solves it using an external SAT solver if available. It uses a bunch of cool tricks to get a simplified ANF and CNF. In particular, it uses ElimLin, XL, ANF propagation, variable replacement, and Karnaugh tables. Check it out :) Mate On Monday, 17 December 2018 19:42:57 UTC+1, Jörg-Volker wrote: > > Hi, > > just want to add that the equation system in my example definitly has a > solution. I boiled it down from a much bigger system. > > Meanwhile I found a ticket in sage-trac dealing with this bug in the > binding of CryptoMiniSat (src/sage/sat/solvers/cryptominisat.py) to > SageMath, see https://trac.sagemath.org/ticket/26676. > <https://trac.sagemath.org/ticket/26676> > > -- 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.
