#22818 closed enhancement (fixed)
Interface cryptominisat 5
Reported by:  Thierry Monteil  Owned by:  

Priority:  major  Milestone:  sage8.0 
Component:  packages: experimental  Keywords:  days86, thursdaysbdx, sdl 
Cc:  François Bissey  Merged in:  
Authors:  Thierry Monteil  Reviewers:  Sébastien Labbé 
Report Upstream:  N/A  Work issues:  
Branch:  c22de1d (Commits, GitHub, GitLab)  Commit:  
Dependencies:  #22817  Stopgaps: 
Description (last modified by )
This ticket is a compagnon of #22817 which updates cryptominisat package to 5.0.1. Since our current cython interface does not work with cryptominisat 5, we have to rewrite the interface to use the python bindings that are now provided by cryptominisat.
The tarball is at https://github.com/msoos/cryptominisat/archive/5.0.1.tar.gz
(might have to renamedor downloaded using a browser)
Change History (70)
comment:1 Changed 6 years ago by
Description:  modified (diff) 

Keywords:  days86 added 
comment:2 Changed 6 years ago by
Branch:  → u/tmonteil/interface_cryptominisat_5 

comment:3 Changed 6 years ago by
Authors:  → Thierry Monteil 

Commit:  → afffd2a0b590c332a34788336ea6b4fcc36bc500 
comment:4 Changed 6 years ago by
Commit:  afffd2a0b590c332a34788336ea6b4fcc36bc500 → 2807be33c315b8ed1bc230f82f4c9284bc218818 

Branch pushed to git repo; I updated commit sha1. New commits:
2807be3  #22818 : let nvars() behave consistently with DIMACS convention.

comment:5 Changed 6 years ago by
Commit:  2807be33c315b8ed1bc230f82f4c9284bc218818 → 262cd467374d41040e280bab399792163459b211 

Branch pushed to git repo; I updated commit sha1. New commits:
1a480b2  #22818 : rhs option is the opposite of the former isfalse option.

1eda2df  #22818 : change in verbose output.

1c45dae  #22818 : cryptominisat does not have a maxrestarts option anymore.

262cd46  #22818 : some solvers (including recent cryptominisat) do not implement a learnt_clauses method.

comment:6 Changed 6 years ago by
Status:  new → needs_review 

comment:7 Changed 6 years ago by
Description:  modified (diff) 

comment:9 followup: 10 Changed 6 years ago by
Why two tickets then?
Can you add any/all of the following to the new module cryptominisat.py
?
# Support of Python 3 from __future__ import division, absolute_import, print_function, unicode_literals
My mac OSX is still compiling the newest version of Sage...
comment:10 followup: 12 Changed 6 years ago by
Description:  modified (diff) 

Replying to slabbe:
Why two tickets then?
Well, they do not really depend on each other, #22818 depends on #22817, but since the current interface was not working anymore, i wanted to make clear to the release manager that #22817 should not be considered until #22818 get a positive review.
Moreover, while i was pretty confident to be able to package cryptominisat 5 (and let it work with cmake), it was not clear to me whether i will be the author of the current ticket, i was first planning to contact Martin Albrecht top help there, but change after change, i could do something acceptable.
Can you add any/all of the following to the new module
cryptominisat.py
?# Support of Python 3 from __future__ import division, absolute_import, print_function, unicode_literals
I will do this.
My mac OSX is still compiling the newest version of Sage...
comment:11 Changed 6 years ago by
Commit:  262cd467374d41040e280bab399792163459b211 → 5f02977b312c5179f10b3aeec48d7f5adead45f6 

Branch pushed to git repo; I updated commit sha1. New commits:
5f02977  #22818 : implement comment 9 for Python 3 compatibility.

comment:12 Changed 6 years ago by
comment:13 Changed 6 years ago by
Keywords:  thursdaysbdx added 

