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:  sage6.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
 Branch set to public/19042
 Cc tmonteil added
 Commit set to 3a548d9882d963d9740d57d7095ad3ac4df24e03
 Status changed from new to needs_review
comment:2 Changed 3 years ago by
 Summary changed from Default SAT solver in Sage to Fallback SAT solver in Sage
comment:3 Changed 3 years ago by
Since cryptominisat is optional for (much) more than one year, why not make it standard ?
comment:4 Changed 3 years ago by
Check the license and if it is compatible write to sagedevel. It may still be useful to have a LP backend to doublecheck results.
comment:5 followup: ↓ 6 Changed 3 years ago by
Why call it "LP" when it's an ILP?
comment:6 in reply to: ↑ 5 Changed 3 years ago by
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
 Commit changed from 3a548d9882d963d9740d57d7095ad3ac4df24e03 to eb01119cd733a39fd72aabfc7feb2114115d1526
Branch pushed to git repo; I updated commit sha1. New commits:
eb01119  trac #19042: Merged with 6.9.rc0

comment:8 followup: ↓ 10 Changed 3 years ago by
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
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 ; followup: ↓ 11 Changed 3 years ago by
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
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) <ipythoninput8257eb3253d78> in <module>() > 1 alarm(RealNumber('0.2')); cms() /usr/local/src/sageconfig/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/sageconfig/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
 Commit changed from eb01119cd733a39fd72aabfc7feb2114115d1526 to 470500f86e188164d23cb5c417ebecbab10f43cc
comment:13 Changed 3 years ago by
Here it is.
Nathann
comment:14 Changed 3 years ago by
I asked #418 about the KeyboardInterrupt
, in case somebody remembers there.
comment:15 Changed 3 years ago by
The correct call is
raise PackageNotFoundError("cryptominisat")
comment:16 Changed 3 years ago by
 Status changed from needs_review to needs_work
comment:17 Changed 3 years ago by
Oh. Automatic error message. Cool.
comment:18 Changed 3 years ago by
 Commit changed from 470500f86e188164d23cb5c417ebecbab10f43cc to e9309e7c826982f251825f1c8f959723daf0ab35
Branch pushed to git repo; I updated commit sha1. New commits:
e9309e7  trac #19042: Wrong text

comment:19 Changed 3 years ago by
 Status changed from needs_work to needs_review
comment:20 Changed 3 years ago by
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
Why the # random
?
sage: solver = SAT() # random
comment:22 Changed 3 years ago by
I would prefer this to be a lazy import:
from solvers.satsolver import SAT
comment:23 Changed 3 years ago by
 Commit changed from e9309e7c826982f251825f1c8f959723daf0ab35 to a4ac4458b8f5aa633047299f9db2269fdf4e74ca
Branch pushed to git repo; I updated commit sha1. New commits:
a4ac445  trac #19042: Review

comment:24 Changed 3 years ago by
About random: I wrongly believed that Cryptominisat always printed information when instanciated.
comment:25 followup: ↓ 27 Changed 3 years ago by
 Reviewers set to Jeroen Demeyer
 Status changed from needs_review to needs_work
A few more details:
 It's ugly that your ILP solver returns values as
0.0
and1.0
. It should be converted toTrue
/False
.
Its performances
>Its performance
cryptominisat_available = True
>solver = 'cryptominisat'
andcryptominisat_available = False
>solver = 'LP'
. That's a lot cleaner: you can remove thesolver is None
checks.
 Please fix the
deicison
typo also insrc/sage/sat/converters/polybori.py
comment:26 Changed 3 years ago by
 Commit changed from a4ac4458b8f5aa633047299f9db2269fdf4e74ca to 94166b67c1a2e0a06770b7e7fb6acffd71d480f6
Branch pushed to git repo; I updated commit sha1. New commits:
94166b6  trac #19042: Review

comment:27 in reply to: ↑ 25 Changed 3 years ago by
 Status changed from needs_work to needs_review
 It's ugly that your ILP solver returns values as
0.0
and1.0
. It should be converted toTrue
/False
.
Right.
Its performances
>Its performance
Done.
cryptominisat_available = True
>solver = 'cryptominisat'
andcryptominisat_available = False
>solver = 'LP'
. That's a lot cleaner: you can remove thesolver is None
checks.
I'm an idiot.
 Please fix the
deicison
typo also insrc/sage/sat/converters/polybori.py
Done.
comment:28 Changed 3 years ago by
 Status changed from needs_review to positive_review
comment:29 Changed 3 years ago by
Thanks !
comment:30 Changed 3 years ago by
 Branch changed from public/19042 to 94166b67c1a2e0a06770b7e7fb6acffd71d480f6
 Resolution set to fixed
 Status changed from positive_review to closed
New commits:
trac #19042: Default SAT solver in Sage