Opened 11 years ago

Closed 6 years ago

Last modified 3 years ago

#418 closed enhancement (fixed)

Add SAT Solvers

Reported by: malb Owned by: was
Priority: minor Milestone: sage-5.3
Component: packages: optional Keywords: SAT
Cc: PolyBoRi, fichtejo, abmasse, sbulygin Merged in: sage-5.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 jdemeyer)

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.

Change History (44)

comment:1 Changed 11 years ago by mabshoff

  • Milestone set to sage-wishlist

comment:2 Changed 11 years ago by 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

comment:3 Changed 10 years ago by mabshoff

#5671 is a duplicate of this ticket.

Cheers,

Michael

comment:4 Changed 10 years ago by 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.

comment:5 Changed 9 years ago by malb

  • Cc PolyBoRi added

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

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 7 years ago by malb

  • Authors set to Martin Albrecht
  • Description modified (diff)
  • Report Upstream set to N/A
  • Status changed from new to needs_review

comment:7 Changed 7 years ago by was

See also #11479.

comment:8 Changed 7 years ago by malb

  • Status changed from needs_review to needs_work

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.

comment:10 Changed 7 years ago by 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.

comment:11 Changed 7 years ago by kcrisman

  • 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 7 years ago by abmasse

  • Cc abmasse added

comment:13 Changed 6 years ago by malb

  • Description modified (diff)
  • Keywords SAT added
  • Milestone changed from sage-wishlist to sage-5.1
  • Status changed from needs_work to needs_review
  • Summary changed from Wrap MiniSAT to Add SAT Solvers

comment:15 follow-up: Changed 6 years ago by malb

Anyone up for reviewing this?

comment:16 in reply to: ↑ 15 ; follow-up: Changed 6 years ago by AlexanderDreyer

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 6 years ago by 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.

comment:18 Changed 6 years ago by 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'

comment:19 Changed 6 years ago by 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

comment:20 Changed 6 years ago by malb

  • 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/cryptominisat-devel/2012-June/000325.html

comment:21 Changed 6 years ago by AlexanderDreyer

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

comment:22 Changed 6 years ago by AlexanderDreyer

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 6 years ago by malb

  • Description modified (diff)
  • Status changed from needs_work to needs_review

comment:24 Changed 6 years ago by 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.

Last edited 6 years ago by malb (previous) (diff)

comment:25 Changed 6 years ago by AlexanderDreyer

  • 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  
    18911891    ext_modules.extend([
    18921892        Extension("sage.sat.solvers.cryptominisat.cryptominisat",
    18931893                  ["sage/sat/solvers/cryptominisat/cryptominisat.pyx"],
    1894                   include_dirs = [SAGE_INC, SAGE_INC+"/cryptominisat/mtl", SAGE_INC+"/cryptominisat/Solver"],
     1894                  include_dirs = [SAGE_INC, SAGE_INC+"/cmsat/"],
    18951895                  language = "c++",
    18961896                  libraries = ['cryptominisat', 'z']),
    18971897        Extension("sage.sat.solvers.cryptominisat.solverconf",
    18981898                  ["sage/sat/solvers/cryptominisat/solverconf.pyx", "sage/sat/solvers/cryptominisat/solverconf_helper.cpp"],
    1899                   include_dirs = [SAGE_INC, SAGE_INC+"/cryptominisat/mtl", SAGE_INC+"/cryptominisat/Solver"],
     1899                  include_dirs = [SAGE_INC, SAGE_INC+"/cmsat/"],
    19001900                  language = "c++",
    19011901                  libraries = ['cryptominisat', 'z'])
    19021902        ])
  • sage/sat/solvers/cryptominisat/solverconf_helper.h

    diff -r ef5eaff5d6cd sage/sat/solvers/cryptominisat/solverconf_helper.h
    a b  
    1414 *                  http://www.gnu.org/licenses/
    1515 ****************************************************************************/
    1616
    17 #include <cryptominisat/Solver/SolverConf.h>
     17#include <SolverConf.h>
    1818
    1919enum sc_type {
    2020  t_int      = 1<<0,

comment:26 Changed 6 years ago by sbulygin

  • Cc sbulygin added

comment:27 Changed 6 years ago by malb

  • 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 6 years ago by malb

ping :)

comment:29 Changed 6 years ago by 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.

comment:30 Changed 6 years ago by AlexanderDreyer

  • Status changed from needs_review to positive_review

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

comment:31 Changed 6 years ago by jdemeyer

  • Description modified (diff)
  • Status changed from positive_review to needs_work

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

comment:32 Changed 6 years ago by jdemeyer

  • Component changed from packages to optional packages

comment:34 Changed 6 years ago by jdemeyer

  • Status changed from needs_work to positive_review

comment:35 Changed 6 years ago by schilly

i just put the spkg on the server+mirrors.

comment:36 Changed 6 years ago by 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).

comment:37 Changed 6 years ago by jdemeyer

  • Dependencies set to #13315
  • Milestone changed from sage-5.3 to sage-pending

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 6 years ago by jdemeyer

  • Milestone changed from sage-pending to sage-5.3

comment:39 Changed 6 years ago by jdemeyer

  • Merged in set to sage-5.3.beta1
  • Resolution set to fixed
  • Status changed from positive_review to closed

comment:40 Changed 3 years ago by 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.

comment:41 Changed 3 years ago by jdemeyer

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

comment:42 Changed 3 years ago by 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.

comment:43 Changed 3 years ago by jdemeyer

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

comment:44 Changed 3 years ago by malb

IIRC, yep.

Note: See TracTickets for help on using tickets.