On top of #22999, with OSX 10.10, sage i cryptominisat
works and I get on relevant files:
sage t long src/sage/sat/solvers/cryptominisat.py [9 tests, 1.04 s] sage t long src/sage/sat/boolean_polynomials.py [2 tests, 1.53 s] sage t long src/sage/sat/converters/polybori.py [121 tests, 1.13 s] sage t long src/sage/sat/solvers/satsolver.pyx [41 tests, 1.07 s]  All tests passed! 
comment:14 Changed 6 years ago by
Be careful that since cryptominisat is tagged as experimental
, sage t long
seems not to consider it as installed. For this, you have to change the file /build/pkgs/cryptominisat/type
to optional
(the number of tests should increase). Note also that the file rings/polynomial/multi_polynomial_sequence.py
should be tested as well.
comment:15 Changed 6 years ago by
I would suggest to move
from sage.misc.package import PackageNotFoundError
inside the except ImportError
clause.
comment:16 Changed 6 years ago by
Commit:  5f02977b312c5179f10b3aeec48d7f5adead45f6 → afe37c5c8d90707b3d3daab9af1e066177fa627f 

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:
afe37c5  #22818 : move PackageNotFoundError import as suggested in comment 15.

comment:17 Changed 6 years ago by
Commit:  afe37c5c8d90707b3d3daab9af1e066177fa627f → 3ff0423b70bdffb5121a67f9033e072bedc30382 

comment:18 Changed 6 years ago by
Ok, so I can install it:
$ sage installed ... cryptominisat...........................5.0.1 ...
but I can not run it properly:
sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat sage: CryptoMiniSat()  PackageNotFoundError Traceback (most recent call last) <ipythoninput28287720c4b48> in <module>() > 1 CryptoMiniSat() /Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat.pyc in __init__(self, verbosity, confl_limit, threads) 58 from pycryptosat import Solver 59 except ImportError: > 60 raise PackageNotFoundError("cryptominisat") 61 self._solver = Solver(verbose=int(verbosity), confl_limit=int(confl_limit), threads=int(threads)) 62 self._nvars = 0 PackageNotFoundError: the package u'cryptominisat' was not found. You can install it by running 'sage i cryptominisat' in a shell
The real error is:
sage: from pycryptosat import Solver  ImportError Traceback (most recent call last) <ipythoninput3280927e3230f> in <module>() > 1 from pycryptosat import Solver ImportError: dlopen(/Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/pycryptosat.so, 2): Library not loaded: libcryptominisat5.5.0.dylib Referenced from: /Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/pycryptosat.so Reason: image not found
comment:19 Changed 6 years ago by
...this shows that message PackageNotFoundError: the package u'cryptominisat' was not found. You can install it by running 'sage i cryptominisat' in a shell
is misleading because for me it *is* installed.
comment:20 Changed 6 years ago by
Could you go to your SAGE_LOCAL
directory and type:
find  grep cryptominisat
comment:22 followup: 24 Changed 6 years ago by
find with no argument?
$ find  grep cryptominisat usage: find [H  L  P] [EXdsx] [f path] path ... [expression] find [H  L  P] [EXdsx] f path [path ...] [expression]
comment:23 Changed 6 years ago by
Maybe this what you mean:
$ cd local/lib $ ls  grep cryp libcryptominisat5.5.0.dylib libcryptominisat5.dylib
comment:24 Changed 6 years ago by
Replying to slabbe:
find with no argument?
$ find  grep cryptominisat usage: find [H  L  P] [EXdsx] [f path] path ... [expression] find [H  L  P] [EXdsx] f path [path ...] [expression]
Who said OSX was userfriendly ?
You can try:
find name '*cryptominisat*'
and
find name '*cryptosat*'
comment:25 Changed 6 years ago by
I needed to add .
:
$ find . name '*cryptominisat*' ./bin/cryptominisat5_simple ./include/cryptominisat5 ./include/cryptominisat5/cryptominisat.h ./include/cryptominisat5/cryptominisat_c.h ./lib/cmake/cryptominisat5 ./lib/cmake/cryptominisat5/cryptominisat5Config.cmake ./lib/cmake/cryptominisat5/cryptominisat5Targetsrelwithdebinfo.cmake ./lib/cmake/cryptominisat5/cryptominisat5Targets.cmake ./lib/libcryptominisat5.5.0.dylib ./lib/libcryptominisat5.dylib ./lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat ./lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat.py ./lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat.pyc ./var/lib/sage/installed/cryptominisat5.0.1
$ find . name '*cryptosat*' ./lib/python2.7/sitepackages/pycryptosat5.0.1py2.7.egginfo ./lib/python2.7/sitepackages/pycryptosat.so
comment:26 Changed 6 years ago by
Cc:  François Bissey added 

