Add SAT Solvers

[malb]

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
2. 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.

Depends on #13315

Upstream: Fixed upstream, in a later stable release.

CC: @sagetrac-PolyBoRi @sagetrac-fichtejo @sagetrac-abmasse @sagetrac-sbulygin

Component: packages: optional

Keywords: SAT

Author: Martin Albrecht

Reviewer: Alexander Dreyer

Merged: sage-5.3.beta1

Issue created by migration from https://trac.sagemath.org/ticket/418

[b614eff1-8a5d-4a32-8fba-5a1846341e28]

comment:2

Actually there are many SAT solvers out of there

http://www.cs.ubc.ca/~hoos/SATLIB/solvers.html

and many of them understand a commond format, the conjuntive normal form in the DIMACS format:

http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps

An important first step, would be creating a method for the symbolic logic class that supports output of a formula in the DIMACS format

[85eec1a4-3d04-4b4d-b711-d4db03337c41]

comment:3

5671 is a duplicate of this ticket.

Cheers,

Michael

[williamstein]

comment:4

5671 a special case of what is asked for in this ticket. This ticket seems to be about wrapping multiple SAT solvers, and implementing porting ANF and CNF codes to Sage. By the way, in wrapping minisat the first thing we did was not use DIMACS format for the wrapper, since that all goes via string processing, and we want a direct C library interface. DIMACS format should also be supported at some point though.

[malb]

comment:5

Btw. there are two independent open-source ANF2CNF converters available now:

• http://bitbucket.org/malb/algebraic_attacks/src/tip/anf2cnf.py
• http://bitbucket.org/brickenstein/polybori-scripts/src/tip/cnf.py

The later will be available in PolyBoRi soon, I am not sure whether the former is completely redundant because of the later. More benchmarks are needed to figure this out I guess.

[malb]

Description changed:

