MiniSAT

MiniSat FAQ

Benchmarks

SATLIB

pigeon-hole.tar.gz

Configurable SAT Solver Challenge 2014

Discussion Forum

notes 15 Jun 2013 Vegard need libgmp

Examples of minisat

http://www.dwheeler.com/essays/minisat-user-guide.html

example_5_3.txt

c Here is a comment.
 p cnf 5 3
 1 -5 4 0
 -1 5 3 4 0
 -3 -4 0
bin/minisat example_5_3.txt example_5_3.out
WARNING: for repeatability, setting FPU to use double precision
============================[ Problem Statistics ]=============================
|                                                                             |
|  Number of variables:             5                                         |
|  Number of clauses:               3                                         |
|  Parse time:                   0.00 s                                       |
|  Eliminated clauses:           0.00 Mb                                      |
|  Simplification time:          0.00 s                                       |
|                                                                             |
============================[ Search Statistics ]==============================
| Conflicts |          ORIGINAL         |          LEARNT          | Progress |
|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |
===============================================================================
===============================================================================
restarts              : 1
conflicts             : 0              (0 /sec)
decisions             : 1              (0.00 % random) (1495 /sec)
propagations          : 0              (0 /sec)
conflict literals     : 0              (-nan % deleted)
Memory used           : 20.79 MB
CPU time              : 0.000669 s

SATISFIABLE

example_5_3.out

SAT
-1 -2 -3 -4 -5 0

Problems Running minisat

bin/minisat bin/minisat: error while loading shared libraries: libminisat.so.2: cannot open shared object file: No such file or directory

Work around

setenv LD_LIBRARY_PATH "$LD_LIBRARY_PATH":lib

github

Jargon

unit clause

A unit clause is a clause containing exactly one literal [G. Sennton, 2014].

UIP

UIP is a unique implication point [Minimizing Learned Clauses, Niklas Soerensson and Armin Biere, 2009].


W.B.Langdon Back 26 July 2015 (last update 11 August)