The minisat-v1.14 from msoos

minisat-v1.14's Introduction

MiniSat v1.14 / MiniSat-p v1.14
========================================

This version is a cleaned up version of the MiniSat solver entering
the SAT 2005 competition.  Some of the most low-level optimization has
been removed for the sake of clarity, resulting in a 5-10% performance
degradation. The guard on "too-many-calls" in 'simplifyDB()' has also
been improved. If uttermost performance is needed, use the competition
version, also available at the MiniSat page
(www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/).

Several things has changed inside MiniSat since the first version,
documented in the paper "An Extensible SAT Solver". The most important
is the lack of support for non-clausal constraints in this
version. Please use MiniSat v1.12b if you need this. Other changes are
special treatment of binary clauses for efficiency (messes up the code
a bit, but gives quite a speedup), improved variable order (still
VSIDS based, but works MUCH better than in previous MiniSat
versions!), conflict clause minimization (by Niklas Sörensson), and a
better Main module (for those of you who use MiniSat as a stand-alone
solver).

The MiniSat-p version also supports proof logging, sacrificing the
binary clauses trick for clarity (some 10-20% slower). For
scalability, we decided to keep the proof only on disk. This frees up
memory for the working set of conflict clauses, and allows for
bigger-than-memory proofs to be produced (which can happen, even if
you garbage collect the proof).

For information about upcomming changes, please review the TODO file.

minisat-v1.14's People

Contributors

Stargazers

Watchers

minisat-v1.14's Issues

Wrong SAT results on Linux/ARM64

Hi,

I don't know if you have the required expertise to fix this issue, but anyway this is an issue. Test CNF (should be UNSAT but now SAT on Linux/ARM64):

Test OS: Ubuntu 20.04 LTS ARM64 (GCC 9.3.0). Below are the wrong result outputs:

==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |      17       40 |       5       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 3              (893 /sec)
propagations          : 9              (2680 /sec)
conflict literals     : 0              ( nan % deleted)
Memory used           : 4.66 MB
CPU time              : 0.003358 s

SATISFIABLE

The correct one (from macOS/ARM64):

==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |      15       34 |       5       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 3              (448 /sec)
decisions             : 2              (299 /sec)
propagations          : 16             (2389 /sec)
conflict literals     : 3              (0.00 % deleted)
CPU time              : 0.006696 s

UNSATISFIABLE

Note: The result is correct on macOS/ARM64, and also correct on Linux/x86_64, thus only is found wrongly on Linux/ARM64, a specific combination. Upgrading to MiniSAT 2 (which has no such issue) is NOT an option, because proof logging is needed.

To get a full ARM64/Linux development environment running on QEMU, I have some scripts [1] that may help.

Regards,

Chun Tian

[1] https://github.com/binghe/qemu-macos-x86-arm64

Recommend Projects