summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat2/README
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-10-21 19:45:52 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-10-21 19:45:52 -0700
commit228dbcc51e8a00cc8e7c002f66b4411aada3a3fa (patch)
tree08926571fa021a4b7e5736f32591cc3a792acfd6 /src/sat/bsat2/README
parenta9317eac758b150ef839aa673e9a04bacb875d8b (diff)
downloadabc-228dbcc51e8a00cc8e7c002f66b4411aada3a3fa.tar.gz
abc-228dbcc51e8a00cc8e7c002f66b4411aada3a3fa.tar.bz2
abc-228dbcc51e8a00cc8e7c002f66b4411aada3a3fa.zip
Adding code of MiniSAT 2.2.
Diffstat (limited to 'src/sat/bsat2/README')
-rw-r--r--src/sat/bsat2/README24
1 files changed, 24 insertions, 0 deletions
diff --git a/src/sat/bsat2/README b/src/sat/bsat2/README
new file mode 100644
index 00000000..e5e5617d
--- /dev/null
+++ b/src/sat/bsat2/README
@@ -0,0 +1,24 @@
+================================================================================
+DIRECTORY OVERVIEW:
+
+mtl/ Mini Template Library
+utils/ Generic helper code (I/O, Parsing, CPU-time, etc)
+core/ A core version of the solver
+simp/ An extended solver with simplification capabilities
+README
+LICENSE
+
+================================================================================
+BUILDING: (release version: without assertions, statically linked, etc)
+
+export MROOT=<minisat-dir> (or setenv in cshell)
+cd { core | simp }
+gmake rs
+cp minisat_static <install-dir>/minisat
+
+================================================================================
+EXAMPLES:
+
+Run minisat with same heuristics as version 2.0:
+
+> minisat <cnf-file> -no-luby -rinc=1.5 -phase-saving=0 -rnd-freq=0.02