I do not see much difference, except that my .so
files become .dylib
, which seems an OSX specificity. Not sure how this impacts things.
Does the following work: put the block
p cnf 2 3 1 0 2 0 1 2 3 0
in the file /tmp/cnf
, and run:
./bin/cryptominisat5 verb 0 /tmp/cnf
comment:27 Changed 6 years ago by
Apparently, you do not have a ./bin/cryptominisat5
file, so try instead:
./bin/cryptominisat5_simple /tmp/cnf
comment:28 Changed 6 years ago by
I get:
$ ./bin/cryptominisat5_simple verb 0 /tmp/cnf dyld: Library not loaded: libcryptominisat5.5.0.dylib Referenced from: /Users/slabbe/Applications/sagegit/local/./bin/cryptominisat5_simple Reason: image not found Trace/BPT trap: 5
Same output without verb 0
.
comment:29 followup: 31 Changed 6 years ago by
What if you do the same from a sage sh
shell ? What is the output of echo $LDFLAGS
?
comment:30 Changed 6 years ago by
OK, I can start debug your stuff. I suspect some stuff is not set as we want it in cryptominisat build system on OS X. Given the reports I am seeing, I'll want the output of
otool L lib/libcryptominisat5.5.0.dylib otool L bin/cryptominisat5_simple otool L lib/python2.7/sitepackages/pycryptosat.so
please.
comment:31 Changed 6 years ago by
Replying to tmonteil:
What if you do the same from a
sage sh
shell ?
same result
What is the output of
echo $LDFLAGS
?
$ sage sh $ echo $LDFLAGS L/Users/slabbe/Applications/sagegit/local/lib Wl,rpath,/Users/slabbe/Applications/sagegit/local/lib
comment:32 Changed 6 years ago by
$ otool L lib/libcryptominisat5.5.0.dylib lib/libcryptominisat5.5.0.dylib: libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/slabbe/Applications/sagegit/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1197.1.1) /Users/slabbe/Applications/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0) $ otool L bin/cryptominisat5_simple bin/cryptominisat5_simple: libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /usr/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.5) /Users/slabbe/Applications/sagegit/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1197.1.1) /Users/slabbe/Applications/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0) $ otool L lib/python2.7/sitepackages/pycryptosat.so lib/python2.7/sitepackages/pycryptosat.so: build/lib.macosx10.9x86_642.7/pycryptosat.so (compatibility version 0.0.0, current version 0.0.0) libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/slabbe/Applications/sagegit/local/lib/libpython2.7.dylib (compatibility version 2.7.0, current version 2.7.0) /System/Library/Frameworks/CoreFoundation.framework/Versions/A/CoreFoundation (compatibility version 150.0.0, current version 1152.0.0) /Users/slabbe/Applications/sagegit/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1213.0.0) /Users/slabbe/Applications/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)
comment:33 Changed 6 years ago by
Mirage:sagebuild fbissey$ otool L /Users/fbissey/build/sagebuild/local/bin/cryptominisat5_simple /Users/fbissey/build/sagebuild/local/bin/cryptominisat5_simple: libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /usr/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.8) /Users/fbissey/build/sagebuild/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 307.5.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.50.2) Mirage:sagebuild fbissey$ otool L /Users/fbissey/build/sagebuild/local/lib/libcryptominisat5.5.0.dylib /Users/fbissey/build/sagebuild/local/lib/libcryptominisat5.5.0.dylib: libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/fbissey/build/sagebuild/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 307.5.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.50.2)
install_name is not set. This will not work properly on OS X but the fix will belong to #22817 as it is for building cryptominisat
itself. Looking into it.
comment:34 followup: 36 Changed 6 years ago by
Documentation of INPUTS of __init__
should go into the class, because it should appear first in:
CryptoMiniSat??
You may write See documentation class for inputs
inside __init__
. There are many example like this in Sage code.
comment:35 Changed 6 years ago by
Commit:  3ff0423b70bdffb5121a67f9033e072bedc30382 → be9db62c3fb4d993f64a6678167c83038ae6c078 

