Update cryptominisat

[equaeghe]

Currently, the optional cryptominisat package spkg refers to CryptoMiniSat? 2.9.6. Currently, CryptoMiniSat? version 3.2 is released. Actually, there is no release (git tag) for versions < 3. To include this package in sage-on-gentoo, it is convenient to be able to refer to a release.

So, both 'to stay current' and for practical reasons (for Gentoo Linux developers), I would like to request that the cryptominisat package be updated. (And understand that time constraints may not allow for this.)

Links:

• CryptoMiniSat? git repo: ​https://github.com/msoos/cryptominisat/
• cryptominisat spkg hg repo: ​https://bitbucket.org/malb/cryptominisat-spkg
• sage-on-gentoo git repo: ​https://github.com/cschwan/sage-on-gentoo
• sage reference mention: ​http://www.sagemath.org/doc/reference/sat

[Martin Albrecht]

I've imported cryptominisat-2.9.6, the update to 3.x is next.

---

New commits:

​a19676f

adding cryptominisat 2.9.6 to build/pkgs

[Martin Albrecht]

Looks like it isn't going to be that straight forward:

CryptoMiniSat needs

• CMake (we don't have that)
• libz (we have that)
• libboost (we have a cropped version, possibly not all we need)
• libboost-program-options (we don't have that)
• m4ri from GITHUB (we have that)

​https://github.com/msoos/cryptominisat/blob/master/INSTALL

[Nathann Cohen]

And I read that yesterday which is not a problem for me but may be one for you :

​http://www.msoos.org/cryptominisat-3/ Is CryptoMiniSat? 3 tuned to solve cryptographic instances? No. In fact, it can’t process XOR clauses natively so maybe CryptoMiniSat? 2 would be a better choice for those types of instances.

By the way, I was impressed at how fast Cryptominisat solved a graph problem I had at that time. Too bad I cannot easily say that the sum of 50 bolean variables should be equal to 10 with SAT clauses T_T

Nathann

[equaeghe]

Replying to malb:

Looks like it isn't going to be that straight forward:

Perhaps I should, to solve the "sage-on-gentoo wants releases" problem until the dependency problem can be sorted out, ask upstream to provide a release of 2.9.6?

[equaeghe]

Replying to equaeghe:

Perhaps I should [...] ask upstream to provide a release of 2.9.6?

Done: ​https://github.com/msoos/cryptominisat/issues/149

[Mate Soos]

I'm the author of CryptoMiniSat?. The 3.x series doesn't support XOR naively. It should be much faster on many instances, though, and has substantially improved in stability and with 3.4 a much cleaner interface too. I am planning on a python interface, too for 3.4 which should make things drag-and-drop from your perspective. See ​https://github.com/netom/satispy for an example.

As a library, 3.x it doesn't need boost, zlib, mysql or m4ri, but needs C++11. It's 2014, so it's been 3 years now, I hope that's okay :S C++11 substantially increases portability due to uint32_t/uint64_t and threads being part of C++11, not to mention the readability of the code. As for cmake, I think I'll make a simple automake version as well. I'll update this ticket when 3.4 is released.

BTW, 3.x supports DRUP (​http://www.cs.utexas.edu/~marijn/drup/), which means UNSAT can be verified(!) and potentially traced back to the exact clauses causing UNSAT. This means that the solver can give more meaningful feedback than just a 1-bit value (UNSAT) in case it's not SAT -- in which case it gives a satisfying assignment, a very helpful trace.

[Martin Albrecht]

Excellent! I'll ask on [sage-devel] about C++11.

[Martin Albrecht]

I created a new ticket which merely integrates CryptoMiniSat? properly into the new SPKG structure at #15723.

[git]

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

​d19d095	adding cryptominisat 2.9.6 to build/pkgs
​85f4b71	removing changelog from SPKG.txt, using upstream tarball directly
​791530f	cmsat-VERSION -> cryptominisat-VERSION
​e9b47aa	Merge branch 'u/malb/ticket-15674-cryptominisat' of trac.sagemath.org:sage into cryptominisat

[Martin Albrecht]

CryptoMiniSat? 4.0 is out and it support for XOR clauses was added back. Hence, we should be able to just upgrade: ​http://www.msoos.org/2014/04/cryptominisat-4-released/

[Martin Albrecht]

There are two holdups. CryptoMiniSat 4 uses

• cmake and not autotools, but Sage does not include cmake
• more of Boost than Sage includes.

[Mate Soos]

Actually, latest release would be best (4.5+) :) It's almost fully backward-compatible with the old one, so all should easy. By the way, CryptoMiniSat? now has a python interface, you can even use that.

[Martin Albrecht]

Hi Mate, IIRC the hold up was because of missing autotools support. Maybe it's time to revive ​https://github.com/msoos/cryptominisat/pull/196 ? :)

[Mate Soos]

Wow. Can't cmake be used? Does it have to have autotools? I mean, it's over 1000 lines of code for the cmake. To make that feature-compatible with autotools it'd be about a month of work. That's a lot. Can cmake be hooked in somehow?

[Jeroen Demeyer]

Replying to msoos:

Wow. Can't cmake be used? Does it have to have autotools? I mean, it's over 1000 lines of code for the cmake. To make that feature-compatible with autotools it'd be about a month of work. That's a lot. Can cmake be hooked in somehow?

Well, there is an experimental cmake package for Sage. So, if you're willing to "downgrade" cryptominisat to experimental, you can use it.

[Martin Albrecht]

Hi Máté, how much of comment:7 is still current? IIRC my pull request does most of the work for that.

[Nathann Cohen]

Just advertising here that I wrote a 'cheap' support for SAT in standard sage at #19042 (needs review)

[Mate Soos]

Well... I can create an autotools-based package. I'll do that in the coming days. But I will not release this to the general public, because re-writing all the build system for autotools and making sure it works for both is simply too much work. I hope this middle ground is good enough :)

And thanks for your pull request! Based on that I should be able to create a good enough autotools-based release :)

[François Bissey]

Superseded by #22817 (cryptominisat 5).

[Erik Bray]

Goes without saying.