Opened 7 years ago
Closed 4 years ago
#15674 closed enhancement (wontfix)
Update cryptominisat
Reported by:  equaeghe  Owned by:  

Priority:  minor  Milestone:  sageduplicate/invalid/wontfix 
Component:  packages: optional  Keywords:  
Cc:  malb, mmezzarobba  Merged in:  
Authors:  Reviewers:  
Report Upstream:  N/A  Work issues:  
Branch:  u/malb/ticket15674cryptominisat (Commits, GitHub, GitLab)  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 sageongentoo, 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/cryptominisatspkg
 sageongentoo git repo: https://github.com/cschwan/sageongentoo
 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/ticket15674cryptominisat
 Commit set to a19676ff338523cb17e9f46f3797e48baf562683
comment:3 followup: ↓ 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)
 libboostprogramoptions (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/cryptominisat3/ 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 ; followup: ↓ 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 "sageongentoo 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 draganddrop 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 1bit 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 [sagedevel] 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 sage6.1 to sage6.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  cmsatVERSION > cryptominisatVERSION

e9b47aa  Merge branch 'u/malb/ticket15674cryptominisat' 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/cryptominisat4released/
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 sage6.2 to sage6.3
comment:15 Changed 7 years ago by
 Milestone changed from sage6.3 to sage6.4
comment:16 Changed 6 years ago by
 Cc mmezzarobba added
comment:17 Changed 6 years ago by
 Dependencies set to #19298
comment:18 Changed 6 years ago by
Actually, latest release would be best (4.5+) :) It's almost fully backwardcompatible 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 6 years ago by
 Milestone changed from sage6.4 to sage6.9
 Summary changed from Update cryptominisat (optional package) from CryptoMiniSat version 2.9.6 to version 3+ to Update cryptominisat
comment:20 Changed 6 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 followup: ↓ 22 Changed 6 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 featurecompatible 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 6 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 featurecompatible 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 6 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 6 years ago by
Just advertising here that I wrote a 'cheap' support for SAT in standard sage at #19042 (needs review)
comment:25 Changed 6 years ago by
Well... I can create an autotoolsbased package. I'll do that in the coming days. But I will not release this to the general public, because rewriting 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 autotoolsbased release :)
comment:26 Changed 4 years ago by
 Milestone changed from sage6.9 to sageduplicate/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 cryptominisat2.9.6, the update to 3.x is next.
New commits:
adding cryptominisat 2.9.6 to build/pkgs