Branch pushed to git repo; I updated commit sha1. New commits:
be9db62  #22818 : move documentation of INPUT from __init__ to the class, as suggested in comment:34.

comment:36 followup: 38 Changed 6 years ago by
Replying to slabbe:
Documentation of INPUTS of
__init__
should go into the class, because it should appear first in:CryptoMiniSat??You may write
See documentation class for inputs
inside__init__
. There are many example like this in Sage code.
Done. Note that actually, we should put most of the doc in the documentation od the SAT
function which is the only one imported in the namespace. Looking at it, it seems that the arguments can not be passed to the different class constructors.
comment:37 Changed 6 years ago by
Commit:  be9db62c3fb4d993f64a6678167c83038ae6c078 → 056610267dbabf730fde0469e76a13f8015559e4 

Branch pushed to git repo; I updated commit sha1. New commits:
0566102  #22818 : pass options from SAT to CruptoMiniSat.

comment:38 Changed 6 years ago by
Replying to tmonteil:
Looking at it, it seems that the arguments can not be passed to the different class constructors.
Done for cryptominisat.
It is less easy for LP solver, since SAT
will need a solver
option to decide between cryptominisat and LP, and then another solver
option to decide which MILP backend to use. Moreover, the SatLP
input tells about a solver
option, but then it does not pass it to MixedIntegerLinearProgram()
. In any case, this will be for another ticket since it does not concerns cryptominisat.
comment:39 Changed 6 years ago by
Commit:  056610267dbabf730fde0469e76a13f8015559e4 → e382251bcd94a8aade51a688bf942a4ecd7ce616 

Branch pushed to git repo; I updated commit sha1. New commits:
e382251  #22818 : remove useless import.

comment:40 Changed 6 years ago by
Still, there should be at least one EXAMPLES::
in __init__
for 100% coverage reason.
comment:41 Changed 6 years ago by
Commit:  e382251bcd94a8aade51a688bf942a4ecd7ce616 → 5236281cb06a89832b57d1a63bc78bedd0156153 

Branch pushed to git repo; I updated commit sha1. New commits:
5236281  #22818 : comment 40.

comment:42 followup: 43 Changed 6 years ago by
You should rebase the branch of this ticket on the new branch of #22817.
comment:43 Changed 6 years ago by
comment:44 Changed 6 years ago by
Commit:  5236281cb06a89832b57d1a63bc78bedd0156153 → 6ed1c73144024dd2af9f8ca88c503e2aebaaec5b 

Branch pushed to git repo; I updated commit sha1. New commits:
6e93c20  Merge branch 'develop' into package_cryptominisat_5

a8db509  patch to get install_name to be properly installed on OS X. Subtle QA for install by using GNUInstallDirs  may need more love.

fd86b98  Make sure we find sage's zlib rather the system one.

6ed1c73  Merge branch 't/22818/interface_cryptominisat_5' into t/22817/package_cryptominisat_5

