Changes between Version 6 and Version 13 of Ticket #418


Ignore:
Timestamp:
06/15/12 16:18:25 (9 years ago)
Author:
malb
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #418

    • Property Keywords SAT added
    • Property Cc fichtejo abmasse added
    • Property Milestone changed from sage-wishlist to sage-5.1
    • Property Summary changed from Wrap MiniSAT to Add SAT Solvers
  • Ticket #418 – Description

    v6 v13  
    1 Make an optional package for (Crypto)MiniSAT an award winning SAT solver.
     1This ticket implements
    22
    3 Also implement/port Nicolas Courtois' and Gregory Bard's ANF to CNF converter (http://eprint.iacr.org/2006/402.pdf) to SAGE.
     3 * an optional Sage package for C!ryptoMiniSat
     4 * a C++ interface to !CryptoMiniSat which supports xor clauses, options, conflict clauses and learnt clause extraction
     5 * a generic interface for various SAT solvers based on the DIMACS file format
     6 * instantiations of this interface for !Glucose and !RSat
     7 * a converter for Boolean Polynomials to !SAT
     8 * highlevel functions for solving Boolean polynomial systems and for learning new polynomials for Boolean polynomial systems
    49
    5 '''Install''' http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.1.spkg
     10How to install/test:
     11
     12 1. '''Install''' http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.1.spkg
     13 1. '''Pull''' from https://bitbucket.org/malb/sage-cryptominisat
     14
     15'''Note to release manager:''' The SPKG is optional but the patches for the Sage library should be merged.