Opened 8 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, 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 8 years ago by ncohen

  • Cc malb added

comment:2 Changed 8 years ago by malb

  • Branch set to u/malb/ticket-15674-cryptominisat
  • Commit set to 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 follow-up: Changed 8 years ago by malb

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 8 years ago by ncohen

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: Changed 8 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 8 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 8 years ago by msoos

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 8 years ago by malb

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

comment:9 Changed 8 years ago by malb

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

comment:10 Changed 8 years ago by vbraun_spam

  • Milestone changed from sage-6.1 to sage-6.2

comment:11 Changed 8 years ago by git

  • Commit changed from a19676ff338523cb17e9f46f3797e48baf562683 to e9b47aac79b7f20af9bfdae89aa99175fd7773d1

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 8 years ago by malb

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 8 years ago by malb

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 vbraun_spam

  • Milestone changed from sage-6.2 to sage-6.3

comment:15 Changed 7 years ago by vbraun_spam

  • Milestone changed from sage-6.3 to sage-6.4

comment:16 Changed 7 years ago by mmezzarobba

  • Cc mmezzarobba added

comment:17 Changed 6 years ago by jdemeyer

  • Dependencies set to #19298

comment:18 Changed 6 years ago by msoos

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 6 years ago by jdemeyer

  • 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 6 years ago by malb

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

comment:22 in reply to: ↑ 21 Changed 6 years ago by jdemeyer

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 6 years ago by malb

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 ncohen

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 msoos

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 fbissey

  • 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 embray

  • Resolution set to wontfix
  • Status changed from needs_review to closed

Goes without saying.

Note: See TracTickets for help on using tickets.