Hi, SAT solvers are very handy for quick problem solving.
cryptominisat was stuck at version 2.9.6 since git migration, and was tagged as an experimental package since it did not build on 32bit systems. I updated it to latest version (5.0.1), which involved some changes: - the build now relies on cmake, which had to be updated and seems now fully functional. OSX users, please test it so that it could move from experimental to optional. Note that cmake might be used in a near future for things like CGAL or csympy/symengine. - the cryptominisat(2) Cython interface is not working anymore, hence was replaced with upstream basic python bindings. We lose some fine tuning options and features (like the posibility to learn clauses from the solver), but we now have an easy-to-maintain package which implements recent progress in the domain, including parallelism, and we could request missing features upstream if needed (they were not really used within Sage). The whole stuff needs review at #22817 and #22818 (cmake is merged already). Testers (in particular OSX) are welcome. Ciao, Thierry -- 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.
