Interface cryptominisat 5

[Thierry Monteil]

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 renamed---or downloaded using a browser)

[Thierry Monteil]

New commits:

​67f23e7	#22817 : package cryptominisat 5.0.1
​756251f	Merge branch 'u/tmonteil/package_cryptominisat_5' of trac.sagemath.org:sage into HEAD
​f66caff	#22818 : remove old cryptominisat directory.
​dc9b158	#22818 : update module_list.py.
​afffd2a	#22818 : new cryptominisat interface.

[git]

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

​2807be3

#22818 : let nvars() behave consistently with DIMACS convention.

[git]

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.

[Dima Pasechnik]

works on freebsd/clang, which is a good approx of OSX.

[Sébastien Labbé]

#22818 and #22817 depend on each other.

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

[Thierry Monteil]

Replying to slabbe:

#22818 and #22817 depend on each other.

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

[git]

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

​5f02977

#22818 : implement comment 9 for Python 3 compatibility.

[Thierry Monteil]

Replying to tmonteil:

Replying to slabbe:

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.

Done.

[Sébastien Labbé]

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!
----------------------------------------------------------------------

[Thierry Monteil]

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.

[Sébastien Labbé]

I would suggest to move

        from sage.misc.package import PackageNotFoundError

inside the except ImportError clause.

[git]

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.

[git]

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

​5f02977	#22818 : implement comment 9 for Python 3 compatibility.
​3ff0423	#22818 : move PackageNotFoundError import as suggested in comment 15.

[Sébastien Labbé]

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)
<ipython-input-2-8287720c4b48> in <module>()
----> 1 CryptoMiniSat()

/Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/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)
<ipython-input-3-280927e3230f> in <module>()
----> 1 from pycryptosat import Solver

ImportError: dlopen(/Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/pycryptosat.so, 2): Library not loaded: libcryptominisat5.5.0.dylib
  Referenced from: /Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/pycryptosat.so
  Reason: image not found

[Sébastien Labbé]

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

[Thierry Monteil]

Could you go to your SAGE_LOCAL directory and type:

find | grep cryptominisat

[Thierry Monteil]

as well as:

 find | grep cryptosat

[Sébastien Labbé]

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]

[Sébastien Labbé]

Maybe this what you mean:

$ cd local/lib
$ ls | grep cryp
libcryptominisat5.5.0.dylib
libcryptominisat5.dylib

[Thierry Monteil]

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 user-friendly ?

You can try:

find -name '*cryptominisat*'

and

find -name '*cryptosat*'

[Sébastien Labbé]

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/cryptominisat5Targets-relwithdebinfo.cmake
./lib/cmake/cryptominisat5/cryptominisat5Targets.cmake
./lib/libcryptominisat5.5.0.dylib
./lib/libcryptominisat5.dylib
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.py
./lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.pyc
./var/lib/sage/installed/cryptominisat-5.0.1

 $ find . -name '*cryptosat*'
./lib/python2.7/site-packages/pycryptosat-5.0.1-py2.7.egg-info
./lib/python2.7/site-packages/pycryptosat.so

[Thierry Monteil]

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

[Thierry Monteil]

Apparently, you do not have a ./bin/cryptominisat5 file, so try instead:

./bin/cryptominisat5_simple /tmp/cnf

[Sébastien Labbé]

I get:

$ ./bin/cryptominisat5_simple --verb 0 /tmp/cnf
dyld: Library not loaded: libcryptominisat5.5.0.dylib
  Referenced from: /Users/slabbe/Applications/sage-git/local/./bin/cryptominisat5_simple
  Reason: image not found
Trace/BPT trap: 5

Same output without --verb 0.

[Thierry Monteil]

What if you do the same from a sage -sh shell ? What is the output of echo $LDFLAGS ?

[François Bissey]

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/site-packages/pycryptosat.so

please.

[Sébastien Labbé]

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/sage-git/local/lib -Wl,-rpath,/Users/slabbe/Applications/sage-git/local/lib

[Sébastien Labbé]

$ 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/sage-git/local/lib/libm4ri-0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0)
	/Users/slabbe/Applications/sage-git/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/sage-git/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/sage-git/local/lib/libm4ri-0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0)
	/Users/slabbe/Applications/sage-git/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/sage-git/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)

$ otool -L lib/python2.7/site-packages/pycryptosat.so
lib/python2.7/site-packages/pycryptosat.so:
	build/lib.macosx-10.9-x86_64-2.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/sage-git/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/sage-git/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/sage-git/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)

[François Bissey]

Mirage:sage-build fbissey$ otool -L /Users/fbissey/build/sage-build/local/bin/cryptominisat5_simple
/Users/fbissey/build/sage-build/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/sage-build/local/lib/libm4ri-0.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:sage-build fbissey$ otool -L /Users/fbissey/build/sage-build/local/lib/libcryptominisat5.5.0.dylib
/Users/fbissey/build/sage-build/local/lib/libcryptominisat5.5.0.dylib:
	libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
	/Users/fbissey/build/sage-build/local/lib/libm4ri-0.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.

[Sébastien Labbé]

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.

[git]

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.

[Thierry Monteil]

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.

[git]

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

​0566102

#22818 : pass options from SAT to CruptoMiniSat.

[Thierry Monteil]

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.

[git]

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

​e382251

#22818 : remove useless import.

[Sébastien Labbé]

