Opened 7 years ago
Closed 4 years ago
#15674 closed enhancement (wontfix)
Update cryptominisat
Reported by: | equaeghe | Owned by: | |
---|---|---|---|
Priority: | minor | Milestone: | sage-duplicate/invalid/wontfix |
Component: | packages: optional | Keywords: | |
Cc: | malb, mmezzarobba | Merged in: | |
Authors: | Reviewers: | ||
Report Upstream: | N/A | Work issues: | |
Branch: | u/malb/ticket-15674-cryptominisat (Commits) | Commit: | e9b47aac79b7f20af9bfdae89aa99175fd7773d1 |
Dependencies: | #19298 | Stopgaps: |
Description
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
Change History (27)
comment:1 Changed 7 years ago by
- Cc malb added
comment:2 Changed 7 years ago by
- Branch set to u/malb/ticket-15674-cryptominisat
- Commit set to a19676ff338523cb17e9f46f3797e48baf562683
comment:3 follow-up: ↓ 5 Changed 7 years ago by
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)
comment:4 Changed 7 years ago by
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
comment:5 in reply to: ↑ 3 ; follow-up: ↓ 6 Changed 7 years ago by
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?
comment:6 in reply to: ↑ 5 Changed 7 years ago by
Replying to equaeghe:
Perhaps I should [...] ask upstream to provide a release of 2.9.6?
comment:7 Changed 7 years ago by
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.
comment:8 Changed 7 years ago by
Excellent! I'll ask on [sage-devel] about C++11.
comment:9 Changed 7 years ago by
I created a new ticket which merely integrates CryptoMiniSat? properly into the new SPKG structure at #15723.
comment:10 Changed 7 years ago by
- Milestone changed from sage-6.1 to sage-6.2
comment:11 Changed 7 years ago by
- Commit changed from a19676ff338523cb17e9f46f3797e48baf562683 to e9b47aac79b7f20af9bfdae89aa99175fd7773d1
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
|
comment:12 Changed 7 years ago by
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/
comment:13 Changed 7 years ago by
There are two holdups. CryptoMiniSat 4 uses
- cmake and not autotools, but Sage does not include cmake
- more of Boost than Sage includes.
comment:14 Changed 7 years ago by
- Milestone changed from sage-6.2 to sage-6.3
comment:15 Changed 6 years ago by
- Milestone changed from sage-6.3 to sage-6.4
comment:16 Changed 6 years ago by
- Cc mmezzarobba added
comment:17 Changed 5 years ago by
- Dependencies set to #19298
comment:18 Changed 5 years ago by
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.
comment:19 Changed 5 years ago by
- Milestone changed from sage-6.4 to sage-6.9
- Summary changed from Update cryptominisat (optional package) from CryptoMiniSat version 2.9.6 to version 3+ to Update cryptominisat
comment:20 Changed 5 years ago by
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 ? :)
comment:21 follow-up: ↓ 22 Changed 5 years ago by
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?
comment:22 in reply to: ↑ 21 Changed 5 years ago by
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.
comment:23 Changed 5 years ago by
Hi Máté, how much of comment:7 is still current? IIRC my pull request does most of the work for that.
comment:24 Changed 5 years ago by
Just advertising here that I wrote a 'cheap' support for SAT in standard sage at #19042 (needs review)
comment:25 Changed 5 years ago by
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 :)
comment:26 Changed 4 years ago by
- Milestone changed from sage-6.9 to sage-duplicate/invalid/wontfix
- Status changed from new to needs_review
Superseded by #22817 (cryptominisat 5).
comment:27 Changed 4 years ago by
- Resolution set to wontfix
- Status changed from needs_review to closed
Goes without saying.
I've imported cryptominisat-2.9.6, the update to 3.x is next.
New commits:
adding cryptominisat 2.9.6 to build/pkgs