#418: Add SAT Solvers
--------------------------------------------------------------+-------------
Reporter: malb | Owner:
was
Type: enhancement | Status:
needs_work
Priority: minor | Milestone:
sage-5.3
Component: packages | Resolution:
Keywords: SAT | Work issues:
Report Upstream: Fixed upstream, in a later stable release. | Reviewers:
Alexander Dreyer
Authors: Martin Albrecht | Merged in:
Dependencies: | Stopgaps:
--------------------------------------------------------------+-------------
Changes (by jdemeyer):
* status: positive_review => needs_work
Old description:
> This ticket implements
>
> * an optional Sage package for C!ryptoMiniSat
> * a C++ interface to !CryptoMiniSat which supports xor clauses, options,
> conflict clauses and learnt clause extraction
> * a generic interface for various SAT solvers based on the DIMACS file
> format
> * instantiations of this interface for Glucose and RSat
> * a converter for Boolean Polynomials to SAT
> * highlevel functions for solving Boolean polynomial systems and for
> learning new polynomials for Boolean polynomial systems
>
> How to install/test:
>
> 1.
> '''Install''' http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.5.spkg
> 1. '''Pull''' from https://bitbucket.org/malb/sage-cryptominisat
>
> '''Note to release manager:''' The SPKG is optional but the patches for
> the Sage library should be merged.
New description:
This ticket implements
* an optional Sage package for !CryptoMiniSat
* a C++ interface to !CryptoMiniSat which supports xor clauses, options,
conflict clauses and learnt clause extraction
* a generic interface for various SAT solvers based on the DIMACS file
format
* instantiations of this interface for Glucose and RSat
* a converter for Boolean Polynomials to SAT
* highlevel functions for solving Boolean polynomial systems and for
learning new polynomials for Boolean polynomial systems
How to install/test:
1.
'''Install''' http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.5.spkg
1. '''Pull''' from https://bitbucket.org/malb/sage-cryptominisat
'''Note to release manager:''' The SPKG is optional but the patches for
the Sage library should be merged.
--
Comment:
`_sig_on` and `_sig_off` are deprecated since sage-4.7. Use `sig_on()`
and `sig_off()` instead. See #10115 (and note the reviewer of that
ticket!).
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/418#comment:31>
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 post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/sage-trac?hl=en.
