Opened 3 years ago

Closed 3 years ago

#19042 closed enhancement (fixed)

Fallback SAT solver in Sage

Reported by: ncohen Owned by:
Priority: major Milestone: sage-6.9
Component: numerical Keywords:
Cc: malb, vdelecroix, tmonteil Merged in:
Authors: Nathann Cohen Reviewers: Jeroen Demeyer
Report Upstream: N/A Work issues:
Branch: 94166b6 (Commits) Commit: 94166b67c1a2e0a06770b7e7fb6acffd71d480f6
Dependencies: Stopgaps:

Description

This ticket implements a SAT solver by relying upon the MILP features of Sage.

This is not glorious, but at least the feature is available by default and we can assume it exists in all cases.

Nathann

Change History (30)

comment:1 Changed 3 years ago by ncohen

  • Branch set to public/19042
  • Cc tmonteil added
  • Commit set to 3a548d9882d963d9740d57d7095ad3ac4df24e03
  • Status changed from new to needs_review

New commits:

3a548d9trac #19042: Default SAT solver in Sage

comment:2 Changed 3 years ago by ncohen

  • Summary changed from Default SAT solver in Sage to Fallback SAT solver in Sage

comment:3 Changed 3 years ago by tmonteil

Since cryptominisat is optional for (much) more than one year, why not make it standard ?

comment:4 Changed 3 years ago by ncohen

Check the license and if it is compatible write to sage-devel. It may still be useful to have a LP backend to double-check results.

comment:5 follow-up: Changed 3 years ago by mkoeppe

Why call it "LP" when it's an ILP?

comment:6 in reply to: ↑ 5 Changed 3 years ago by ncohen

Why call it "LP" when it's an ILP?

I use it as a generic term. LP, MILP, ILP... As long as people understand what it is about ..

comment:7 Changed 3 years ago by git

  • Commit changed from 3a548d9882d963d9740d57d7095ad3ac4df24e03 to eb01119cd733a39fd72aabfc7feb2114115d1526

Branch pushed to git repo; I updated commit sha1. New commits:

eb01119trac #19042: Merged with 6.9.rc0

comment:8 follow-up: Changed 3 years ago by jdemeyer

Just a comment: why is src/sage/sat/solvers/sat_lp.pyx a Cython file? You don't seem to use any Cython features...

I also don't like the except KeyboardInterrupt. Why did you add that?

comment:9 Changed 3 years ago by jdemeyer

We now have PackageNotFoundError (in src/sage/misc/package.py) for this:

        except ImportError:
            raise ImportError("To enable this feature, run 'sage -i cryptominisat'.")

I remind you that this is an expensive check: is_package_installed('cryptominisat') Checking whether the import succeeds is a lot more efficient.

comment:10 in reply to: ↑ 8 ; follow-up: Changed 3 years ago by ncohen

Just a comment: why is src/sage/sat/solvers/sat_lp.pyx a Cython file? You don't seem to use any Cython features...

Probably because it used to be a copy/paste of the cryptominisat file. I can change it if you prefer.

I also don't like the except KeyboardInterrupt. Why did you add that?

I do not like it either. But the doc of the same function in cryptominisat says that the function returns None when it is interrupted.

Nathann

comment:11 in reply to: ↑ 10 Changed 3 years ago by jdemeyer

Replying to ncohen:

But the doc of the same function in cryptominisat says that the function returns None when it is interrupted.

I don't believe that doc. From an example based on a doctest:

sage: from sage.sat.solvers import CryptoMiniSat          # optional - cryptominisat
sage: from sage.sat.converters.polybori import CNFEncoder # optional - cryptominisat
sage: set_random_seed( 22 )                               # optional - cryptominisat
sage: sr = mq.SR(1,4,4,4,gf2=True,polybori=True)          # optional - cryptominisat
sage: F,s = sr.polynomial_system()                        # optional - cryptominisat
sage: cms = CryptoMiniSat(maxrestarts=10,verbosity=0)     # optional - cryptominisat
sage: phi = CNFEncoder(cms, F.ring())(F)                  # optional - cryptominisat
sage: alarm(0.2); cms()
---------------------------------------------------------------------------
AlarmInterrupt                            Traceback (most recent call last)
<ipython-input-8-257eb3253d78> in <module>()
----> 1 alarm(RealNumber('0.2')); cms()

/usr/local/src/sage-config/src/sage/sat/solvers/cryptominisat/cryptominisat.pyx in sage.sat.solvers.cryptominisat.cryptominisat.CryptoMiniSat.__call__ (build/cythonized/sage/sat/solvers/cryptominisat/cryptominisat.cpp:2211)()
    299         cdef lbool r
    300         if assumptions is None:
