cryptominisat
cryptominisat copied to clipboard
msoos
An advanced SAT solver
When a program uses `pycryptosat`, it'll fail to respond to the `Ctrl+C` shortcut because the native component of `pycryptosat`, `SATSolver` from CryptoMiniSat, doesn't invoke Python's signal handler. Demonstration: ```python3 from...
Hi, DRAT proof checkers ignore deletions of (pseudo) unit clauses for reasons stated [here](https://github.com/marijnheule/drat-trim#clause-deletion-details). Unsatisfiability proofs by CryptoMiniSat can contain deletions of unit clauses and as a result many of...
Hi @msoos, I am a contributor to the [Conda](https://github.com/conda/conda/), the package manager, and I'm currently [working on speeding up the dependency resolution](https://github.com/conda/conda/pull/7676) therein. One very important aspect of this is...
Hello, I just noticed, that `msolve_selected` in the Python API can return the same solution multiple times. When I checked the source-code I found the reason here: https://github.com/msoos/cryptominisat/blob/0bc084f15cb3ef94618817372d6cba29a86868c4/python/src/pycryptosat.cpp#L937-L977 As you...
[bugCMS.zip](https://github.com/msoos/cryptominisat/files/10827911/bugCMS.zip) Hi, attached instance which causes error. If running with first row c ind (which is VAR variables for me) it fails. I've tried version 580x64 (static release from git)...
Hi, I think https://github.com/msoos/cryptominisat/commit/d477b0db9cf066f3c2852e6fe5b22f7d4946b8b4 removed support for having multiple `c ind` lines. I'm not sure if this is intended but, in particular, it seems like only the very last `c...
``` /tmp/SBo/cryptominisat-5.11.21/src/searcher.cpp: In member function ‘CMSat::Clause* CMSat::Searcher::handle_last_confl(uint32_t, uint32_t, uint32_t, uint32_t, bool, uint32_t, int32_t&)’: /tmp/SBo/cryptominisat-5.11.21/src/searcher.cpp:1673:27: error: ‘std::mt19937_64’ {aka ‘class std::mersenne_twister_engine’} has no member named ‘randDblExc’ 1673 | double myrnd = mtrand.randDblExc();...
Hello, I have implemented support for IDRUP in Cryptominisat (the paper is available at https://cca.informatik.uni-freiburg.de/papers/FazekasPollittFleuryBiere-MBMV24.pdf). It is a proof format for incremental SAT solving. A checker and a fuzzer are...
See: https://github.com/cython/cython/issues/5134 and https://docs.python.org/3.13/whatsnew/3.13.html#unittest