--- 
+++ 
@@ -1 +1,5 @@
-Make an optional SAGE package for MiniSAT (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/) an award winning SAT solver. Also implement/port Nicolas Courtois' and Gregory Bard's ANF to CNF converter (http://eprint.iacr.org/2006/402.pdf) to SAGE.
+Make an optional package for (Crypto)MiniSAT an award winning SAT solver. 
+
+Also implement/port Nicolas Courtois' and Gregory Bard's ANF to CNF converter (http://eprint.iacr.org/2006/402.pdf) to SAGE.
+
+**Install** http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.1.spkg

[malb]

Author: Martin Albrecht

[malb]

comment:6

an optional SPKG is available here:

http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.1.spkg

[williamstein]

comment:7

See also #11479.

[malb]

comment:8

See https://bitbucket.org/malb/sage-cryptominisat https://bitbucket.org/malb/cryptominisat-spkg for a C++ interface to CryptoMiniSat from !Sage. The basic solver works, but lots of work is still to be done.

[malb]

comment:9

New SPKG here: http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.4.spkg

[kcrisman]

comment:10

What is the relationship of this ticket to #5671 and #11479? I feel like they could be considered dups, but they both have code attached and after all there are other such solvers out there.

[kcrisman]

comment:11

At #11479 the suggestion was to make sure there was a generic backend for eventually having interfaces with other solvers (presumably using some of the code there). Would that be pretty easy to do with this, or pretty challenging? It sounds like fichtejo is interested in helping with that, if it is practical/meaningful; naturally, it may be the case that combining any of these pieces would be too challenging to be practical.

[malb]

Changed keywords from none to SAT

[malb]

Description changed:

--- 
+++ 
@@ -1,5 +1,15 @@
-Make an optional package for (Crypto)MiniSAT an award winning SAT solver. 
+This ticket implements

-Also implement/port Nicolas Courtois' and Gregory Bard's ANF to CNF converter (http://eprint.iacr.org/2006/402.pdf) to SAGE.
+* 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

-**Install** http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.1.spkg
+How to install/test:
+
+1. **Install** http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.1.spkg
+2. **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.

[malb]

comment:14

I rebased https://bitbucket.org/malb/sage-cryptominisat to 5.0.1

[malb]

comment:15

Anyone up for reviewing this?

[d46d2cb1-860f-484d-8329-8ebfc9f5d004]

comment:16

Replying to @malb:

Anyone up for reviewing this?

I'll have a look at it. What about kcrisman's questions?

[kcrisman]

comment:17

Anyone up for reviewing this?

I'll have a look at it. What about kcrisman's questions?

malb considers them more or less dupes (at least #5671), especially since he added DIMACS to this ticket. I am not knowledgeable enough to say whether that is legitimate, but had just wanted to point it out.

[malb]

comment:18

I should mention that I didn't implement reading from DIMACS files. I did implement exporting to DIMACS but perhaps some people would find this interface not that nice. I find it reasonably elegant though because it is quite modular:

sage: from sage.sat.converters.polybori import CNFEncoder        
sage: solver = sage.sat.solvers.dimacs.DIMACS(filename="mycnf.cnf")
sage: F,s = mq.SR(1,2,2,4,gf2=True,polybori=True).polynomial_system()
sage: encoder = CNFEncoder(solver, F.ring())
sage: _ = encoder(F)
sage: solver.write()
'mycnf.cnf'

[89f39f15-88e8-4e79-9bc0-0739a7fc497c]

comment:19

Installation of the spkg fails on my 32-bit ubuntu 12.04.

g++ -DHAVE_CONFIG_H -I. -I.. -I/usr/local/sage/local/include -Wall -I. -I./../MTRand -I./../mtl -fopenmp -I/usr/local/sage/local/include -L/usr/local/sage/local/lib -g -fPIC -Wall -pedantic -O2 -MT DimacsParser.lo -MD -MP -MF .deps/DimacsParser.Tpo -c DimacsParser.cpp  -fPIC -DPIC -o .libs/DimacsParser.o
DimacsParser.cpp: In member function ‘void CMSat::DimacsParser::parse_DIMACS(T) [with T = _IO_FILE*]’:
DimacsParser.cpp:482:60:   instantiated from here
DimacsParser.cpp:461:33: erreur: no matching function for call to ‘StreamBuffer::StreamBuffer(_IO_FILE*&)’
DimacsParser.cpp:461:33: note: candidates are:
StreamBuffer.h:59:5: note: StreamBuffer::StreamBuffer(gzFile)
StreamBuffer.h:59:5: note:   no known conversion for argument 1 from ‘_IO_FILE*’ to ‘gzFile’
StreamBuffer.h:29:7: note: StreamBuffer::StreamBuffer(const StreamBuffer&)
StreamBuffer.h:29:7: note:   no known conversion for argument 1 from ‘_IO_FILE*’ to ‘const StreamBuffer&’
make[2]: *** [DimacsParser.lo] Erreur 1

[malb]

comment:20

Ah, it's a known issue and the next release of CryptoMiniSat is supposed to fix this:

http://lists.gforge.inria.fr/pipermail/cryptominisat-devel/2012-June/000325.html

[malb]

Upstream: Fixed upstream, in a later stable release.

[d46d2cb1-860f-484d-8329-8ebfc9f5d004]

comment:21

I have the same issue here. But I can give the sage library part already a positive review.

[d46d2cb1-860f-484d-8329-8ebfc9f5d004]

comment:22

PS: It seems that Mate has just release cryptominisat 2.9.5: https://gforge.inria.fr/frs/?group_id=1992&release_id=7438

[malb]

Description changed:

--- 
+++ 
@@ -3,13 +3,13 @@
 * 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
+* 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. **Install** http://sage.math.washington.edu/home/malb/spkgs/cryptominisat-2.9.5.spkg
 2. **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.

[malb]

comment:24

I've updated the SPKG to 2.9.5 and I have also added a patch to the Sage interface which deals with GCC 4.7.0 being more strict (I believe) about return 1; from void function.

[d46d2cb1-860f-484d-8329-8ebfc9f5d004]

comment:25

It seems that interfaces had changes, so the spkg doesn't fit with the sage library patches. It seems that your installation picked up the headers from the old install. Maybe its enough to delete SAGE_INC+"/cryptominisat/?

I fixed a few trivial things below, but there's more to be done:

diff -r ef5eaff5d6cd module_list.py
--- a/module_list.py    Fri Jun 29 17:04:34 2012 +0100
+++ b/module_list.py    Sun Jul 01 23:40:53 2012 +0200
@@ -1891,12 +1891,12 @@
     ext_modules.extend([
         Extension("sage.sat.solvers.cryptominisat.cryptominisat",
                   ["sage/sat/solvers/cryptominisat/cryptominisat.pyx"],
-                  include_dirs = [SAGE_INC, SAGE_INC+"/cryptominisat/mtl", SAGE_INC+"/cryptominisat/Solver"],
+                  include_dirs = [SAGE_INC, SAGE_INC+"/cmsat/"],
                   language = "c++",
                   libraries = ['cryptominisat', 'z']),
         Extension("sage.sat.solvers.cryptominisat.solverconf",
                   ["sage/sat/solvers/cryptominisat/solverconf.pyx", "sage/sat/solvers/cryptominisat/solverconf_helper.cpp"],
-                  include_dirs = [SAGE_INC, SAGE_INC+"/cryptominisat/mtl", SAGE_INC+"/cryptominisat/Solver"],
+                  include_dirs = [SAGE_INC, SAGE_INC+"/cmsat/"],
                   language = "c++",
                   libraries = ['cryptominisat', 'z'])
         ])
diff -r ef5eaff5d6cd sage/sat/solvers/cryptominisat/solverconf_helper.h
--- a/sage/sat/solvers/cryptominisat/solverconf_helper.h        Fri Jun 29 17:04:34 2012 +0100
+++ b/sage/sat/solvers/cryptominisat/solverconf_helper.h        Sun Jul 01 23:40:53 2012 +0200
@@ -14,7 +14,7 @@
  *                  http://www.gnu.org/licenses/
  ****************************************************************************/

-#include <cryptominisat/Solver/SolverConf.h>
+#include <SolverConf.h>

 enum sc_type {
   t_int      = 1<<0,

[malb]

comment:27

I've updated the interface to work with 2.9.5. Thanks for spotting this!

[malb]

Reviewer: Alexander Dreyer

[malb]

comment:28

ping :)

[d46d2cb1-860f-484d-8329-8ebfc9f5d004]

comment:29

The spkg installs and I was also able to pull from Sage 5.1(rc0) with automated merge. First tests succeeded, So we are close to a positive review, I'm just waiting for make ptestlong to finish.

[d46d2cb1-860f-484d-8329-8ebfc9f5d004]

comment:30

Ok, tests succeeded, so I can give positive review.

[jdemeyer]

Description changed:

--- 
+++ 
@@ -1,6 +1,6 @@
 This ticket implements

-* an optional Sage package for C!ryptoMiniSat
+* 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

[jdemeyer]

comment:31

_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!).

[malb]

comment:33

Doh! Fixed: https://bitbucket.org/malb/sage-cryptominisat/changeset/bf994dfe464e

[haraldschilly]

comment:35

i just put the spkg on the server+mirrors.

[jdemeyer]

comment:36

Okay, I'm testing the repo. Please don't change it anymore (unless of course this ticket gets set to needs_work for some reason).

[jdemeyer]

comment:37

There is a problem with sage/sat/solvers/cryptominisat/solverconf_helper.cpp not showing up in a Sage source distribution, a fix is to appear at #13315.

[jdemeyer]

Dependencies: #13315

[jdemeyer]

Merged: sage-5.3.beta1

[jdemeyer]

comment:40

Does anybody remember why this sentence was added to the documentation?

        - If the solver was interrupted before deciding satisfiability
          ``None``.

I don't believe that this claim is true.

[jdemeyer]

comment:41

And even if it were true, I wouldn't like it (interrupts should raise KeyboardInterrupt).

[malb]

comment:42

You can limit the SAT solver. For example, you can tell it to only do x restarts. In this case, we might not know if the problem is satisfiable, so we return None.

[jdemeyer]

comment:43

I see, so the interrupts this talks about do not refer to KeyboardInterrupts (a.k.a. CTRL-C)?

[malb]

comment:44

IIRC, yep.