#418: Add SAT Solvers
--------------------------------------------------------------+-------------
Reporter: malb | Owner:
was
Type: enhancement | Status:
needs_review
Priority: minor | Milestone:
sage-5.1
Component: packages | Resolution:
Keywords: SAT | Work issues:
Report Upstream: Fixed upstream, in a later stable release. | Reviewers:
Authors: Martin Albrecht | Merged in:
Dependencies: | Stopgaps:
--------------------------------------------------------------+-------------
Changes (by malb):
* status: needs_work => needs_review
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.1.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 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.
--
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/418#comment:23>
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.
