Fallback SAT solver in Sage

[ncohen]

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

[ncohen]

New commits:

​3a548d9

trac #19042: Default SAT solver in Sage

[tmonteil]

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

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

[mkoeppe]

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

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

[git]

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

​eb01119

trac #19042: Merged with 6.9.rc0

[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?

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

[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

[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: 

[git]

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

​d9ba9b2	trac #19042: Faster package check
​d35f98f	trac #19042: Remove KeyboardInterrupt check
​470500f	trac #19042: pyx->py

[ncohen]

Here it is.

Nathann

[jdemeyer]

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

[jdemeyer]

The correct call is

raise PackageNotFoundError("cryptominisat")

[ncohen]

Oh. Automatic error message. Cool.

[git]

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

​e9309e7

trac #19042: Wrong text

[jdemeyer]

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

[jdemeyer]

Why the # random?

sage: solver = SAT() # random

[jdemeyer]

I would prefer this to be a lazy import:

from solvers.satsolver import SAT

[git]

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

​a4ac445

trac #19042: Review

[ncohen]

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

[jdemeyer]

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.

2. Its performances -> Its performance

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

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

[git]

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

​94166b6

trac #19042: Review

[ncohen]

1. It's ugly that your ILP solver returns values as 0.0 and 1.0. It should be converted to True/False.

Right.

2. Its performances -> Its performance

Done.

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

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

Done.

[ncohen]

Thanks !