Opened 9 years ago

Closed 5 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: Martin Albrecht, Marc Mezzarobba Merged in:
Authors: Reviewers:
Report Upstream: N/A Work issues:
Branch: u/malb/ticket-15674-cryptominisat (Commits, GitHub, GitLab) Commit: e9b47aac79b7f20af9bfdae89aa99175fd7773d1
Dependencies: #19298 Stopgaps:

Status badges

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:

Change History (27)

comment:1 Changed 9 years ago by Nathann Cohen

Cc: Martin Albrecht added

comment:2 Changed 9 years ago by Martin Albrecht

Branch: u/malb/ticket-15674-cryptominisat
Commit: a19676ff338523cb17e9f46f3797e48baf562683

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


New commits:

a19676fadding cryptominisat 2.9.6 to build/pkgs

comment:3 Changed 9 years ago by 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

comment:4 Changed 9 years ago by 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

comment:5 in reply to:  3 ; Changed 9 years ago by 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?

comment:6 in reply to:  5 Changed 9 years ago by 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

comment:7 Changed 9 years ago by 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.

comment:8 Changed 9 years ago by Martin Albrecht

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

comment:9 Changed 9 years ago by Martin Albrecht

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

comment:10 Changed 9 years ago by For batch modifications

Milestone: sage-6.1sage-6.2

comment:11 Changed 9 years ago by git

Commit: a19676ff338523cb17e9f46f3797e48baf562683e9b47aac79b7f20af9bfdae89aa99175fd7773d1

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

d19d095adding cryptominisat 2.9.6 to build/pkgs
85f4b71removing changelog from SPKG.txt, using upstream tarball directly
791530fcmsat-VERSION -> cryptominisat-VERSION
e9b47aaMerge branch 'u/malb/ticket-15674-cryptominisat' of trac.sagemath.org:sage into cryptominisat

comment:12 Changed 9 years ago by 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/

comment:13 Changed 9 years ago by 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.

comment:14 Changed 9 years ago by For batch modifications

Milestone: sage-6.2sage-6.3

comment:15 Changed 8 years ago by For batch modifications

Milestone: sage-6.3sage-6.4

comment:16 Changed 8 years ago by Marc Mezzarobba

Cc: Marc Mezzarobba added

comment:17 Changed 7 years ago by Jeroen Demeyer

Dependencies: #19298

comment:18 Changed 7 years ago by 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.

comment:19 Changed 7 years ago by Jeroen Demeyer

Milestone: sage-6.4sage-6.9
Summary: Update cryptominisat (optional package) from CryptoMiniSat version 2.9.6 to version 3+Update cryptominisat

comment:20 Changed 7 years ago by 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 ? :)

comment:21 Changed 7 years ago by 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?

comment:22 in reply to:  21 Changed 7 years ago by 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.

comment:23 Changed 7 years ago by Martin Albrecht

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 7 years ago by Nathann Cohen

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

comment:25 Changed 7 years ago by 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 :)

comment:26 Changed 5 years ago by François Bissey

Milestone: sage-6.9sage-duplicate/invalid/wontfix
Status: newneeds_review

Superseded by #22817 (cryptominisat 5).

comment:27 Changed 5 years ago by Erik Bray

Resolution: wontfix
Status: needs_reviewclosed

Goes without saying.

Note: See TracTickets for help on using tickets.