comment:46 Changed 6 years ago by
On OSX 10.10, on top of #22999 and with #22818, I get:
$ sage f cryptominisat ... [cryptominisat5.0.1] Successfully installed cryptominisat5.0.1
Then, I still get:
sage: import pycryptosat Traceback (most recent call last) <ipythoninput11cca6683c235> in <module>() > 1 import pycryptosat ImportError: dlopen(/Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/pycryptosat.so, 2): Library not loaded: libcryptominisat5.5.0.dylib Referenced from: /Users/slabbe/Applications/sagegit/local/lib/python2.7/sitepackages/pycryptosat.so Reason: image not found
I do not know if there is something else I must do to install the new version of the branch? Do some rm
in the lib
folder to erase previous wrong cryptominisat lib from previous tries? Tell me if so.
Here is the output of previous commands you asked me:
$ find local name '*cryptominisat*' local/bin/cryptominisat5_simple local/include/cryptominisat5 local/include/cryptominisat5/cryptominisat.h local/include/cryptominisat5/cryptominisat_c.h local/lib/cmake/cryptominisat5 local/lib/cmake/cryptominisat5/cryptominisat5Config.cmake local/lib/cmake/cryptominisat5/cryptominisat5Targetsrelwithdebinfo.cmake local/lib/cmake/cryptominisat5/cryptominisat5Targets.cmake local/lib/libcryptominisat5.5.0.dylib local/lib/libcryptominisat5.dylib local/lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat local/lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat.py local/lib/python2.7/sitepackages/sage/sat/solvers/cryptominisat.pyc local/var/lib/sage/installed/cryptominisat5.0.1 $ find local name '*cryptosat*' local/lib/python2.7/sitepackages/pycryptosat5.0.1py2.7.egginfo local/lib/python2.7/sitepackages/pycryptosat.so
Here is the output of otool as above if this may help:
$ otool L lib/libcryptominisat5.5.0.dylib lib/libcryptominisat5.5.0.dylib: /Users/slabbe/Applications/sagegit/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/slabbe/Applications/sagegit/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1197.1.1) /Users/slabbe/Applications/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0) $ otool L bin/cryptominisat5_simple bin/cryptominisat5_simple: /Users/slabbe/Applications/sagegit/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/slabbe/Applications/sagegit/local/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.8) /Users/slabbe/Applications/sagegit/local/lib/libm4ri0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1197.1.1) /Users/slabbe/Applications/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0) $ otool L lib/python2.7/sitepackages/pycryptosat.so lib/python2.7/sitepackages/pycryptosat.so: build/lib.macosx10.9x86_642.7/pycryptosat.so (compatibility version 0.0.0, current version 0.0.0) libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/slabbe/Applications/sagegit/local/lib/libpython2.7.dylib (compatibility version 2.7.0, current version 2.7.0) /System/Library/Frameworks/CoreFoundation.framework/Versions/A/CoreFoundation (compatibility version 150.0.0, current version 1152.0.0) /Users/slabbe/Applications/sagegit/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1213.0.0) /Users/slabbe/Applications/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)
comment:47 followup: 48 Changed 6 years ago by
lib/python2.7/sitepackages/pycryptosat.so
is not normal. My install shows
Mirage:sagebuild fbissey$ otool L local/lib/python2.7/sitepackages/pycryptosat.so local/lib/python2.7/sitepackages/pycryptosat.so: build/lib.macosx10.9x86_642.7/pycryptosat.so (compatibility version 0.0.0, current version 0.0.0) /Users/fbissey/build/sagebuild/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/fbissey/build/sagebuild/local/lib/libpython2.7.dylib (compatibility version 2.7.0, current version 2.7.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1238.60.2) /System/Library/Frameworks/CoreFoundation.framework/Versions/A/CoreFoundation (compatibility version 150.0.0, current version 1349.8.0) /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 307.5.0)
For some reason you appear to have an old install in the python folder. I didn't have to do any rm
but removing that file before reinstalling may be something to try.
comment:48 followup: 49 Changed 6 years ago by
I did:
rm local/lib/python2.7/sitepackages/pycryptosat.so sage f cryptominisat
I get:
$ otool L local/lib/python2.7/sitepackages/pycryptosat.so local/lib/python2.7/sitepackages/pycryptosat.so: build/lib.macosx10.9x86_642.7/pycryptosat.so (compatibility version 0.0.0, current version 0.0.0) /Users/slabbe/Applications/sagegit/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0) /Users/slabbe/Applications/sagegit/local/lib/libpython2.7.dylib (compatibility version 2.7.0, current version 2.7.0) /System/Library/Frameworks/CoreFoundation.framework/Versions/A/CoreFoundation (compatibility version 150.0.0, current version 1152.0.0) /Users/slabbe/Applications/sagegit/local/lib/libstdc++.6.dylib (compatibility version 7.0.0, current version 7.20.0) /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1213.0.0) /Users/slabbe/Applications/sagegit/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)
and now:
sage: import pycryptosat sage: from pycryptosat import Solver sage: s = Solver() sage: s.add_clause((1r,1r,1r,1r,1r)) sage: s.solve() (True, (None, False))
which is great! Should I sage f c cryptominisat
now?
comment:49 followup: 50 Changed 6 years ago by
Replying to slabbe:
I did:
rm local/lib/python2.7/sitepackages/pycryptosat.so sage f cryptominisatand now:
sage: import pycryptosat sage: from pycryptosat import Solver sage: s = Solver() sage: s.add_clause((1r,1r,1r,1r,1r)) sage: s.solve() (True, (None, False))
Looks good. I am not sure why the old one stuck around. It must have tricked cmake in being up to date.
Should I
sage f c cryptominisat
now?
????
comment:50 Changed 6 years ago by
comment:51 Changed 6 years ago by
It could be a dependency of #218017, which is about building cryptominisat 5. Also, if everything builds fine on supported archs, we could move crymtominisat
from experimental to optional (in particular this avoids the need to modify its type
by hand when running doctests).
Regarding sage f c cryptominisat
, there is no selftests yet, so it will make no difference with sage f cryptominisat
(though it is always a good idea when reviewing a packaging ticket).
comment:52 Changed 6 years ago by
That said, i would really like to have cryptominisat 5 entering Sage 8.0, since i rely on sat solvers for some tutorials, where some people run the 32bit Sage Debian Live USB.
comment:53 Changed 6 years ago by
On osx 10.10 with 8.0.beta7 + #22999 + #22818 + this change:

