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.

[pdenapo]

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

[mabshoff]

#5671 is a duplicate of this ticket.

Cheers,

Michael

[was]

#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]

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]

an optional SPKG is available here:

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

[was]

See also #11479.

[malb]

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]

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

[kcrisman]

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]

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]

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

[malb]

Anyone up for reviewing this?

[AlexanderDreyer]

Replying to malb:

Anyone up for reviewing this?

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

[kcrisman]

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]

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'

[Bouillaguet]

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]

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

[AlexanderDreyer]

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

[AlexanderDreyer]

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

[malb]

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.

[AlexanderDreyer]

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:

module_list.py

@@ -1891 +1891 @@
     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'])
         ])

sage/sat/solvers/cryptominisat/solverconf_helper.h

@@ -14 +14 @@
  *                  http://www.gnu.org/licenses/
  ****************************************************************************/
 
-#include <cryptominisat/Solver/SolverConf.h>
+#include <SolverConf.h>
 
 enum sc_type {
   t_int      = 1<<0,

[malb]

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

[malb]

ping :)

[AlexanderDreyer]

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.

[AlexanderDreyer]

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

[jdemeyer]

_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]

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

[schilly]

i just put the spkg on the server+mirrors.

[jdemeyer]

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]

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]

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]

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

[malb]

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]

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

[malb]

IIRC, yep.