#418 closed enhancement (fixed)
Add SAT Solvers
Reported by:  malb  Owned by:  was 

Priority:  minor  Milestone:  sage5.3 
Component:  packages: optional  Keywords:  SAT 
Cc:  PolyBoRi, fichtejo, abmasse, sbulygin  Merged in:  sage5.3.beta1 
Authors:  Martin Albrecht  Reviewers:  Alexander Dreyer 
Report Upstream:  Fixed upstream, in a later stable release.  Work issues:  
Branch:  Commit:  
Dependencies:  #13315  Stopgaps: 
Description (last modified by )
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:
 Install http://sage.math.washington.edu/home/malb/spkgs/cryptominisat2.9.5.spkg
 Pull from https://bitbucket.org/malb/sagecryptominisat
Note to release manager: The SPKG is optional but the patches for the Sage library should be merged.
Change History (44)
comment:1 Changed 15 years ago by
 Milestone set to sagewishlist
comment:2 Changed 15 years ago by
comment:3 Changed 13 years ago by
comment:4 Changed 13 years ago by
#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.
comment:5 Changed 13 years ago by
 Cc PolyBoRi added
Btw. there are two independent opensource ANF2CNF converters available now:
 http://bitbucket.org/malb/algebraic_attacks/src/tip/anf2cnf.py
 http://bitbucket.org/brickenstein/polyboriscripts/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.
comment:6 Changed 11 years ago by
 Description modified (diff)
 Report Upstream set to N/A
 Status changed from new to needs_review
an optional SPKG is available here:
http://sage.math.washington.edu/home/malb/spkgs/cryptominisat2.9.1.spkg
comment:7 Changed 11 years ago by
See also #11479.
comment:8 Changed 10 years ago by
 Status changed from needs_review to needs_work
See
https://bitbucket.org/malb/sagecryptominisat https://bitbucket.org/malb/cryptominisatspkg
for a C++ interface to CryptoMiniSat from !Sage. The basic solver works, but lots of work is still to be done.
comment:9 Changed 10 years ago by
comment:10 Changed 10 years ago by
comment:11 Changed 10 years ago by
 Cc fichtejo added
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.
comment:12 Changed 10 years ago by
 Cc abmasse added
comment:13 Changed 10 years ago by
 Description modified (diff)
 Keywords SAT added
 Milestone changed from sagewishlist to sage5.1
 Status changed from needs_work to needs_review
 Summary changed from Wrap MiniSAT to Add SAT Solvers
comment:14 Changed 10 years ago by
I rebased https://bitbucket.org/malb/sagecryptominisat to 5.0.1
comment:15 followup: ↓ 16 Changed 10 years ago by
Anyone up for reviewing this?
comment:16 in reply to: ↑ 15 ; followup: ↓ 17 Changed 10 years ago by
Replying to malb:
Anyone up for reviewing this?
I'll have a look at it. What about kcrisman's questions?
comment:17 in reply to: ↑ 16 Changed 10 years ago by
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.
comment:18 Changed 10 years ago by
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'
comment:19 Changed 10 years ago by
Installation of the spkg fails on my 32bit 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
comment:20 Changed 10 years ago by
 Report Upstream changed from N/A to Fixed upstream, in a later stable release.
 Status changed from needs_review to needs_work
Ah, it's a known issue and the next release of CryptoMiniSat? is supposed to fix this:
http://lists.gforge.inria.fr/pipermail/cryptominisatdevel/2012June/000325.html
comment:21 Changed 10 years ago by
I have the same issue here. But I can give the sage library part already a positive review.
comment:22 Changed 10 years ago by
PS: It seems that Mate has just release cryptominisat 2.9.5: https://gforge.inria.fr/frs/?group_id=1992&release_id=7438
comment:23 Changed 10 years ago by
 Description modified (diff)
 Status changed from needs_work to needs_review
comment:24 Changed 10 years ago by
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.
comment:25 Changed 10 years ago by
 Status changed from needs_review to needs_work
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
diff r ef5eaff5d6cd module_list.py
a b 1891 1891 ext_modules.extend([ 1892 1892 Extension("sage.sat.solvers.cryptominisat.cryptominisat", 1893 1893 ["sage/sat/solvers/cryptominisat/cryptominisat.pyx"], 1894 include_dirs = [SAGE_INC, SAGE_INC+"/c ryptominisat/mtl", SAGE_INC+"/cryptominisat/Solver"],1894 include_dirs = [SAGE_INC, SAGE_INC+"/cmsat/"], 1895 1895 language = "c++", 1896 1896 libraries = ['cryptominisat', 'z']), 1897 1897 Extension("sage.sat.solvers.cryptominisat.solverconf", 1898 1898 ["sage/sat/solvers/cryptominisat/solverconf.pyx", "sage/sat/solvers/cryptominisat/solverconf_helper.cpp"], 1899 include_dirs = [SAGE_INC, SAGE_INC+"/c ryptominisat/mtl", SAGE_INC+"/cryptominisat/Solver"],1899 include_dirs = [SAGE_INC, SAGE_INC+"/cmsat/"], 1900 1900 language = "c++", 1901 1901 libraries = ['cryptominisat', 'z']) 1902 1902 ]) 
sage/sat/solvers/cryptominisat/solverconf_helper.h
diff r ef5eaff5d6cd sage/sat/solvers/cryptominisat/solverconf_helper.h
a b 14 14 * http://www.gnu.org/licenses/ 15 15 ****************************************************************************/ 16 16 17 #include < cryptominisat/Solver/SolverConf.h>17 #include <SolverConf.h> 18 18 19 19 enum sc_type { 20 20 t_int = 1<<0,
comment:26 Changed 10 years ago by
 Cc sbulygin added
comment:27 Changed 10 years ago by
 Reviewers set to Alexander Dreyer
 Status changed from needs_work to needs_review
I've updated the interface to work with 2.9.5. Thanks for spotting this!
comment:28 Changed 10 years ago by
ping :)
comment:29 Changed 10 years ago by
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.
comment:30 Changed 10 years ago by
 Status changed from needs_review to positive_review
Ok, tests succeeded, so I can give positive review.
comment:31 Changed 10 years ago by
 Description modified (diff)
 Status changed from positive_review to needs_work
_sig_on
and _sig_off
are deprecated since sage4.7. Use sig_on()
and sig_off()
instead. See #10115 (and note the reviewer of that ticket!).
comment:32 Changed 10 years ago by
 Component changed from packages to optional packages
comment:33 Changed 10 years ago by
comment:34 Changed 10 years ago by
 Status changed from needs_work to positive_review
comment:35 Changed 10 years ago by
i just put the spkg on the server+mirrors.
comment:36 Changed 10 years ago by
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).
comment:37 Changed 10 years ago by
 Dependencies set to #13315
 Milestone changed from sage5.3 to sagepending
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.
comment:38 Changed 10 years ago by
 Milestone changed from sagepending to sage5.3
comment:39 Changed 10 years ago by
 Merged in set to sage5.3.beta1
 Resolution set to fixed
 Status changed from positive_review to closed
comment:40 Changed 7 years ago by
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.
comment:41 Changed 7 years ago by
And even if it were true, I wouldn't like it (interrupts should raise KeyboardInterrupt
).
comment:42 Changed 7 years ago by
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
.
comment:43 Changed 7 years ago by
I see, so the interrupts this talks about do not refer to KeyboardInterrupt
s (a.k.a. CTRLC)?
comment:44 Changed 7 years ago by
IIRC, yep.
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