msoos / minisat-v1.14 Goto Github PK
View Code? Open in Web Editor NEWMiniSat v1.14
License: Other
MiniSat v1.14
License: Other
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.
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):
p cnf 9 19
2 -1
0
2 -3
0
1 3 -2
0
5 4 2
0
5 -2 -4
0
4 -2 -5
0
2 -4 -5
0
8 -7 -6
0
7 -8
0
6 -8
0
9 5
0
-5 -9
0
4 8
0
-8 -4
0
3 6
0
-6 -3
0
1 7
0
-7 -1
0
9
0
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.