Still, there should be at least one EXAMPLES:: in __init__ for 100% coverage reason.

[git]

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

​5236281

#22818 : comment 40.

[François Bissey]

You should rebase the branch of this ticket on the new branch of #22817.

[Thierry Monteil]

Replying to fbissey:

You should rebase the branch of this ticket on the new branch of #22817.

Sure, i must first compile the changes made on #22817, and test it.

[git]

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

[Thierry Monteil]

Done.

[Sébastien Labbé]

On OSX 10.10, on top of #22999 and with #22818, I get:

$ sage -f cryptominisat
...
[cryptominisat-5.0.1] Successfully installed cryptominisat-5.0.1

Then, I still get:

sage: import pycryptosat
Traceback (most recent call last)
<ipython-input-1-1cca6683c235> in <module>()
----> 1 import pycryptosat

ImportError: dlopen(/Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/pycryptosat.so, 2): Library not loaded: libcryptominisat5.5.0.dylib
  Referenced from: /Users/slabbe/Applications/sage-git/local/lib/python2.7/site-packages/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/cryptominisat5Targets-relwithdebinfo.cmake
local/lib/cmake/cryptominisat5/cryptominisat5Targets.cmake
local/lib/libcryptominisat5.5.0.dylib
local/lib/libcryptominisat5.dylib
local/lib/python2.7/site-packages/sage/sat/solvers/cryptominisat
local/lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.py
local/lib/python2.7/site-packages/sage/sat/solvers/cryptominisat.pyc
local/var/lib/sage/installed/cryptominisat-5.0.1

$ find local -name '*cryptosat*'
local/lib/python2.7/site-packages/pycryptosat-5.0.1-py2.7.egg-info
local/lib/python2.7/site-packages/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/sage-git/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
	/Users/slabbe/Applications/sage-git/local/lib/libm4ri-0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0)
	/Users/slabbe/Applications/sage-git/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/sage-git/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/sage-git/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
	/Users/slabbe/Applications/sage-git/local/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.8)
	/Users/slabbe/Applications/sage-git/local/lib/libm4ri-0.0.20140914.dylib (compatibility version 0.0.0, current version 0.0.0)
	/Users/slabbe/Applications/sage-git/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/sage-git/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)

$ otool -L lib/python2.7/site-packages/pycryptosat.so
lib/python2.7/site-packages/pycryptosat.so:
	build/lib.macosx-10.9-x86_64-2.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/sage-git/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/sage-git/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/sage-git/local/lib/libgcc_s.1.dylib (compatibility version 1.0.0, current version 1.0.0)

[François Bissey]

lib/python2.7/site-packages/pycryptosat.so is not normal. My install shows

Mirage:sage-build fbissey$ otool -L local/lib/python2.7/site-packages/pycryptosat.so 
local/lib/python2.7/site-packages/pycryptosat.so:
	build/lib.macosx-10.9-x86_64-2.7/pycryptosat.so (compatibility version 0.0.0, current version 0.0.0)
	/Users/fbissey/build/sage-build/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
	/Users/fbissey/build/sage-build/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 re-installing may be something to try.

[Sébastien Labbé]

I did:

rm local/lib/python2.7/site-packages/pycryptosat.so
sage -f cryptominisat

I get:

$ otool -L local/lib/python2.7/site-packages/pycryptosat.so
local/lib/python2.7/site-packages/pycryptosat.so:
	build/lib.macosx-10.9-x86_64-2.7/pycryptosat.so (compatibility version 0.0.0, current version 0.0.0)
	/Users/slabbe/Applications/sage-git/local/lib/libcryptominisat5.5.0.dylib (compatibility version 5.0.0, current version 5.0.0)
	/Users/slabbe/Applications/sage-git/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/sage-git/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/sage-git/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?

[François Bissey]

Replying to slabbe:

I did:

rm local/lib/python2.7/site-packages/pycryptosat.so
sage -f cryptominisat

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))

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?

????

[Sébastien Labbé]

Should I sage -f -c cryptominisat now?

????

Indeed, I was confusing with #22999.

Should #22999 be a dependency of #22818, since it is now necessary for some versions of osx?

[Thierry Monteil]

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 self-tests yet, so it will make no difference with sage -f cryptominisat (though it is always a good idea when reviewing a packaging ticket).

[Thierry Monteil]

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.

[Sébastien Labbé]

On osx 10.10 with 8.0.beta7 + #22999 + #22818 + this change:

build/pkgs/cryptominisat/type

@@ -1 @@
-experimental
+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!
----------------------------------------------------------------------

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

[Sébastien Labbé]

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 DIMACS-based 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

[git]

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

​9593ce6	Merge
​c9dd355	#22818 : comment 55.

[Thierry Monteil]

Thanks for the hints. I applied them quite blindly since i do not have enough RAM to build de doc anymore.

[Sébastien Labbé]

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 

[git]

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

​c22de1d

#22818 : comment 59.

[Thierry Monteil]

Sorry, it was an editing noise, the right sentences ends brefore, see ​https://www.msoos.org/xor-clauses/

[Thierry Monteil]

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 ?

[Sébastien Labbé]

I think yes. Maybe in another ticket.

[Thierry Monteil]

Replying to slabbe:

I think yes. Maybe in another ticket.

OK, let us not miss the 8.0 with a new round for that.

[Thierry Monteil]

This is now #23219.

[Sébastien Labbé]

See #23351 for a follow up ticket.