#15674: Update cryptominisat (optional package) from CryptoMiniSat version 
2.9.6 to
version 3+
-------------------------------------+-------------------------------------
       Reporter:  equaeghe           |        Owner:
           Type:  enhancement        |       Status:  new
       Priority:  minor              |    Milestone:  sage-6.1
      Component:  packages:          |   Resolution:
  optional                           |    Merged in:
       Keywords:                     |    Reviewers:
        Authors:                     |  Work issues:
Report Upstream:  N/A                |       Commit:
         Branch:                     |  a19676ff338523cb17e9f46f3797e48baf562683
  u/malb/ticket-15674-cryptominisat  |     Stopgaps:
   Dependencies:                     |
-------------------------------------+-------------------------------------

Comment (by msoos):

 I'm the author of CryptoMiniSat. The 3.x series doesn't support XOR
 naively. It should be much faster on many instances, though, and has
 substantially improved in stability and with 3.4 a much cleaner interface
 too. I am planning on a python interface, too for 3.4 which should make
 things drag-and-drop from your perspective. See
 https://github.com/netom/satispy for an example.

 As a library, 3.x it doesn't need boost, zlib, mysql or m4ri, but needs
 C++11. It's 2014, so it's been 3 years now, I hope that's okay :S C++11
 substantially increases portability due to uint32_t/uint64_t and threads
 being part of C++11, not to mention the readability of the code. As for
 cmake, I think I'll make a simple automake version as well. I'll update
 this ticket when 3.4 is released.

 BTW, 3.x supports DRUP (http://www.cs.utexas.edu/~marijn/drup/), which
 means UNSAT can be verified(!) and potentially traced back to the exact
 clauses causing UNSAT. This means that the solver can give more meaningful
 feedback than just a 1-bit value (UNSAT) in case it's not SAT -- in which
 case it gives a satisfying assignment, a very helpful trace.

--
Ticket URL: <http://trac.sagemath.org/ticket/15674#comment:7>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica, 
and MATLAB

-- 
You received this message because you are subscribed to the Google Groups 
"sage-trac" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sage-trac.
For more options, visit https://groups.google.com/groups/opt_out.

Reply via email to