--> 301              sig_on()
    302              r = self._solver.solve()
    303              sig_off()

/usr/local/src/sage-config/src/sage/ext/interrupt/interrupt.pyx in sage.ext.interrupt.interrupt.sig_raise_exception (build/cythonized/sage/ext/interrupt/interrupt.c:957)()
     88         raise KeyboardInterrupt
     89     if sig == SIGALRM:
---> 90         raise AlarmInterrupt
     91     if sig == SIGILL:
     92         if msg == NULL:

AlarmInterrupt: 

comment:12 Changed 3 years ago by git

  • Commit changed from eb01119cd733a39fd72aabfc7feb2114115d1526 to 470500f86e188164d23cb5c417ebecbab10f43cc

Branch pushed to git repo; I updated commit sha1. New commits:

d9ba9b2trac #19042: Faster package check
d35f98ftrac #19042: Remove KeyboardInterrupt check
470500ftrac #19042: pyx->py

comment:13 Changed 3 years ago by ncohen

Here it is.

Nathann

comment:14 Changed 3 years ago by jdemeyer

I asked #418 about the KeyboardInterrupt, in case somebody remembers there.

comment:15 Changed 3 years ago by jdemeyer

The correct call is

raise PackageNotFoundError("cryptominisat")

comment:16 Changed 3 years ago by jdemeyer

  • Status changed from needs_review to needs_work

comment:17 Changed 3 years ago by ncohen

Oh. Automatic error message. Cool.

comment:18 Changed 3 years ago by git

  • Commit changed from 470500f86e188164d23cb5c417ebecbab10f43cc to e9309e7c826982f251825f1c8f959723daf0ab35

Branch pushed to git repo; I updated commit sha1. New commits:

e9309e7trac #19042: Wrong text

comment:19 Changed 3 years ago by ncohen

  • Status changed from needs_work to needs_review

comment:20 Changed 3 years ago by jdemeyer

In turns out that the word "interrupt" has a specific meaning in cryptominisat, which is unrelated to KeyboardInterrupt.

comment:21 Changed 3 years ago by jdemeyer

Why the # random?

sage: solver = SAT() # random

comment:22 Changed 3 years ago by jdemeyer

I would prefer this to be a lazy import:

from solvers.satsolver import SAT

comment:23 Changed 3 years ago by git

  • Commit changed from e9309e7c826982f251825f1c8f959723daf0ab35 to a4ac4458b8f5aa633047299f9db2269fdf4e74ca

Branch pushed to git repo; I updated commit sha1. New commits:

a4ac445trac #19042: Review

comment:24 Changed 3 years ago by ncohen

About random: I wrongly believed that Cryptominisat always printed information when instanciated.

comment:25 follow-up: Changed 3 years ago by jdemeyer

  • Reviewers set to Jeroen Demeyer
  • Status changed from needs_review to needs_work

A few more details:

  1. It's ugly that your ILP solver returns values as 0.0 and 1.0. It should be converted to True/False.
  1. Its performances -> Its performance
  1. cryptominisat_available = True -> solver = 'cryptominisat' and cryptominisat_available = False -> solver = 'LP'. That's a lot cleaner: you can remove the solver is None checks.
  1. Please fix the deicison typo also in src/sage/sat/converters/polybori.py

comment:26 Changed 3 years ago by git

  • Commit changed from a4ac4458b8f5aa633047299f9db2269fdf4e74ca to 94166b67c1a2e0a06770b7e7fb6acffd71d480f6

Branch pushed to git repo; I updated commit sha1. New commits:

94166b6trac #19042: Review

comment:27 in reply to: ↑ 25 Changed 3 years ago by ncohen

  • Status changed from needs_work to needs_review
  1. It's ugly that your ILP solver returns values as 0.0 and 1.0. It should be converted to True/False.

Right.

  1. Its performances -> Its performance

Done.

  1. cryptominisat_available = True -> solver = 'cryptominisat' and cryptominisat_available = False -> solver = 'LP'. That's a lot cleaner: you can remove the solver is None checks.

I'm an idiot.

  1. Please fix the deicison typo also in src/sage/sat/converters/polybori.py

Done.

comment:28 Changed 3 years ago by jdemeyer

  • Status changed from needs_review to positive_review

comment:29 Changed 3 years ago by ncohen

Thanks !

comment:30 Changed 3 years ago by vbraun

  • Branch changed from public/19042 to 94166b67c1a2e0a06770b7e7fb6acffd71d480f6
  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.