build/pkgs/cryptominisat/type
diff git a/build/pkgs/cryptominisat/type b/build/pkgs/cryptominisat/type index 9839eb2..134d9bc 100644
a b 1 experimental1 optional
the command:
sage t long src/sage/sat/solvers/cryptominisat.py src/sage/sat/boolean_polynomials.py src/sage/sat/converters/polybori.py src/sage/sat/solvers/satsolver.pyx src/sage/rings/polynomial/multi_polynomial_sequence.py
gives
Using optional=4ti2,atlas,cbc,ccache,cryptominisat,latte_int,lidia,lrslib,mpir,pandoc_attributes,pandocfilters,python2,rst2ipynb,sage Doctesting 5 files. sage t long src/sage/sat/solvers/cryptominisat.py [49 tests, 1.16 s] sage t long src/sage/sat/boolean_polynomials.py [27 tests, 1.98 s] sage t long src/sage/sat/converters/polybori.py [121 tests, 1.21 s] sage t long src/sage/sat/solvers/satsolver.pyx [42 tests, 1.20 s] sage t long src/sage/rings/polynomial/multi_polynomial_sequence.py [237 tests, 11.70 s]  All tests passed! 
comment:54 Changed 6 years ago by
Reviewers:  → Sébastien Labbé 

To me this is good to go and I am ok with changing type to optional.
I did not check that documentation builds fine though (overnight my computer will work on #22999 instead).
comment:55 Changed 6 years ago by
I builded the documentation but I can't find cryptominisat doc in the reference manual:
sage/sat/solvers/cryptominisat
should be listed in src/doc/en/reference/sat/index.rst
in the following section:
Details on Specific Solvers ^^^^^^^^^^^^^^^^^^^^^^^^^^^ .. toctree:: :maxdepth: 1 sage/sat/solvers/satsolver sage/sat/solvers/dimacs sage/sat/solvers/sat_lp .. optional  cryptominisat .. sage/sat/solvers/cryptominisat/cryptominisat .. sage/sat/solvers/cryptominisat/solverconf
In the same file, is the following paragraph still up to date?
Furthermore, Sage provides a C++ interface to the *CryptoMiniSat* [CMS]_ SAT solver which can be used interchangably with DIMACSbased solvers, but also provides advanced features. For this last solver, the optional CryptoMiniSat package must be installed, this can be accomplished by typing the following in the shell:: sage i cryptominisat sagelib
In cryptominisat.py
, it should be ``
instead of '
:
 'confl_limit'  an integer (default: ``None``). Abort after this many conflicts. If set to ``None``, never aborts.
Similar problem some lines below (I think this one should break the doc building) :
 ``filename''  ...
In input blocks, 
should be changed to 
to adhere to the sage convention (several instances):
  ``decision``  accepted for compatibility with other solvers, ignored. +  ``decision``  accepted for compatibility with other solvers, ignored.
Remove the empty line here:
+ sage: from sage.sat.solvers.cryptominisat import CryptoMiniSat + sage: solver = CryptoMiniSat() # optional  cryptominisat + + sage: solver.nvars() # optional  cryptominisat + 0
Finaly, I would replace the top paragraph:
This solver relies on Python bindings provided by upstream cryptominisat, and replaces the cython interface (written by Martin Albrecht in 2012) that does not work with recent versions of cryptominisat anymore.  The ``cryptominisat`` package should be installed on your Sage installation.  AUTHORS:   Thierry Monteil (2017): first version +This solver relies on Python bindings provided by upstream cryptominisat. + +The ``cryptominisat`` package should be installed on your Sage installation. + +AUTHORS: + + Thierry Monteil (2017): replaced the cython interface that does not work + with version >=5.0 of cryptominisat anymore. + Martin Albrecht (2012): first version
Finally, no dot in the title:
CryptoMiniSat Solver. +CryptoMiniSat Solver
comment:56 Changed 6 years ago by
Status:  needs_review → needs_work 

comment:57 Changed 6 years ago by
Commit:  6ed1c73144024dd2af9f8ca88c503e2aebaaec5b → c9dd3554d82e640ff88eb435d51a823ad6608ac4 

comment:58 Changed 6 years ago by
Status:  needs_work → needs_review 

Thanks for the hints. I applied them quite blindly since i do not have enough RAM to build de doc anymore.
comment:59 Changed 5 years ago by
Great. I managed to build the documentation without errors. I managed to see the Cryptominisat documentation in the reference manual. Every things is okay. Only one problem with the following paragraph which
 misses a
::
at the end,  misses a punctuation before
Note that
 misses the end of the last sentence?
Note that in cryptominisat, the DIMACS standard format is augmented with the following extension: having an ``x`` in front of a line makes that line an XOR clause i Note that cryptominisat has its own
comment:60 Changed 5 years ago by
Status:  needs_review → needs_work 

comment:61 Changed 5 years ago by
Commit:  c9dd3554d82e640ff88eb435d51a823ad6608ac4 → c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4 

Branch pushed to git repo; I updated commit sha1. New commits:
c22de1d  #22818 : comment 59.

comment:62 Changed 5 years ago by
Status:  needs_work → needs_review 

Sorry, it was an editing noise, the right sentences ends brefore, see https://www.msoos.org/xorclauses/
comment:63 Changed 5 years ago by
Status:  needs_review → positive_review 

comment:64 Changed 5 years ago by
Thanks for all the review, i am so happy that cryptominisat can now be installed on 32bit machines. BTW, shall we move the package from experimental to optional ?
comment:66 Changed 5 years ago by
Replying to slabbe:
I think yes. Maybe in another ticket.
OK, let us not miss the 8.0 with a new round for that.
comment:68 Changed 5 years ago by
Branch:  u/tmonteil/interface_cryptominisat_5 → c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4 

Resolution:  → fixed 
Status:  positive_review → closed 
comment:69 Changed 5 years ago by
Commit:  c22de1d4fcce1be2ba2c0c40b096b99079c5e9a4 

See #23351 for a follow up ticket.
comment:70 Changed 3 years ago by
Keywords:  sdl added 

New commits:
#22817 : package cryptominisat 5.0.1
Merge branch 'u/tmonteil/package_cryptominisat_5' of trac.sagemath.org:sage into HEAD
#22818 : remove old cryptominisat directory.
#22818 : update module_list.py.
#22818 : new cryptominisat interface.