enable proof printing through CMake option

.gitignore

@@ -111,3 +111,6 @@ _deps
 .ionide
 
 # End of https://www.toptal.com/developers/gitignore/api/c,c++,cmake,visualstudiocode
+
+build/*
+.cache/*

CMakeLists.txt

@@ -0,0 +1,80 @@
+cmake_minimum_required(VERSION 3.21 FATAL_ERROR)
+
+project(minisat)
+set(CMAKE_CXX_STANDARD 17)
+
+#--------------------------------------------------------------------------------------------------
+# Configurable options:
+
+option(STATIC_BINARIES "Link binaries statically." ON)
+option(USE_SORELEASE   "Use SORELEASE in shared library filename." ON)
+option(PRINT_PROOFS    "Enable the -c option in the minisat binary to print resolution proofs." ON)
+
+#--------------------------------------------------------------------------------------------------
+# Library version:
+
+set(MINISAT_SOMAJOR   1)
+set(MINISAT_SOMINOR   14)
+set(MINISAT_SORELEASE "P")
+
+# Compute VERSION and SOVERSION:
+if (USE_SORELEASE)
+  set(MINISAT_VERSION ${MINISAT_SOMAJOR}.${MINISAT_SOMINOR}.${MINISAT_SORELEASE})
+else()
+  set(MINISAT_VERSION ${MINISAT_SOMAJOR}.${MINISAT_SOMINOR})
+endif()
+set(MINISAT_SOVERSION ${MINISAT_SOMAJOR})
+
+#--------------------------------------------------------------------------------------------------
+# Dependencies:
+
+find_package(ZLIB)
+include_directories(${ZLIB_INCLUDE_DIR})
+include_directories(${minisat_SOURCE_DIR})
+
+#--------------------------------------------------------------------------------------------------
+# Compile flags:
+
+add_definitions(-D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS)
+
+#--------------------------------------------------------------------------------------------------
+# Macro switches:
+
+if(PRINT_PROOFS)
+    add_compile_definitions(ENABLE_PROOF)
+endif()
+
+#--------------------------------------------------------------------------------------------------
+# Build Targets:
+
+add_subdirectory(src)
+
+target_link_libraries(minisat-lib-shared ${ZLIB_LIBRARY})
+target_link_libraries(minisat-lib-static ${ZLIB_LIBRARY})
+
+add_executable(minisat_core src/Main.C)
+
+if(STATIC_BINARIES)
+  target_link_libraries(minisat_core minisat-lib-static)
+else()
+  target_link_libraries(minisat_core minisat-lib-shared)
+endif()
+
+set_target_properties(minisat-lib-static PROPERTIES OUTPUT_NAME "minisat")
+set_target_properties(minisat-lib-shared
+  PROPERTIES
+    OUTPUT_NAME "minisat" 
+    VERSION ${MINISAT_VERSION}
+    SOVERSION ${MINISAT_SOVERSION})
+
+#--------------------------------------------------------------------------------------------------
+# Installation targets:
+
+install(TARGETS minisat-lib-static minisat-lib-shared minisat_core 
+        RUNTIME DESTINATION bin
+        LIBRARY DESTINATION lib
+        ARCHIVE DESTINATION lib)
+
+install(DIRECTORY src
+        DESTINATION include/minisat
+        FILES_MATCHING PATTERN "*.h")

LICENSE

@@ -0,0 +1,20 @@
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a
+copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

README

@@ -0,0 +1,30 @@
+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.

README.md

@@ -1,4 +0,0 @@
-# Minisat
-
-This Git repository holds all major release versions of [Minisat](http://minisat.se/Main.html) plus occasional patches for your convenience.
-To get a specific version, see the branches of this repository.

TODO

@@ -0,0 +1,73 @@
+==================================================
+The 'ok' flag...
+==================================================
+
+The vector 'clauses[]' store all clauses of size >= 2, the vector
+'assigns[]' store clauses of size 1, the boolean 'ok' stores clauses
+of size 0 -- and there is only one such clause, the empty clause, so
+in other words, 'ok' stores "is there an empty clause or not".
+
+As Niklas Sörensson pointed out, the 'ok' flag is a bit error prone
+and probably best viewed as an abstraction provided by the public
+member functions for user convenience (you don't have to watch the
+return value after each 'addClause()'). This is currently not
+implemented, and the 'ok' flag is still present in the internal
+methods. This will change in the future.
+
+
+==================================================
+Assumptions
+==================================================
+
+The handling of assumptions and the 'root_level' is a bit clumsy.  We
+will probably change so that the conflict driven backtracking can undo
+beyond the 'root_level', and then let the assumptions be
+remade. Currently we have to put in a hack to assure unit clauses have
+a 'level' of zero, or else the 'analyzeFinal()' method will not work
+properly. These unit clauses will also be forgotten before the next
+incremental SAT, which is also undesirable (but doesn't seem to
+degrade performance).
+
+
+==================================================
+Floating points
+==================================================
+
+The IEEE standard allows, in principle, floating points to behave
+identical on different systems. However, the FPU can be set in different
+modes, and Linux defaults to 80 bits mantissa, while most other systems,
+including Free BSD, defaults to 64 bits. The latter is preferd, as 
+the 80 bit precision in Linux is only preserved as long as the 'double'
+is kept in a register (which depends on the C-compiler -- you have 
+no control). With proper #ifdef's for differnt systems, the FPU can
+be put into the right mode.
+
+Of course it doesn't affect the efficiency of the solver, but since we
+use floats in our activity heuristic, eventually the same solver can
+behave different on different systems. The most stop-gap incarnation
+of this is a statically linked Linux binary, which when ran on
+identical hardware but under FreeBSD, can produce different behavior.
+
+
+==================================================
+Proof logging (for the '1.14p' version)
+==================================================
+
+Proof logging is still missing the implementation of the 'compress()'
+method, that will pull out the "proof" from the "trace", i.e. remove
+the derivation of clauses that did not participate in the final
+conflict (deriving the empty clause).  It's just work, and it will
+happen, but currently you can only traverse the whole trace (which is
+still very useful).
+
+
+==================================================
+Conflict clause minimization & 'trail_pos[]'
+==================================================
+
+In proof logging mode, the order of literals in 'trail[]' (the
+assignment stack) must be recorded to do the logging correctly for
+conflict clause minimization. However, this position could actually,
+with some modification, replace the 'level[]' vector all together. It
+makes a lot of sense to do this, but for the time being we record
+both. This will change in the future.

src/CMakeLists.txt

@@ -0,0 +1,12 @@
+include_directories(./)
+include_directories(../lib/minisat/minisat/core/)
+
+file(
+    GLOB MINISAT_LIB_SOURCES
+    "File.C"
+    "Proof.C"
+    "Solver.C"
+)
+
+add_library(minisat-lib-static STATIC ${MINISAT_LIB_SOURCES})
+add_library(minisat-lib-shared SHARED ${MINISAT_LIB_SOURCES})

src/File.C

@@ -0,0 +1,156 @@
+#include "File.h"
+
+
+void File::open(int file_descr, FileMode m, bool own)
+{
+    if (fd != -1) ::close(fd);
+    fd     = file_descr;
+    mode   = m;
+    own_fd = own;
+    pos    = 0;
+    buf    = xmalloc<uchar>(File_BufSize);
+    if (mode == READ) size = read(fd, buf, File_BufSize);
+    else              size = -1;
+}
+
+void File::open(cchar* name, cchar* mode_)
+{
+    if (fd != -1) ::close(fd);
+    bool    has_r = strchr(mode_, 'r') != NULL;
+    bool    has_w = strchr(mode_, 'w') != NULL;
+    bool    has_a = strchr(mode_, 'a') != NULL;
+    bool    has_p = strchr(mode_, '+') != NULL;
+    bool    has_x = strchr(mode_, 'x') != NULL;
+    assert(!(has_r && has_w));
+    assert(has_r || has_w || has_a);
+
+    int mask = 0;
+    if      (has_p) mask |= O_RDWR;
+    else if (has_r) mask |= O_RDONLY;
+    else            mask |= O_WRONLY;
+
+    if (!has_r) mask |= O_CREAT;
+    if (has_w)  mask |= O_TRUNC;
+    if (has_x)  mask |= O_EXCL;
+
+    fd = open64(name, mask, S_IRUSR|S_IWUSR|S_IRGRP|S_IWGRP|S_IROTH|S_IWOTH);
+
+    if (fd != -1){
+        mode   = has_r ? READ : WRITE;
+        own_fd = true;
+        pos    = 0;
+        if (has_a) lseek64(fd, 0, SEEK_END);
+        buf    = xmalloc<uchar>(File_BufSize);
+        if (mode == READ) size = read(fd, buf, File_BufSize);
+        else              size = -1;
+    }
+}
+
+
+void File::close(void)
+{
+    if (fd == -1) return;
+    if (mode == WRITE)
+        flush();
+    xfree(buf); buf = NULL;
+    if (own_fd)
+        ::close(fd);
+    fd = -1;
+}
+
+void File::seek(int64 file_pos, int whence)
+{
+    if (mode == WRITE){
+        flush();
+        pos = 0;
+        lseek64(fd, file_pos, whence);
+    }else{
+        if (whence == SEEK_CUR) lseek64(fd, file_pos - (size - pos), SEEK_CUR);
+        else                    lseek64(fd, file_pos, whence);
+        size = read(fd, buf, File_BufSize);
+        pos = 0;
+    }
+}
+
+int64 File::tell(void)
+{
+    if (mode == WRITE)
+        return lseek64(fd, 0, SEEK_CUR);
+    else
+        return lseek64(fd, 0, SEEK_CUR) - (size - pos);
+}
+
+
+//=================================================================================================
+// Marshaling:
+
+
+void putUInt(File& out, uint64 val)
+{
+    if (val < 0x20000000){
+        uint    v = (uint)val;
+        if (v < 0x80)
+            out.putChar(v);
+        else{
+            if (v < 0x2000)
+                out.putChar(0x80 | (v >> 8)),
+                out.putChar((uchar)v);
+            else if (v < 0x200000)
+                out.putChar(0xA0 | (v >> 16)),
+                out.putChar((uchar)(v >> 8)),
+                out.putChar((uchar)v);
+            else
+                out.putChar((v >> 24) | 0xC0),
+                out.putChar((uchar)(v >> 16)),
+                out.putChar((uchar)(v >> 8)),
+                out.putChar((uchar)v);
+        }
+    }else
+        out.putChar(0xE0),
+        out.putChar((uchar)(val >> 56)),
+        out.putChar((uchar)(val >> 48)),
+        out.putChar((uchar)(val >> 40)),
+        out.putChar((uchar)(val >> 32)),
+        out.putChar((uchar)(val >> 24)),
+        out.putChar((uchar)(val >> 16)),
+        out.putChar((uchar)(val >> 8)),
+        out.putChar((uchar)val);
+}
+
+
+uint64 getUInt(File& in)
+{
+    uint byte0, byte1, byte2, byte3, byte4, byte5, byte6, byte7;
+    byte0 = in.getChar();
+    if (byte0 == (uint)EOF)
+        throw Exception_EOF();
+    if (!(byte0 & 0x80))
+        return byte0;
+    else{
+        switch ((byte0 & 0x60) >> 5){
+        case 0:
+            byte1 = in.getChar();
+            return ((byte0 & 0x1F) << 8) | byte1;
+        case 1:
+            byte1 = in.getChar();
+            byte2 = in.getChar();
+            return ((byte0 & 0x1F) << 16) | (byte1 << 8) | byte2;
+        case 2:
+            byte1 = in.getChar();
+            byte2 = in.getChar();
+            byte3 = in.getChar();
+            return ((byte0 & 0x1F) << 24) | (byte1 << 16) | (byte2 << 8) | byte3;
+        default:
+            byte0 = in.getChar();
+            byte1 = in.getChar();
+            byte2 = in.getChar();
+            byte3 = in.getChar();
+            byte4 = in.getChar();
+            byte5 = in.getChar();
+            byte6 = in.getChar();
+            byte7 = in.getChar();
+            return ((uint64)((byte0 << 24) | (byte1 << 16) | (byte2 << 8) | byte3) << 32)
+                 |  (uint64)((byte4 << 24) | (byte5 << 16) | (byte6 << 8) | byte7);
+        }
+    }
+}

src/File.h

@@ -0,0 +1,140 @@
+#ifndef File_h
+#define File_h
+
+#ifndef Global_h
+#include "Global.h"
+#endif
+
+#include <unistd.h>
+#include <fcntl.h>
+#include <sys/stat.h>
+
+#ifndef _LARGEFILE64_SOURCE
+#define lseek64 ::lseek
+#define open64  ::open
+#endif
+
+
+//=================================================================================================
+// A buffered file abstraction with only 'putChar()' and 'getChar()'.
+
+
+#define File_BufSize 1024   // A small buffer seem to work just as fine as a big one (at least under Linux)
+
+enum FileMode { READ, WRITE };
+
+class Exception_EOF {};
+
+
+// WARNING! This code is not thoroughly tested. May contain bugs!
+
+class File {
+    int         fd;         // Underlying file descriptor.
+    FileMode    mode;       // Reading or writing.
+    uchar*      buf;        // Read or write buffer.
+    int         size;       // Size of buffer (at end of file, less than 'File_BufSize').
+    int         pos;        // Current position in buffer
+    bool        own_fd;     // Do we own the file descriptor? If so, will close file in destructor.
+
+public:
+    #define DEFAULTS fd(-1), mode(READ), buf(NULL), size(-1), pos(0), own_fd(true)
+    File(void) : DEFAULTS {}
+
+    File(int fd, FileMode mode, bool own_fd = true) : DEFAULTS  {
+        open(fd, mode, own_fd); }
+
+    File(cchar* name, cchar* mode) : DEFAULTS {
+        open(name, mode); }
+    #undef DEFAULTS
+
+   ~File(void) {
+        close(); }
+
+    void open(int fd, FileMode mode, bool own_fd = true);    // Low-level open. If 'own_fd' is FALSE, descriptor will not be closed by destructor.
+    void open(cchar* name, cchar* mode);                     // FILE* compatible interface.
+    void close(void);
+
+    bool null(void) {               // TRUE if no file is opened.
+        return fd == -1; }
+
+    int releaseDescriptor(void) {   // Don't run UNIX function 'close()' on descriptor in 'File's 'close()'.
+        if (mode == READ)
+            lseek64(fd, pos - size, SEEK_CUR);
+        own_fd = false;
+        return fd; }
+
+    FileMode getMode(void) {
+        return mode; }
+
+    void setMode(FileMode m) {
+        if (m == mode) return;
+        if (m == READ){
+            flush();
+            size = read(fd, buf, File_BufSize);
+        }else{
+            lseek64(fd, pos - size, SEEK_CUR);
+            size = -1; }
+        mode = m;
+        pos = 0; }
+
+    int getCharQ(void) {            // Quick version with minimal overhead -- don't call this in the wrong mode!
+      #ifdef PARANOID
+        assert(mode == READ);
+      #endif
+        if (pos < size) return (uchar)buf[pos++];
+        if (size < File_BufSize) return EOF;
+        size = read(fd, buf, File_BufSize);
+        pos  = 0;
+        if (size == 0) return EOF;
+        return (uchar)buf[pos++]; }
+
+    int putCharQ(int chr) {         // Quick version with minimal overhead -- don't call this in the wrong mode!
+      #ifdef PARANOID
+        assert(mode == WRITE);
+      #endif
+        if (pos == File_BufSize)
+            write(fd, buf, File_BufSize),
+            pos = 0;
+        return buf[pos++] = (uchar)chr; }
+
+    int getChar(void) {
+        if (mode == WRITE) setMode(READ);
+        return getCharQ(); }
+
+    int putChar(int chr) {
+        if (mode == READ) setMode(WRITE);
+        return putCharQ(chr); }
+
+    bool eof(void) {
+        assert(mode == READ);
+        if (pos < size) return false;
+        if (size < File_BufSize) return true;
+        size = read(fd, buf, File_BufSize);
+        pos  = 0;
+        if (size == 0) return true;
+        return false; }
+
+    void flush(void) {
+        assert(mode == WRITE);
+        write(fd, buf, pos);
+        pos = 0; }
+
+    void  seek(int64 pos, int whence = SEEK_SET);
+    int64 tell(void);
+};
+
+
+//=================================================================================================
+// Some nice helper functions:
+
+
+void                 putUInt (File& out, uint64 val);
+uint64               getUInt (File& in);
+static inline uint64 encode64(int64  val)           { return (val >= 0) ? (uint64)val << 1 : (((uint64)(~val) << 1) | 1); }
+static inline int64  decode64(uint64 val)           { return ((val & 1) == 0) ? (int64)(val >> 1) : ~(int64)(val >> 1); }
+static inline void   putInt  (File& out, int64 val) { putUInt(out, encode64(val)); }
+static inline uint64 getInt  (File& in)             { return decode64(getUInt(in)); }
+
+
+//=================================================================================================
+#endif

src/Global.h

@@ -0,0 +1,274 @@
+/****************************************************************************************[Global.h]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Global_h
+#define Global_h
+
+#include <cassert>
+#include <cstdio>
+#include <cstdlib>
+#include <cstring>
+#include <climits>
+#include <cfloat>
+#include <new>
+
+
+//=================================================================================================
+// Basic Types & Minor Things:
+
+
+#ifdef _MSC_VER
+typedef INT64              int64;
+typedef UINT64             uint64;
+typedef INT_PTR            intp;
+typedef UINT_PTR           uintp;
+#define I64_fmt "I64d"
+#else
+typedef long long          int64;
+typedef unsigned long long uint64;
+typedef __PTRDIFF_TYPE__   intp;
+typedef unsigned __PTRDIFF_TYPE__ uintp;
+#define I64_fmt "lld"
+#endif
+typedef unsigned char uchar;
+typedef const char    cchar;
+
+
+template<class T> static inline T min(T x, T y) { return (x < y) ? x : y; }
+template<class T> static inline T max(T x, T y) { return (x > y) ? x : y; }
+
+template <bool> struct STATIC_ASSERTION_FAILURE;
+template <> struct STATIC_ASSERTION_FAILURE<true>{};
+#define TEMPLATE_FAIL STATIC_ASSERTION_FAILURE<false>()
+
+
+//=================================================================================================
+// 'malloc()'-style memory allocation -- never returns NULL; aborts instead:
+
+
+template<class T> static inline T* xmalloc(size_t size) {
+    T*   tmp = (T*)malloc(size * sizeof(T));
+    assert(size == 0 || tmp != NULL);
+    return tmp; }
+
+template<class T> static inline T* xrealloc(T* ptr, size_t size) {
+    T*   tmp = (T*)realloc((void*)ptr, size * sizeof(T));
+    assert(size == 0 || tmp != NULL);
+    return tmp; }
+
+template<class T> static inline void xfree(T *ptr) {
+    if (ptr != NULL) free((void*)ptr); }
+
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double& seed) {
+    seed *= 1389796;
+    int q = (int)(seed / 2147483647);
+    seed -= (double)q * 2147483647;
+    return seed / 2147483647; }
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double& seed, int size) {
+    return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// Time and Memory:
+
+
+//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+#ifdef _MSC_VER
+
+#include <ctime>
+
+static inline double cpuTime(void) {
+    return (double)clock() / CLOCKS_PER_SEC; }
+
+static inline int64 memUsed() {
+    return 0; }
+
+//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+#else
+
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <unistd.h>
+
+static inline double cpuTime(void) {
+    struct rusage ru;
+    getrusage(RUSAGE_SELF, &ru);
+    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
+
+static inline int memReadStat(int field)
+{
+    char    name[256];
+    pid_t pid = getpid();
+    sprintf(name, "/proc/%d/statm", pid);
+    FILE*   in = fopen(name, "rb");
+    if (in == NULL) return 0;
+    int     value;
+    for (; field >= 0; field--)
+        fscanf(in, "%d", &value);
+    fclose(in);
+    return value;
+}
+
+static inline int64 memUsed() { return (int64)memReadStat(0) * (int64)getpagesize(); }
+
+//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+#endif
+
+
+
+//=================================================================================================
+// 'vec' -- automatically resizable arrays (via 'push()' method):
+
+
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T>
+class vec {
+    T*  data;
+    int sz;
+    int cap;
+
+    void     init(int size, const T& pad);
+    void     grow(int min_cap);
+
+public:
+    // Types:
+    typedef int Key;
+    typedef T   Datum;
+
+    // Constructors:
+    vec(void)                   : data(NULL) , sz(0)   , cap(0)    { }
+    vec(int size)               : data(NULL) , sz(0)   , cap(0)    { growTo(size); }
+    vec(int size, const T& pad) : data(NULL) , sz(0)   , cap(0)    { growTo(size, pad); }
+    vec(T* array, int size)     : data(array), sz(size), cap(size) { }      // (takes ownership of array -- will be deallocated with 'xfree()')
+   ~vec(void)                                                      { clear(true); }
+
+    // Ownership of underlying array:
+    T*       release  (void)           { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; }
+    operator T*       (void)           { return data; }     // (unsafe but convenient)
+    operator const T* (void) const     { return data; }
+
+    // Size operations:
+    int      size   (void) const       { return sz; }
+    void     shrink (int nelems)       { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); }
+    void     pop    (void)             { sz--, data[sz].~T(); }
+    void     growTo (int size);
+    void     growTo (int size, const T& pad);
+    void     clear  (bool dealloc = false);
+    void     capacity (int size) { grow(size); }
+
+    // Stack interface:
+    void     push  (void)              { if (sz == cap) grow(sz+1); new (&data[sz]) T()    ; sz++; }
+    void     push  (const T& elem)     { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; }
+    const T& last  (void) const        { return data[sz-1]; }
+    T&       last  (void)              { return data[sz-1]; }
+
+    // Vector interface:
+    const T& operator [] (int index) const  { return data[index]; }
+    T&       operator [] (int index)        { return data[index]; }
+
+    // Don't allow copying (error prone):
+    vec<T>&  operator = (vec<T>& other) { TEMPLATE_FAIL; }
+             vec        (vec<T>& other) { TEMPLATE_FAIL; }
+
+    // Duplicatation (preferred instead):
+    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (&copy[i]) T(data[i]); }
+    void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
+};
+
+template<class T>
+void vec<T>::grow(int min_cap) {
+    if (min_cap <= cap) return;
+    if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
+    else          do cap = (cap*3+1) >> 1; while (cap < min_cap);
+    data = xrealloc(data, cap); }
+
+template<class T>
+void vec<T>::growTo(int size, const T& pad) {
+    if (sz >= size) return;
+    grow(size);
+    for (int i = sz; i < size; i++) new (&data[i]) T(pad);
+    sz = size; }
+
+template<class T>
+void vec<T>::growTo(int size) {
+    if (sz >= size) return;
+    grow(size);
+    for (int i = sz; i < size; i++) new (&data[i]) T();
+    sz = size; }
+
+template<class T>
+void vec<T>::clear(bool dealloc) {
+    if (data != NULL){
+        for (int i = 0; i < sz; i++) data[i].~T();
+        sz = 0;
+        if (dealloc) xfree(data), data = NULL, cap = 0; } }
+
+
+//=================================================================================================
+// Lifted booleans:
+
+
+class lbool {
+    int     value;
+    explicit lbool(int v) : value(v) { }
+
+public:
+    lbool()       : value(0) { }
+    lbool(bool x) : value((int)x*2-1) { }
+    int toInt(void) const { return value; }
+
+    bool  operator == (const lbool& other) const { return value == other.value; }
+    bool  operator != (const lbool& other) const { return value != other.value; }
+    lbool operator ~  (void)               const { return lbool(-value); }
+
+    friend int   toInt  (lbool l);
+    friend lbool toLbool(int   v);
+};
+inline int   toInt  (lbool l) { return l.toInt(); }
+inline lbool toLbool(int   v) { return lbool(v);  }
+
+const lbool l_True  = toLbool( 1);
+const lbool l_False = toLbool(-1);
+const lbool l_Undef = toLbool( 0);
+
+
+//=================================================================================================
+// Relation operators -- extend definitions from '==' and '<'
+
+
+#ifndef __SGI_STL_INTERNAL_RELOPS   // (be aware of SGI's STL implementation...)
+#define __SGI_STL_INTERNAL_RELOPS
+template <class T> static inline bool operator != (const T& x, const T& y) { return !(x == y); }
+template <class T> static inline bool operator >  (const T& x, const T& y) { return y < x;     }
+template <class T> static inline bool operator <= (const T& x, const T& y) { return !(y < x);  }
+template <class T> static inline bool operator >= (const T& x, const T& y) { return !(x < y);  }
+#endif
+
+
+//=================================================================================================
+#endif

src/Heap.h

@@ -0,0 +1,100 @@
+/******************************************************************************************[Heap.h]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Heap_h
+#define Heap_h
+
+
+//=================================================================================================
+
+
+static inline int left  (int i) { return i+i; }
+static inline int right (int i) { return i+i + 1; }
+static inline int parent(int i) { return i >> 1; }
+
+template<class C>
+class Heap {
+  public:
+    C        comp;
+    vec<int> heap;     // heap of ints
+    vec<int> indices;  // int -> index in heap
+
+    inline void percolateUp(int i)
+    {
+        int x = heap[i];
+        while (parent(i) != 0 && comp(x,heap[parent(i)])){
+            heap[i]          = heap[parent(i)];
+            indices[heap[i]] = i;
+            i                = parent(i);
+        }
+        heap   [i] = x;
+        indices[x] = i;
+    }
+
+    inline void percolateDown(int i)
+    {
+        int x = heap[i];
+        while (left(i) < heap.size()){
+            int child = right(i) < heap.size() && comp(heap[right(i)],heap[left(i)]) ? right(i) : left(i);
+            if (!comp(heap[child],x)) break;
+            heap[i]          = heap[child];
+            indices[heap[i]] = i;
+            i                = child;
+        }
+        heap   [i] = x;
+        indices[x] = i;
+    }
+
+    bool ok(int n) { return n >= 0 && n < (int)indices.size(); }
+
+  public:
+    Heap(C c) : comp(c) { heap.push(-1); }
+
+    void setBounds (int size) { assert(size >= 0); indices.growTo(size,0); }
+    bool inHeap    (int n)    { assert(ok(n)); return indices[n] != 0; }
+    void increase  (int n)    { assert(ok(n)); assert(inHeap(n)); percolateUp(indices[n]); }
+    bool empty     ()         { return heap.size() == 1; }
+
+    void insert(int n) {
+        assert(ok(n));
+        indices[n] = heap.size();
+        heap.push(n);
+        percolateUp(indices[n]); }
+
+    int  getmin() {
+        int r            = heap[1];
+        heap[1]          = heap.last();
+        indices[heap[1]] = 1;
+        indices[r]       = 0;
+        heap.pop();
+        if (heap.size() > 1)
+            percolateDown(1);
+        return r; }
+
+    bool heapProperty() {
+        return heapProperty(1); }
+
+    bool heapProperty(int i) {
+        return (size_t)i >= heap.size()
+            || ((parent(i) == 0 || !comp(heap[i],heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
+};
+
+
+//=================================================================================================
+#endif

src/Main.C

@@ -0,0 +1,383 @@
+/******************************************************************************************[Main.C]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#include "Solver.h"
+#include <ctime>
+#include <iomanip>
+#include <iostream>
+#include <ostream>
+#include <unistd.h>
+#include <signal.h>
+#include <zlib.h>
+
+
+//=================================================================================================
+// BCNF Parser:
+
+
+#define CHUNK_LIMIT 1048576
+
+static void parse_BCNF(cchar* filename, Solver& S)
+{
+    FILE*   in = fopen(filename, "rb");
+    if (in == NULL) fprintf(stderr, "ERROR! Could not open file: %s\n", filename), exit(1);
+
+    char    header[16];
+    fread(header, 1, 16, in);
+    if (strncmp(header, "BCNF", 4) != 0) fprintf(stderr, "ERROR! Not a BCNF file: %s\n", filename), exit(1);
+    if (*(int*)(header+4) != 0x01020304) fprintf(stderr, "ERROR! BCNF file in unsupported byte-order: %s\n", filename), exit(1);
+
+    int      n_vars    = *(int*)(header+ 8);
+    //int    n_clauses = *(int*)(header+12);
+    int*     buf       = xmalloc<int>(CHUNK_LIMIT);
+    int      buf_sz;
+    vec<Lit> c;
+
+    for (int i = 0; i < n_vars; i++) S.newVar();
+
+    for(;;){
+        int n = fread(&buf_sz, 4, 1, in);
+        if (n != 1) break;
+        assert(buf_sz <= CHUNK_LIMIT);
+        fread(buf, 4, buf_sz, in);
+
+        int* p = buf;
+        while (*p != -1){
+            int size = *p++;
+            c.clear();
+            c.growTo(size);
+            for (int i = 0; i < size; i++)
+                c[i] = toLit(p[i]);
+            p += size;
+
+            S.addClause(c);     // Add clause.
+            if (!S.okay()){
+                xfree(buf); fclose(in);
+                return; }
+        }
+    }
+
+    xfree(buf);
+    fclose(in);
+}
+
+
+//=================================================================================================
+// DIMACS Parser:
+
+
+class StreamBuffer {
+    gzFile  in;
+    char    buf[CHUNK_LIMIT];
+    int     pos;
+    int     size;
+
+    void assureLookahead() {
+        if (pos >= size) {
+            pos  = 0;
+            size = gzread(in, buf, sizeof(buf)); } }
+
+public:
+    StreamBuffer(gzFile i) : in(i), pos(0), size(0) {
+        assureLookahead(); }
+
+    int  operator *  () { return (pos >= size) ? EOF : buf[pos]; }
+    void operator ++ () { pos++; assureLookahead(); }
+};
+
+//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+
+template<class B>
+static void skipWhitespace(B& in) {
+    while ((*in >= 9 && *in <= 13) || *in == 32)
+        ++in; }
+
+template<class B>
+static void skipLine(B& in) {
+    for (;;){
+        if (*in == EOF) return;
+        if (*in == '\n') { ++in; return; }
+        ++in; } }
+
+template<class B>
+static int parseInt(B& in) {
+    int     val = 0;
+    bool    neg = false;
+    skipWhitespace(in);
+    if      (*in == '-') neg = true, ++in;
+    else if (*in == '+') ++in;
+    if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
+    while (*in >= '0' && *in <= '9')
+        val = val*10 + (*in - '0'),
+        ++in;
+    return neg ? -val : val; }
+
+template<class B>
+static void readClause(B& in, Solver& S, vec<Lit>& lits) {
+    int     parsed_lit, var;
+    lits.clear();
+    for (;;){
+        parsed_lit = parseInt(in);
+        if (parsed_lit == 0) break;
+        var = abs(parsed_lit)-1;
+        while (var >= S.nVars()) S.newVar();
+        lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) );
+    }
+}
+
+template<class B>
+static void parse_DIMACS_main(B& in, Solver& S) {
+    vec<Lit> lits;
+    for (;;){
+        skipWhitespace(in);
+        if (*in == EOF)
+            break;
+        else if (*in == 'c' || *in == 'p')
+            skipLine(in);
+        else
+            readClause(in, S, lits),
+            S.addClause(lits);
+    }
+}
+
+// Inserts problem into solver.
+//
+static void parse_DIMACS(gzFile input_stream, Solver& S) {
+    StreamBuffer in(input_stream);
+    parse_DIMACS_main(in, S); }
+
+
+//=================================================================================================
+
+
+void printStats(SolverStats& stats)
+{
+    double  cpu_time = cpuTime();
+    int64   mem_used = memUsed();
+    using namespace std;
+    cout << setprecision(0);
+    cout << "restarts              : " << stats.starts << endl << flush;
+    cout << "conflicts             : " << stats.conflicts << "   (" << stats.conflicts / cpu_time << " /sec)" << endl << flush;
+    cout << "decisions             : " << stats.decisions << "   (" << stats.decisions / cpu_time << " /sec)" << endl << flush;
+    cout << "propagations          : " << stats.propagations << "   (" << stats.propagations / cpu_time << " /sec)" << endl << flush;
+    cout << std::setprecision(2);
+    cout << "conflict literals     : " << stats.tot_literals << "   (" << setw(4) << (stats.max_literals - stats.tot_literals)*100 / (double)stats.max_literals << " %% deleted)" << endl << flush;
+    if (mem_used != 0) std::cout << "Memory used           : " << setprecision(2) << mem_used / 1048576.0 << " MB" << endl << flush;
+    cout << "CPU time              : " << cpu_time << " s" << endl << flush;
+}
+
+Solver* solver;
+static void SIGINT_handler(int signum) {
+    reportf("\n"); reportf("*** INTERRUPTED ***\n");
+    printStats(solver->stats);
+    reportf("\n"); reportf("*** INTERRUPTED ***\n");
+    exit(1); }
+
+
+//=================================================================================================
+// Simplistic proof-checker -- just to illustrate the use of 'ProofTraverser':
+
+
+#include "Sort.h"
+
+
+static void resolve(vec<Lit>& main, vec<Lit>& other, Var x)
+{
+    Lit     p;
+    bool    ok1 = false, ok2 = false;
+    for (int i = 0; i < main.size(); i++){
+        if (var(main[i]) == x){
+            ok1 = true, p = main[i];
+            main[i] = main.last();
+            main.pop();
+            break;
+        }
+    }
+
+    for (int i = 0; i < other.size(); i++){
+        if (var(other[i]) != x)
+            main.push(other[i]);
+        else{
+            if (p != ~other[i])
+                printf("PROOF ERROR! Resolved on variable with SAME polarity in both clauses: %d\n", x+1);
+            ok2 = true;
+        }
+    }
+
+    if (!ok1 || !ok2)
+        printf("PROOF ERROR! Resolved on missing variable: %d\n", x+1);
+
+    sortUnique(main);
+}
+
+
+struct Checker : public ProofTraverser {
+    vec<vec<Lit> >  clauses;
+
+    void root   (const vec<Lit>& c) {
+#ifdef ENABLE_PROOF
+        printf("%d: ROOT", clauses.size()); for (int i = 0; i < c.size(); i++) printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n");
+#endif
+        clauses.push();
+        c.copyTo(clauses.last()); }
+
+    void chain  (const vec<ClauseId>& cs, const vec<Var>& xs) {
+#ifdef ENABLE_PROOF
+        printf("%d: CHAIN %d", clauses.size(), cs[0]); for (int i = 0; i < xs.size(); i++) printf(" [%d] %d", xs[i]+1, cs[i+1]);
+#endif
+        clauses.push();
+        vec<Lit>& c = clauses.last();
+        clauses[cs[0]].copyTo(c);
+        for (int i = 0; i < xs.size(); i++)
+            resolve(c, clauses[cs[i+1]], xs[i]);
+#ifdef ENABLE_PROOF
+        printf(" =>"); for (int i = 0; i < c.size(); i++) printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1); printf("\n");
+#endif
+        }
+
+    void deleted(ClauseId c) {
+        clauses[c].clear(); }
+};
+
+
+void checkProof(Proof* proof, ClauseId goal = ClauseId_NULL)
+{
+    Checker trav;
+    proof->traverse(trav, goal);
+
+    vec<Lit>& c = trav.clauses.last();
+    printf("Final clause:");
+    if (c.size() == 0)
+        printf(" <empty>\n");
+    else{
+        for (int i = 0; i < c.size(); i++)
+            printf(" %s%d", sign(c[i])?"-":"", var(c[i])+1);
+        printf("\n");
+    }
+}
+
+
+//=================================================================================================
+// Main:
+
+
+static const char* doc =
+    "USAGE: minisat <input-file> [options]\n"
+    "  -r <result file>   Write result (the word \"SAT\" plus model, or just \"UNSAT\") to file.\n"
+    "  -p <proof trace>   Write the proof trace to this file.\n"
+    "  -c                 Check the proof trace by simple (read \"slow\") proof checker.\n"
+;
+
+int main(int argc, char** argv)
+{
+    char*       input  = NULL;
+    char*       result = NULL;
+    char*       proof  = NULL;
+    bool        check  = false;
+
+    // Parse options:
+    //
+    for (int i = 1; i < argc; i++){
+        if (argv[i][0] != '-'){
+            if (input != NULL)
+                fprintf(stderr, "ERROR! Only one input file may be specified.\n"), exit(1);
+            input = argv[i];
+        }else{
+            switch (argv[i][1]){
+            case 'r':
+                i++; if (i >= argc) fprintf(stderr, "ERROR! Missing filename after '-r' option.\n");
+                result = argv[i];
+                break;
+            case 'p':
+                i++; if (i >= argc) fprintf(stderr, "ERROR! Missing filename after '-p' option.\n");
+                proof = argv[i];
+                break;
+            case 'c':
+                check = true;
+                break;
+            case 'h':
+                reportf("%s", doc);
+                exit(0);
+            default:
+                fprintf(stderr, "ERROR! Invalid option: %s\n", argv[i]), exit(1);
+            }
+        }
+    }
+
+    // Parse input and perform SAT:
+    //
+    Solver      S;
+    if (proof != NULL || check)
+        S.proof = new Proof();
+
+    if (input != NULL && strlen(input) >= 5 && strcmp(&input[strlen(input)-5], ".bcnf") == 0)
+        parse_BCNF(input, S);
+    else{
+        if (input == NULL)
+            reportf("Reading from standard input... Use '-h' for help.\n");
+
+        gzFile in = (input == NULL) ? gzdopen(0, "rb") : gzopen(input, "rb");
+        if (in == NULL)
+            fprintf(stderr, "ERROR! Could not open file: %s\n", (input == NULL) ? "<stdin>" : input), exit(1);
+        parse_DIMACS(in, S);
+        gzclose(in);
+    }
+    FILE*   res = (result != NULL) ? fopen(result, "wb") : NULL;
+
+    if (!S.okay()){
+        if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+        if (S.proof != NULL && proof != NULL) S.proof->save(proof);
+        if (S.proof != NULL && check) printf("Checking proof...\n"), checkProof(S.proof);
+        reportf("Trivial problem\n");
+        reportf("UNSATISFIABLE\n");
+        exit(20);
+    }
+
+    S.verbosity = 1;
+    solver = &S;
+    signal(SIGINT,SIGINT_handler);
+    signal(SIGHUP,SIGINT_handler);
+
+    S.solve();
+    printStats(S.stats);
+    reportf("\n");
+    reportf(S.okay() ? "SATISFIABLE\n" : "UNSATISFIABLE\n");
+
+    if (res != NULL){
+        if (S.okay()){
+            fprintf(res, "SAT\n");
+            for (int i = 0; i < S.nVars(); i++)
+                if (S.model[i] != l_Undef)
+                    fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
+            fprintf(res, " 0\n");
+        }else
+            fprintf(res, "UNSAT\n");
+        fclose(res);
+    }
+
+    if (S.proof != NULL && !S.okay()){
+        if (proof != NULL)
+            S.proof->save(proof);
+        if (check)
+            printf("Checking proof...\n"),
+            checkProof(S.proof);
+    }
+
+    exit(S.okay() ? 10 : 20);     // (faster than "return", which will invoke the destructor for 'Solver')
+}

src/Makefile

@@ -0,0 +1,88 @@
+##
+##  Makefile for Standard, Profile, Debug, Release, and Release-static versions of MiniSat
+##
+##    eg: "make rs" for a statically linked release version.
+##        "make d"  for a debug version (no optimizations).
+##        "make"    for the standard version (optimized, but with debug information and assertions active)
+
+CSRCS     = $(wildcard *.C)
+CHDRS     = $(wildcard *.h)
+COBJS     = $(addsuffix .o, $(basename $(CSRCS)))
+
+PCOBJS    = $(addsuffix p,  $(COBJS))
+DCOBJS    = $(addsuffix d,  $(COBJS))
+RCOBJS    = $(addsuffix r,  $(COBJS))
+
+EXEC      = minisat
+
+CXX       = g++
+CFLAGS    = -Wall -ffloat-store
+COPTIMIZE = -O3
+
+
+.PHONY : s p d r build clean depend
+
+s:	WAY=standard
+p:	WAY=profile
+d:	WAY=debug
+r:	WAY=release
+rs:	WAY=release static
+
+s:	CFLAGS+=$(COPTIMIZE) -ggdb -D DEBUG
+p:	CFLAGS+=$(COPTIMIZE) -pg -ggdb -D DEBUG
+d:	CFLAGS+=-O0 -ggdb -D DEBUG
+r:	CFLAGS+=$(COPTIMIZE) -D NDEBUG
+rs:	CFLAGS+=$(COPTIMIZE) -D NDEBUG
+
+s:	build $(EXEC)
+p:	build $(EXEC)_profile
+d:	build $(EXEC)_debug
+r:	build $(EXEC)_release
+rs:	build $(EXEC)_static
+
+build:
+	@echo Building $(EXEC) "("$(WAY)")"
+
+clean:
+	@rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
+	  $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) depend.mak
+
+## Build rule
+%.o %.op %.od %.or:	%.C
+	@echo Compiling: $<
+	@$(CXX) $(CFLAGS) -c -o $@ $<
+
+## Linking rules (standard/profile/debug/release)
+$(EXEC): $(COBJS)
+	@echo Linking $(EXEC)
+	@$(CXX) $(COBJS) -lz -ggdb -Wall -o $@ 
+
+$(EXEC)_profile: $(PCOBJS)
+	@echo Linking $@
+	@$(CXX) $(PCOBJS) -lz -ggdb -Wall -pg -o $@
+
+$(EXEC)_debug:	$(DCOBJS)
+	@echo Linking $@
+	@$(CXX) $(DCOBJS) -lz -ggdb -Wall -o $@
+
+$(EXEC)_release: $(RCOBJS)
+	@echo Linking $@
+	@$(CXX) $(RCOBJS) -lz -Wall -o $@
+
+$(EXEC)_static: $(RCOBJS)
+	@echo Linking $@
+	@$(CXX) --static $(RCOBJS) -lz -Wall -o $@
+
+
+## Make dependencies
+depend:	depend.mak
+depend.mak: $(CSRCS) $(CHDRS)
+	@echo Making dependencies ...
+	@$(CXX) -MM $(CSRCS) > depend.mak
+	@cp depend.mak /tmp/depend.mak.tmp
+	@sed "s/o:/op:/" /tmp/depend.mak.tmp >> depend.mak
+	@sed "s/o:/od:/" /tmp/depend.mak.tmp >> depend.mak
+	@sed "s/o:/or:/" /tmp/depend.mak.tmp >> depend.mak
+	@rm /tmp/depend.mak.tmp
+
+include depend.mak

src/Proof.C

@@ -0,0 +1,235 @@
+/*****************************************************************************************[Proof.C]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#include "Proof.h"
+#include "Sort.h"
+
+
+//=================================================================================================
+// Temporary files handling:
+
+
+class TempFiles {
+    vec<cchar*> files;      // For clean-up purposed on abnormal exit.
+
+public:
+   ~TempFiles()
+    {
+        for (int i = 0; i < files.size(); i++)
+            remove(files[i]);
+            //printf("Didn't delete:\n  %s\n", files[i]);
+    }
+
+    // Returns a read-only string with the filename of the temporary file. The pointer can be used to 
+    // remove the file (which is otherwise done automatically upon program exit).
+    //
+    char* open(File& fp)
+    {
+        char*   name;
+        for(;;){
+            name = tempnam(NULL, NULL);     // (gcc complains about this... stupid gcc...)
+            assert(name != NULL);
+            fp.open(name, "wx+");
+            if (fp.null())
+                xfree(name);
+            else{
+                files.push(name);
+                return name;
+            }
+        }
+    }
+};
+static TempFiles temp_files;       // (should be singleton)
+
+
+//=================================================================================================
+// Proof logging:
+
+
+Proof::Proof()
+{
+    fp_name    = temp_files.open(fp);
+    id_counter = 0;
+    trav       = NULL;
+}
+
+
+Proof::Proof(ProofTraverser& t)
+{
+    id_counter = 0;
+    trav       = &t;
+}
+
+
+ClauseId Proof::addRoot(vec<Lit>& cl)
+{
+    cl.copyTo(clause);
+    sortUnique(clause);
+
+    if (trav != NULL)
+        trav->root(clause);
+    if (!fp.null()){
+        putUInt(fp, index(clause[0]) << 1);
+        for (int i = 1; i < clause.size(); i++)
+            putUInt(fp, index(clause[i]) - index(clause[i-1]));
+        putUInt(fp, 0);     // (0 is safe terminator since we removed duplicates)
+    }
+
+    return id_counter++;
+}
+
+
+void Proof::beginChain(ClauseId start)
+{
+    assert(start != ClauseId_NULL);
+    chain_id .clear();
+    chain_var.clear();
+    chain_id.push(start);
+}
+
+
+void Proof::resolve(ClauseId next, Var x)
+{
+    assert(next != ClauseId_NULL);
+    chain_id .push(next);
+    chain_var.push(x);
+}
+
+
+ClauseId Proof::endChain()
+{
+    assert(chain_id.size() == chain_var.size() + 1);
+    if (chain_id.size() == 1)
+        return chain_id[0];
+    else{
+        if (trav != NULL)
+            trav->chain(chain_id, chain_var);
+        if (!fp.null()){
+            putUInt(fp, ((id_counter - chain_id[0]) << 1) | 1);
+            for (int i = 0; i < chain_var.size(); i++)
+                putUInt(fp, chain_var[i] + 1),
+                putUInt(fp, id_counter - chain_id[i+1]);
+            putUInt(fp, 0);
+        }
+
+        return id_counter++;
+    }
+}
+
+
+void Proof::deleted(ClauseId gone)
+{
+    if (trav != NULL)
+        trav->deleted(gone);
+    if (!fp.null()){
+        putUInt(fp, ((id_counter - gone) << 1) | 1);
+        putUInt(fp, 0);
+    }
+}
+
+
+//=================================================================================================
+// Read-back methods:
+
+
+void Proof::compress(Proof& dst, ClauseId goal)
+{
+    assert(!fp.null());
+    assert(false);  // Not yet!    
+}
+
+
+bool Proof::save(cchar* filename)
+{
+    assert(!fp.null());
+
+    // Switch to read mode:
+    fp.setMode(READ);
+    fp.seek(0);
+
+    // Copy file:
+    File    out(filename, "wox");
+    if (out.null())
+        return false;
+
+    while (!fp.eof())
+        out.putChar(fp.getChar());
+
+    // Restore write (proof-logging) mode:
+    fp.seek(0, SEEK_END);
+    fp.setMode(WRITE);
+    return true;
+}
+
+
+void Proof::traverse(ProofTraverser& trav, ClauseId goal)
+{
+    assert(!fp.null());
+
+    // Switch to read mode:
+    fp.setMode(READ);
+    fp.seek(0);
+
+    // Traverse proof:
+    if (goal == ClauseId_NULL)
+        goal = last();
+
+    uint64  tmp;
+    int     idx;
+    for(ClauseId id = 0; id <= goal; id++){
+        tmp = getUInt(fp);
+        if ((tmp & 1) == 0){
+            // Root clause:
+            clause.clear();
+            idx = tmp >> 1;
+            clause.push(toLit(idx));
+            for(;;){
+                tmp = getUInt(fp);
+                if (tmp == 0) break;
+                idx += tmp;
+                clause.push(toLit(idx));
+            }
+            trav.root(clause);
+
+        }else{
+            // Derivation or Deletion:
+            chain_id .clear();
+            chain_var.clear();
+            chain_id.push(id - (tmp >> 1));
+            for(;;){
+                tmp = getUInt(fp);
+                if (tmp == 0) break;
+                chain_var.push(tmp - 1);
+                tmp = getUInt(fp);
+                chain_id.push(id - tmp);
+            }
+
+            if (chain_var.size() == 0)
+                id--,   // (no new clause introduced)
+                trav.deleted(chain_id[0]);
+            else
+                trav.chain(chain_id, chain_var);
+        }
+    }
+    trav.done();
+
+    // Restore write (proof-logging) mode:
+    fp.seek(0, SEEK_END);
+    fp.setMode(WRITE);
+}

src/Proof.h

@@ -0,0 +1,71 @@
+/*****************************************************************************************[Proof.h]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Proof_h
+#define Proof_h
+
+#include "SolverTypes.h"
+#include "File.h"
+
+
+//=================================================================================================
+
+
+// A "listner" for the proof. Proof events will be passed onto (online mode) or replayed to
+// (offline mode) this class.  Each call to 'root()' or 'chain()' produces a new clause. The first
+// clause has ID 0, the next 1 and so on. These are the IDs passed to 'chain()'s 'cs' parameter.
+//
+struct ProofTraverser {
+    virtual void root   (const vec<Lit>& c) {}
+    virtual void chain  (const vec<ClauseId>& cs, const vec<Var>& xs) {}
+    virtual void deleted(ClauseId c) {}
+    virtual void done   () {}
+    virtual ~ProofTraverser() {}
+};
+
+
+class Proof {
+    File            fp;
+    cchar*          fp_name;
+    ClauseId        id_counter;
+    ProofTraverser* trav;
+
+    vec<Lit>        clause;
+    vec<ClauseId>   chain_id;
+    vec<Var>        chain_var;
+
+public:
+    Proof();                        // Offline mode -- proof stored to a file, which can be saved, compressed, and/or traversed.
+    Proof(ProofTraverser& t);       // Online mode -- proof will not be stored.
+
+    ClauseId addRoot   (vec<Lit>& clause);
+    void     beginChain(ClauseId start);
+    void     resolve   (ClauseId next, Var x);
+    ClauseId endChain  ();
+    void     deleted   (ClauseId gone);
+    ClauseId last      () { assert(id_counter != ClauseId_NULL); return id_counter - 1; }
+
+    void     compress  (Proof& dst, ClauseId goal = ClauseId_NULL);     // 'dst' should be a newly constructed, empty proof.
+    bool     save      (cchar* filename);
+    void     traverse  (ProofTraverser& trav, ClauseId goal = ClauseId_NULL) ;
+};
+
+
+//=================================================================================================
+#endif

src/Solver.C

@@ -0,0 +1,819 @@
+/****************************************************************************************[Solver.C]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#include "Solver.h"
+#include "Sort.h"
+#include <cmath>
+
+#define CC_MINIMIZATION
+
+
+//=================================================================================================
+// Helper functions:
+
+
+void removeWatch(vec<Clause*>& ws, Clause* elem)
+{
+    if (ws.size() == 0) return;     // (skip lists that are already cleared)
+    int j = 0;
+    for (; ws[j] != elem  ; j++) assert(j < ws.size());
+    for (; j < ws.size()-1; j++) ws[j] = ws[j+1];
+    ws.pop();
+}
+
+
+//=================================================================================================
+// Operations on clauses:
+
+
+/*_________________________________________________________________________________________________
+|
+|  newClause : (ps : const vec<Lit>&) (learnt : bool) (id : ClauseId)  ->  [void]
+|  
+|  Description:
+|    Allocate and add a new clause to the SAT solvers clause database. If a conflict is detected,
+|    the 'ok' flag is cleared and the solver is in an unusable state (must be disposed).
+|  
+|  Input:
+|    ps     - The new clause as a vector of literals.
+|    learnt - Is the clause a learnt clause? For learnt clauses, 'ps[0]' is assumed to be the
+|             asserting literal. An appropriate 'enqueue()' operation will be performed on this
+|             literal. One of the watches will always be on this literal, the other will be set to
+|             the literal with the highest decision level.
+|    id     - If logging proof, learnt clauses should be given an ID by caller.
+|  
+|  Effect:
+|    Activity heuristics are updated.
+|________________________________________________________________________________________________@*/
+void Solver::newClause(const vec<Lit>& ps_, bool learnt, ClauseId id)
+{
+    assert(learnt || id == ClauseId_NULL);
+    if (!ok) return;
+
+    vec<Lit>    qs;
+    if (!learnt){
+        assert(decisionLevel() == 0);
+        ps_.copyTo(qs);                     // Make a copy of the input vector.
+
+        // Remove duplicates:
+        sortUnique(qs);
+
+        // Check if clause is satisfied:
+        for (int i = 0; i < qs.size()-1; i++){
+            if (qs[i] == ~qs[i+1])
+                return; }
+        for (int i = 0; i < qs.size(); i++){
+            if (value(qs[i]) == l_True)
+                return; }
+
+        // Remove false literals:
+        int     i, j;
+        if (proof != NULL) proof->beginChain(proof->addRoot(qs));
+        for (i = j = 0; i < qs.size(); i++)
+            if (value(qs[i]) != l_False)
+                qs[j++] = qs[i];
+            else
+                if (proof != NULL) proof->resolve(unit_id[var(qs[i])], var(qs[i]));
+        qs.shrink(i - j);
+        if (proof != NULL) id = proof->endChain();
+    }
+    const vec<Lit>& ps = learnt ? ps_ : qs; // 'ps' is now the (possibly) reduced vector of literals.
+
+    if (ps.size() == 0){
+        ok = false;
+
+    }else if (ps.size() == 1){
+        // NOTE: If enqueue takes place at root level, the assignment will be lost in incremental use (it doesn't seem to hurt much though).
+        if (id != ClauseId_NULL)
+            unit_id[var(ps[0])] = id;
+        if (!enqueue(ps[0]))
+            ok = false;
+
+    }else{
+        // Allocate clause:
+        Clause* c   = Clause_new(learnt, ps, id);
+
+        if (learnt){
+            // Put the second watch on the literal with highest decision level:
+            int     max_i = 1;
+            int     max   = level[var(ps[1])];
+            for (int i = 2; i < ps.size(); i++)
+                if (level[var(ps[i])] > max)
+                    max   = level[var(ps[i])],
+                    max_i = i;
+            (*c)[1]     = ps[max_i];
+            (*c)[max_i] = ps[1];
+
+            // Bumping:
+            claBumpActivity(c); // (newly learnt clauses should be considered active)
+
+            // Enqueue asserting literal:
+            check(enqueue((*c)[0], c));
+
+            // Store clause:
+            watches[index(~(*c)[0])].push(c);
+            watches[index(~(*c)[1])].push(c);
+            learnts.push(c);
+            stats.learnts_literals += c->size();
+
+        }else{
+            // Store clause:
+            watches[index(~(*c)[0])].push(c);
+            watches[index(~(*c)[1])].push(c);
+            clauses.push(c);
+            stats.clauses_literals += c->size();
+        }
+    }
+}
+
+
+// Disposes a clauses and removes it from watcher lists. NOTE! Low-level; does NOT change the 'clauses' and 'learnts' vector.
+//
+void Solver::remove(Clause* c, bool just_dealloc)
+{
+    if (!just_dealloc){
+        removeWatch(watches[index(~(*c)[0])], c),
+        removeWatch(watches[index(~(*c)[1])], c);
+
+        if (c->learnt()) stats.learnts_literals -= c->size();
+        else             stats.clauses_literals -= c->size();
+
+        if (proof != NULL) proof->deleted(c->id());
+    }
+
+    xfree(c);
+}
+
+
+// Can assume everything has been propagated! (esp. the first two literals are != l_False, unless
+// the clause is binary and satisfied, in which case the first literal is true)
+// Returns True if clause is satisfied (will be removed), False otherwise.
+//
+bool Solver::simplify(Clause* c) const
+{
+    assert(decisionLevel() == 0);
+    for (int i = 0; i < c->size(); i++){
+        if (value((*c)[i]) == l_True)
+            return true;
+    }
+    return false;
+}
+
+
+//=================================================================================================
+// Minor methods:
+
+
+// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
+// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
+//
+Var Solver::newVar() {
+    int     index;
+    index = nVars();
+    watches     .push();          // (list for positive literal)
+    watches     .push();          // (list for negative literal)
+    reason      .push(NULL);
+    assigns     .push(toInt(l_Undef));
+    level       .push(-1);
+    trail_pos   .push(-1);
+    activity    .push(0);
+    order       .newVar();
+    analyze_seen.push(0);
+    if (proof != NULL) unit_id.push(ClauseId_NULL);
+    return index; }
+
+
+// Returns FALSE if immediate conflict.
+bool Solver::assume(Lit p) {
+    trail_lim.push(trail.size());
+    return enqueue(p); }
+
+
+// Revert to the state at given level.
+void Solver::cancelUntil(int level) {
+    if (decisionLevel() > level){
+        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+            Var     x  = var(trail[c]);
+            assigns[x] = toInt(l_Undef);
+            reason [x] = NULL;
+            order.undo(x); }
+        trail.shrink(trail.size() - trail_lim[level]);
+        trail_lim.shrink(trail_lim.size() - level);
+        qhead = trail.size(); } }
+
+
+//=================================================================================================
+// Major methods:
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
+|  
+|  Description:
+|    Analyze conflict and produce a reason clause ('out_learnt') and a backtracking level
+|    ('out_btlevel').
+|  
+|    Pre-conditions:
+|      * 'out_learnt' is assumed to be cleared.
+|      * Current decision level must be greater than root level.
+|  
+|    Post-conditions:
+|      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
+|      * If performing proof-logging, the last derived clause in the proof is the reason clause.
+|________________________________________________________________________________________________@*/
+
+class lastToFirst_lt {  // Helper class to 'analyze' -- order literals from last to first occurance in 'trail[]'.
+    const vec<int>& trail_pos;
+public:
+    lastToFirst_lt(const vec<int>& t) : trail_pos(t) {}
+    bool operator () (Lit p, Lit q) { return trail_pos[var(p)] > trail_pos[var(q)]; }
+};
+
+void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel)
+{
+    vec<char>&     seen  = analyze_seen;
+    int            pathC = 0;
+    Lit            p     = lit_Undef;
+
+    // Generate conflict clause:
+    //
+    if (proof != NULL) proof->beginChain(confl->id());
+    out_learnt.push();          // (leave room for the asserting literal)
+    out_btlevel = 0;
+    int index = trail.size()-1;
+    for(;;){
+        assert(confl != NULL);  // (otherwise should be UIP)
+
+        Clause& c = *confl;
+        if (c.learnt())
+            claBumpActivity(&c);
+
+        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
+            Lit q = c[j];
+            if (!seen[var(q)]){
+                if (level[var(q)] > 0){
+                    varBumpActivity(q);
+                    seen[var(q)] = 1;
+                    if (level[var(q)] == decisionLevel())
+                        pathC++;
+                    else{
+                        out_learnt.push(q);
+                        out_btlevel = max(out_btlevel, level[var(q)]);
+                    }
+                }else
+                    if (proof != NULL) proof->resolve(unit_id[var(q)], var(q));
+            }
+        }
+
+        // Select next clause to look at:
+        while (!seen[var(trail[index--])]);
+        p     = trail[index+1];
+        confl = reason[var(p)];
+        seen[var(p)] = 0;
+        pathC--;
+        if (pathC == 0) break;
+
+        if (proof != NULL) proof->resolve(confl->id(), var(p));
+    }
+    out_learnt[0] = ~p;
+
+    // Conflict clause minimization:
+    //
+#ifdef CC_MINIMIZATION
+    int     i, j;
+    if (expensive_ccmin){
+        // Simplify conflict clause (a lot):
+        //
+        uint    min_level = 0;
+        for (i = 1; i < out_learnt.size(); i++)
+            min_level |= 1 << (level[var(out_learnt[i])] & 31);         // (maintain an abstraction of levels involved in conflict)
+
+        analyze_toclear.clear();
+        for (i = j = 1; i < out_learnt.size(); i++)
+            if (reason[var(out_learnt[i])] == NULL || !analyze_removable(out_learnt[i], min_level))
+                out_learnt[j++] = out_learnt[i];
+    }else{
+        // Simplify conflict clause (a little):
+        //
+        analyze_toclear.clear();
+        for (i = j = 1; i < out_learnt.size(); i++){
+            Clause* r = reason[var(out_learnt[i])];
+            if (r == NULL)
+                out_learnt[j++] = out_learnt[i];
+            else{
+                Clause& c = *r;
+                for (int k = 1; k < c.size(); k++)
+                    if (!seen[var(c[k])] && level[var(c[k])] != 0){
+                        out_learnt[j++] = out_learnt[i];
+                        goto Keep;
+                    }
+                analyze_toclear.push(out_learnt[i]);
+              Keep:;
+            }
+        }
+    }
+#else
+    int i = 0, j = 0;
+#endif
+
+    // Finilize proof logging with conflict clause minimization steps:
+    //
+    if (proof != NULL){
+        sort(analyze_toclear, lastToFirst_lt(trail_pos));
+        for (int k = 0; k < analyze_toclear.size(); k++){
+            Var     v = var(analyze_toclear[k]); assert(level[v] > 0);
+            Clause& c = *reason[v];
+            proof->resolve(c.id(), v);
+            for (int k = 1; k < c.size(); k++)
+                if (level[var(c[k])] == 0)
+                    proof->resolve(unit_id[var(c[k])], var(c[k]));
+        }
+        proof->endChain();
+    }
+    // Clean up:
+    //
+    for (int j = 0; j < out_learnt.size()     ; j++) seen[var(out_learnt     [j])] = 0;
+    for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
+
+    stats.max_literals += out_learnt.size();
+    out_learnt.shrink(i - j);
+    stats.tot_literals += out_learnt.size();
+}
+
+
+// Check if 'p' can be removed. 'min_level' is used to abort early if visiting literals at a level that cannot be removed.
+//
+bool Solver::analyze_removable(Lit p, uint min_level)
+{
+    assert(reason[var(p)] != NULL);
+    analyze_stack.clear(); analyze_stack.push(p);
+    int top = analyze_toclear.size();
+    while (analyze_stack.size() > 0){
+        assert(reason[var(analyze_stack.last())] != NULL);
+        Clause& c = *reason[var(analyze_stack.last())];
+        analyze_stack.pop();
+        for (int i = 1; i < c.size(); i++){
+            Lit p = c[i];
+            if (!analyze_seen[var(p)] && level[var(p)] != 0){
+                if (reason[var(p)] != NULL && ((1 << (level[var(p)] & 31)) & min_level) != 0){
+                    analyze_seen[var(p)] = 1;
+                    analyze_stack.push(p);
+                    analyze_toclear.push(p);
+                }else{
+                    for (int j = top; j < analyze_toclear.size(); j++)
+                        analyze_seen[var(analyze_toclear[j])] = 0;
+                    analyze_toclear.shrink(analyze_toclear.size() - top);
+                    return false;
+                }
+            }
+        }
+    }
+    analyze_toclear.push(p);
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyzeFinal : (confl : Clause*) (skip_first : bool)  ->  [void]
+|  
+|  Description:
+|    Specialized analysis procedure to express the final conflict in terms of assumptions.
+|    'root_level' is allowed to point beyond end of trace (useful if called after conflict while
+|    making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is  ignored (needed
+|    if conflict arose before search even started).
+|________________________________________________________________________________________________@*/
+void Solver::analyzeFinal(Clause* confl, bool skip_first)
+{
+    // -- NOTE! This code is relatively untested. Please report bugs!
+    conflict.clear();
+    if (root_level == 0){
+        if (proof != NULL) conflict_id = proof->last();
+        return; }
+
+    vec<char>&     seen  = analyze_seen;
+    if (proof != NULL) proof->beginChain(confl->id());
+    for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
+        Var     x = var((*confl)[i]);
+        if (level[x] > 0)
+            seen[x] = 1;
+        else
+            if (proof != NULL) proof->resolve(unit_id[x], x);
+    }
+
+    int     start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level];
+    for (int i = start; i >= trail_lim[0]; i--){
+        Var     x = var(trail[i]);
+        if (seen[x]){
+            Clause* r = reason[x];
+            if (r == NULL){
+                assert(level[x] > 0);
+                conflict.push(~trail[i]);
+            }else{
+                Clause& c = *r;
+                if (proof != NULL) proof->resolve(c.id(), x);
+                for (int j = 1; j < c.size(); j++)
+                    if (level[var(c[j])] > 0)
+                        seen[var(c[j])] = 1;
+                    else
+                        if (proof != NULL) proof->resolve(unit_id[var(c[j])], var(c[j]));
+            }
+            seen[x] = 0;
+        }
+    }
+    if (proof != NULL) conflict_id = proof->endChain();
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  enqueue : (p : Lit) (from : Clause*)  ->  [bool]
+|  
+|  Description:
+|    Puts a new fact on the propagation queue as well as immediately updating the variable's value.
+|    Should a conflict arise, FALSE is returned.
+|  
+|  Input:
+|    p    - The fact to enqueue
+|    from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'.
+|           Default value is NULL (no reason).
+|  
+|  Output:
+|    TRUE if fact was enqueued without conflict, FALSE otherwise.
+|________________________________________________________________________________________________@*/
+bool Solver::enqueue(Lit p, Clause* from)
+{
+    if (value(p) != l_Undef)
+        return value(p) != l_False;
+    else{
+        Var     x = var(p);
+        assigns  [x] = toInt(lbool(!sign(p)));
+        level    [x] = decisionLevel();
+        trail_pos[x] = trail.size();
+        reason   [x] = from;
+        trail.push(p);
+        return true;
+    }
+}
+
+
+
+/*_________________________________________________________________________________________________
+|
+|  propagate : [void]  ->  [Clause*]
+|  
+|  Description:
+|    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
+|    otherwise NULL. NOTE! This method has been optimized for speed rather than readability.
+|  
+|    Post-conditions:
+|      * The propagation queue is empty, even if there was a conflict.
+|________________________________________________________________________________________________@*/
+Clause* Solver::propagate()
+{
+    Clause* confl = NULL;
+    while (qhead < trail.size()){
+        stats.propagations++;
+        simpDB_props--;
+
+        Lit            p  = trail[qhead++];     // 'p' is enqueued fact to propagate.
+        vec<Clause*>&  ws = watches[index(p)];
+        Clause**       i,** j,** end;
+
+        for (i = j = (Clause**)ws, end = i + ws.size();  i != end;){
+            Clause& c = **i; i++;
+            // Make sure the false literal is data[1]:
+            Lit false_lit = ~p;
+            if (c[0] == false_lit)
+                c[0] = c[1], c[1] = false_lit;
+
+            assert(c[1] == false_lit);
+
+            // If 0th watch is true, then clause is already satisfied.
+            Lit   first = c[0];
+            lbool val   = value(first);
+            if (val == l_True){
+                *j++ = &c;
+            }else{
+                // Look for new watch:
+                for (int k = 2; k < c.size(); k++)
+                    if (value(c[k]) != l_False){
+                        c[1] = c[k]; c[k] = false_lit;
+                        watches[index(~c[1])].push(&c);
+                        goto FoundWatch; }
+
+                // Did not find watch -- clause is unit under assignment:
+                if (decisionLevel() == 0 && proof != NULL){
+                    // Log the production of this unit clause:
+                    proof->beginChain(c.id());
+                    for (int k = 1; k < c.size(); k++)
+                        proof->resolve(unit_id[var(c[k])], var(c[k]));
+                    ClauseId id = proof->endChain();
+                    assert(unit_id[var(first)] == ClauseId_NULL || value(first) == l_False);    // (if variable already has 'id', it must be with the other polarity and we should have derived the empty clause here)
+                    if (value(first) != l_False)
+                        unit_id[var(first)] = id;
+                    else{
+                        // Empty clause derived:
+                        proof->beginChain(unit_id[var(first)]);
+                        proof->resolve(id, var(first));
+                        proof->endChain();
+                    }
+                }
+
+                *j++ = &c;
+                if (!enqueue(first, &c)){
+                    if (decisionLevel() == 0)
+                        ok = false;
+                    confl = &c;
+                    qhead = trail.size();
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                }
+              FoundWatch:;
+            }
+        }
+        ws.shrink(i - j);
+    }
+
+    return confl;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  reduceDB : ()  ->  [void]
+|  
+|  Description:
+|    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
+|    clauses are clauses that are reason to some assignment. Binary clauses are never removed.
+|________________________________________________________________________________________________@*/
+struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); } };
+void Solver::reduceDB()
+{
+    int     i, j;
+    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity
+
+    sort(learnts, reduceDB_lt());
+    for (i = j = 0; i < learnts.size() / 2; i++){
+        if (learnts[i]->size() > 2 && !locked(learnts[i]))
+            remove(learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < learnts.size(); i++){
+        if (learnts[i]->size() > 2 && !locked(learnts[i]) && learnts[i]->activity() < extra_lim)
+            remove(learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    learnts.shrink(i - j);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  simplifyDB : [void]  ->  [bool]
+|  
+|  Description:
+|    Simplify the clause database according to the current top-level assigment. Currently, the only
+|    thing done here is the removal of satisfied clauses, but more things can be put here.
+|________________________________________________________________________________________________@*/
+void Solver::simplifyDB()
+{
+    if (!ok) return;    // GUARD (public method)
+    assert(decisionLevel() == 0);
+
+    if (propagate() != NULL){
+        ok = false;
+        return; }
+
+    if (nAssigns() == simpDB_assigns || simpDB_props > 0)   // (nothing has changed or preformed a simplification too recently)
+        return;
+
+    // Clear watcher lists:
+    for (int i = simpDB_assigns; i < nAssigns(); i++){
+        Lit p = trail[i];
+        watches[index( p)].clear(true);
+        watches[index(~p)].clear(true);
+    }
+
+    // Remove satisfied clauses:
+    for (int type = 0; type < 2; type++){
+        vec<Clause*>& cs = type ? learnts : clauses;
+        int           j  = 0;
+        for (int i = 0; i < cs.size(); i++){
+            if (!locked(cs[i]) && simplify(cs[i]))
+                remove(cs[i]);
+            else
+                cs[j++] = cs[i];
+        }
+        cs.shrink(cs.size()-j);
+    }
+
+    simpDB_assigns = nAssigns();
+    simpDB_props   = stats.clauses_literals + stats.learnts_literals;   // (shouldn't depend on 'stats' really, but it will do for now)
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&)  ->  [lbool]
+|  
+|  Description:
+|    Search for a model the specified number of conflicts, keeping the number of learnt clauses
+|    below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to
+|    indicate infinity.
+|  
+|  Output:
+|    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
+|    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
+|    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
+|________________________________________________________________________________________________@*/
+lbool Solver::search(int nof_conflicts, int nof_learnts, const SearchParams& params)
+{
+    if (!ok) return l_False;    // GUARD (public method)
+    assert(root_level == decisionLevel());
+
+    stats.starts++;
+    int     conflictC = 0;
+    var_decay = 1 / params.var_decay;
+    cla_decay = 1 / params.clause_decay;
+    model.clear();
+
+    for (;;){
+        Clause* confl = propagate();
+        if (confl != NULL){
+            // CONFLICT
+
+            stats.conflicts++; conflictC++;
+            vec<Lit>    learnt_clause;
+            int         backtrack_level;
+            if (decisionLevel() == root_level){
+                // Contradiction found:
+                analyzeFinal(confl);
+                return l_False; }
+            analyze(confl, learnt_clause, backtrack_level);
+            cancelUntil(max(backtrack_level, root_level));
+            newClause(learnt_clause, true, (proof != NULL) ? proof->last() : ClauseId_NULL);
+            if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;    // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
+            varDecayActivity();
+            claDecayActivity();
+
+        }else{
+            // NO CONFLICT
+
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+                // Reached bound on number of conflicts:
+                progress_estimate = progressEstimate();
+                cancelUntil(root_level);
+                return l_Undef; }
+
+            if (decisionLevel() == 0)
+                // Simplify the set of problem clauses:
+                simplifyDB(), assert(ok);
+
+            if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
+                // Reduce the set of learnt clauses:
+                reduceDB();
+
+            // New variable decision:
+            stats.decisions++;
+            Var next = order.select(params.random_var_freq);
+
+            if (next == var_Undef){
+                // Model found:
+                model.growTo(nVars());
+                for (int i = 0; i < nVars(); i++) model[i] = value(i);
+                cancelUntil(root_level);
+                return l_True;
+            }
+
+            check(assume(~Lit(next)));
+        }
+    }
+}
+
+
+// Return search-space coverage. Not extremely reliable.
+//
+double Solver::progressEstimate()
+{
+    double  progress = 0;
+    double  F = 1.0 / nVars();
+    for (int i = 0; i < nVars(); i++)
+        if (value(i) != l_Undef)
+            progress += pow(F, level[i]);
+    return progress / nVars();
+}
+
+
+// Divide all variable activities by 1e100.
+//
+void Solver::varRescaleActivity()
+{
+    for (int i = 0; i < nVars(); i++)
+        activity[i] *= 1e-100;
+    var_inc *= 1e-100;
+}
+
+
+// Divide all constraint activities by 1e100.
+//
+void Solver::claRescaleActivity()
+{
+    for (int i = 0; i < learnts.size(); i++)
+        learnts[i]->activity() *= 1e-20;
+    cla_inc *= 1e-20;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  solve : (assumps : const vec<Lit>&)  ->  [bool]
+|  
+|  Description:
+|    Top-level solve. If using assumptions (non-empty 'assumps' vector), you must call
+|    'simplifyDB()' first to see that no top-level conflict is present (which would put the solver
+|    in an undefined state).
+|  
+|  Input:
+|    A list of assumptions (unit clauses coded as literals). Pre-condition: The assumptions must
+|    not contain both 'x' and '~x' for any variable 'x'.
+|________________________________________________________________________________________________@*/
+bool Solver::solve(const vec<Lit>& assumps)
+{
+    simplifyDB();
+    if (!ok) return false;
+
+    SearchParams    params(default_params);
+    double  nof_conflicts = 100;
+    double  nof_learnts   = nClauses() / 3;
+    lbool   status        = l_Undef;
+
+    // Perform assumptions:
+    root_level = assumps.size();
+    for (int i = 0; i < assumps.size(); i++){
+        Lit p = assumps[i];
+        assert(var(p) < nVars());
+        if (!assume(p)){
+            if (reason[var(p)] != NULL){
+                analyzeFinal(reason[var(p)], true);
+                conflict.push(~p);
+            }else{
+                assert(proof == NULL || unit_id[var(p)] != ClauseId_NULL);   // (this is the pre-condition above)
+                conflict.clear();
+                conflict.push(~p);
+                if (proof != NULL) conflict_id = unit_id[var(p)];
+            }
+            cancelUntil(0);
+            return false; }
+        Clause* confl = propagate();
+        if (confl != NULL){
+            analyzeFinal(confl), assert(conflict.size() > 0);
+            cancelUntil(0);
+            return false; }
+    }
+    assert(root_level == decisionLevel());
+
+    // Search:
+    if (verbosity >= 1){
+        reportf("==================================[MINISAT]===================================\n");
+        reportf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
+        reportf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
+        reportf("==============================================================================\n");
+    }
+
+    while (status == l_Undef){
+        if (verbosity >= 1){
+            reportf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nClauses(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100);
+            fflush(stdout);
+        }
+        status = search((int)nof_conflicts, (int)nof_learnts, params);
+        nof_conflicts *= 1.5;
+        nof_learnts   *= 1.1;
+    }
+    if (verbosity >= 1)
+        reportf("==============================================================================\n");
+
+    cancelUntil(0);
+    return status == l_True;
+}

src/Solver.h

@@ -0,0 +1,212 @@
+/****************************************************************************************[Solver.h]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Solver_h
+#define Solver_h
+
+#include "SolverTypes.h"
+#include "VarOrder.h"
+#include "Proof.h"
+
+// Redfine if you want output to go somewhere else:
+#define reportf(format, args...) ( printf(format , ## args), fflush(stdout) )
+
+
+//=================================================================================================
+// Solver -- the main class:
+
+
+struct SolverStats {
+    int64   starts, decisions, propagations, conflicts;
+    int64   clauses_literals, learnts_literals, max_literals, tot_literals;
+    SolverStats() : starts(0), decisions(0), propagations(0), conflicts(0)
+      , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) { }
+};
+
+
+struct SearchParams {
+    double  var_decay, clause_decay, random_var_freq;    // (reasonable values are: 0.95, 0.999, 0.02)    
+    SearchParams(double v = 1, double c = 1, double r = 0) : var_decay(v), clause_decay(c), random_var_freq(r) { }
+};
+
+
+class Solver {
+protected:
+    // Solver state:
+    //
+    bool                ok;               // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
+    vec<Clause*>        clauses;          // List of problem clauses.
+    vec<Clause*>        learnts;          // List of learnt clauses.
+    vec<ClauseId>       unit_id;          // 'unit_id[var]' is the clause ID for the unit literal 'var' or '~var' (if set at toplevel).
+    double              cla_inc;          // Amount to bump next clause with.
+    double              cla_decay;        // INVERSE decay factor for clause activity: stores 1/decay.
+
+    vec<double>         activity;         // A heuristic measurement of the activity of a variable.
+    double              var_inc;          // Amount to bump next variable with.
+    double              var_decay;        // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
+    VarOrder            order;            // Keeps track of the decision variable order.
+
+    vec<vec<Clause*> >  watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+    vec<char>           assigns;          // The current assignments (lbool:s stored as char:s).
+    vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
+    vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail[]'.
+    vec<Clause*>        reason;           // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
+    vec<int>            level;            // 'level[var]' is the decision level at which assignment was made.
+    vec<int>            trail_pos;        // 'trail_pos[var]' is the variable's position in 'trail[]'. This supersedes 'level[]' in some sense, and 'level[]' will probably be removed in future releases.
+    int                 root_level;       // Level of first proper decision.
+    int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
+    int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplifyDB()'.
+    int64               simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplifyDB()'.
+
+    // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which is used:
+    //
+    vec<char>           analyze_seen;
+    vec<Lit>            analyze_stack;
+    vec<Lit>            analyze_toclear;
+    Clause*             propagate_tmpbin;
+    Clause*             analyze_tmpbin;
+    vec<Lit>            addUnit_tmp;
+    vec<Lit>            addBinary_tmp;
+    vec<Lit>            addTernary_tmp;
+
+    // Main internal methods:
+    //
+    bool        assume           (Lit p);
+    void        cancelUntil      (int level);
+    void        record           (const vec<Lit>& clause);
+
+    void        analyze          (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
+    bool        analyze_removable(Lit p, uint min_level);                                 // (helper method for 'analyze()')
+    void        analyzeFinal     (Clause* confl, bool skip_first = false);
+    bool        enqueue          (Lit fact, Clause* from = NULL);
+    Clause*     propagate        ();
+    void        reduceDB         ();
+    Lit         pickBranchLit    (const SearchParams& params);
+    lbool       search           (int nof_conflicts, int nof_learnts, const SearchParams& params);
+    double      progressEstimate ();
+
+    // Activity:
+    //
+    void     varBumpActivity(Lit p) {
+        if (var_decay < 0) return;     // (negative decay means static variable order -- don't bump)
+        if ( (activity[var(p)] += var_inc) > 1e100 ) varRescaleActivity();
+        order.update(var(p)); }
+    void     varDecayActivity  () { if (var_decay >= 0) var_inc *= var_decay; }
+    void     varRescaleActivity();
+    void     claDecayActivity  () { cla_inc *= cla_decay; }
+    void     claRescaleActivity();
+
+    // Operations on clauses:
+    //
+    void     newClause(const vec<Lit>& ps, bool learnt = false, ClauseId id = ClauseId_NULL);
+    void     claBumpActivity (Clause* c) { if ( (c->activity() += cla_inc) > 1e20 ) claRescaleActivity(); }
+    void     remove          (Clause* c, bool just_dealloc = false);
+    bool     locked          (const Clause* c) const { return reason[var((*c)[0])] == c; }
+    bool     simplify        (Clause* c) const;
+
+    int      decisionLevel() const { return trail_lim.size(); }
+
+public:
+    Solver() : ok               (true)
+             , cla_inc          (1)
+             , cla_decay        (1)
+             , var_inc          (1)
+             , var_decay        (1)
+             , order            (assigns, activity)
+             , qhead            (0)
+             , simpDB_assigns   (0)
+             , simpDB_props     (0)
+             , default_params   (SearchParams(0.95, 0.999, 0.02))
+             , expensive_ccmin  (true)
+             , proof            (NULL)
+             , verbosity        (0)
+             , progress_estimate(0)
+             , conflict_id      (ClauseId_NULL)
+             {
+                vec<Lit> dummy(2,lit_Undef);
+                propagate_tmpbin = Clause_new(false, dummy);
+                analyze_tmpbin   = Clause_new(false, dummy);
+                addUnit_tmp   .growTo(1);
+                addBinary_tmp .growTo(2);
+                addTernary_tmp.growTo(3);
+             }
+
+   ~Solver() {
+       for (int i = 0; i < learnts.size(); i++) remove(learnts[i], true);
+       for (int i = 0; i < clauses.size(); i++) if (clauses[i] != NULL) remove(clauses[i], true);
+       remove(propagate_tmpbin, true);
+       remove(analyze_tmpbin, true);
+    }
+
+    // Helpers: (semi-internal)
+    //
+    lbool   value(Var x) const { return toLbool(assigns[x]); }
+    lbool   value(Lit p) const { return sign(p) ? ~toLbool(assigns[var(p)]) : toLbool(assigns[var(p)]); }
+
+    int     nAssigns() { return trail.size(); }
+    int     nClauses() { return clauses.size(); }
+    int     nLearnts() { return learnts.size(); }
+
+    // Statistics: (read-only member variable)
+    //
+    SolverStats     stats;
+
+    // Mode of operation:
+    //
+    SearchParams    default_params;     // Restart frequency etc.
+    bool            expensive_ccmin;    // Controls conflict clause minimization. TRUE by default.
+    Proof*          proof;              // Set this directly after constructing 'Solver' to enable proof logging. Initialized to NULL.
+    int             verbosity;          // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+    // Problem specification:
+    //
+    Var     newVar    ();
+    int     nVars     ()                    { return assigns.size(); }
+    void    addUnit   (Lit p)               { addUnit_tmp   [0] = p; addClause(addUnit_tmp); }
+    void    addBinary (Lit p, Lit q)        { addBinary_tmp [0] = p; addBinary_tmp [1] = q; addClause(addBinary_tmp); }
+    void    addTernary(Lit p, Lit q, Lit r) { addTernary_tmp[0] = p; addTernary_tmp[1] = q; addTernary_tmp[2] = r; addClause(addTernary_tmp); }
+    void    addClause (const vec<Lit>& ps)  { newClause(ps); }  // (used to be a difference between internal and external method...)
+
+    // Solving:
+    //
+    bool    okay() { return ok; }       // FALSE means solver is in an conflicting state (must never be used again!)
+    void    simplifyDB();
+    bool    solve(const vec<Lit>& assumps);
+    bool    solve() { vec<Lit> tmp; return solve(tmp); }
+
+    double      progress_estimate;  // Set by 'search()'.
+    vec<lbool>  model;              // If problem is satisfiable, this vector contains the model (if any).
+    vec<Lit>    conflict;           // If problem is unsatisfiable under assumptions, this vector represent the conflict clause expressed in the assumptions.
+    ClauseId    conflict_id;        // (In proof logging mode only.) ID for the clause 'conflict' (for proof traverseral). NOTE! The empty clause is always the last clause derived, but for conflicts under assumption, this is not necessarly true.
+};
+
+
+//=================================================================================================
+// Debug:
+
+
+#define L_LIT    "%s%d"
+#define L_lit(p) sign(p)?"-":"", var(p)+1
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+inline void check(bool expr) { assert(expr); }
+
+
+//=================================================================================================
+#endif

src/SolverTypes.h

@@ -0,0 +1,139 @@
+/***********************************************************************************[SolverTypes.h]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+
+#ifndef SolverTypes_h
+#define SolverTypes_h
+
+#ifndef Global_h
+#include "Global.h"
+#endif
+
+
+//=================================================================================================
+// Variables, literals, clause IDs:
+
+
+// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N,
+// so that they can be used as array indices.
+
+typedef int Var;
+#define var_Undef (-1)
+
+
+class Lit {
+    int     x;
+public:
+    Lit() : x(2*var_Undef) {}   // (lit_Undef)
+    explicit Lit(Var var, bool sgn = false) : x((var+var) + (int)sgn) {}
+    friend Lit operator ~ (Lit p);
+
+    friend bool sign  (Lit p);
+    friend int  var   (Lit p);
+    friend int  index (Lit p);
+    friend Lit  toLit (int i);
+    friend Lit  unsign(Lit p);
+    friend Lit  id    (Lit p, bool sgn);
+
+    friend bool operator == (Lit p, Lit q);
+    friend bool operator <  (Lit p, Lit q);
+
+    uint hash() const { return (uint)x; }
+};
+inline Lit operator ~ (Lit p) { Lit q; q.x = p.x ^ 1; return q; }
+inline bool sign  (Lit p) { return p.x & 1; }
+inline int  var   (Lit p) { return p.x >> 1; }
+inline int  index (Lit p) { return p.x; }                // A "toInt" method that guarantees small, positive integers suitable for array indexing.
+inline Lit  toLit (int i) { Lit p; p.x = i; return p; }  // Inverse of 'index()'.
+inline Lit  unsign(Lit p) { Lit q; q.x = p.x & ~1; return q; }
+inline Lit  id    (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; }
+inline bool operator == (Lit p, Lit q) { return index(p) == index(q); }
+inline bool operator <  (Lit p, Lit q) { return index(p)  < index(q); }  // '<' guarantees that p, ~p are adjacent in the ordering.
+
+const Lit lit_Undef(var_Undef, false);  // }- Useful special constants.
+const Lit lit_Error(var_Undef, true );  // }
+
+inline int toDimacs(Lit p) { return sign(p) ? -var(p) - 1 : var(p) + 1; }
+
+
+//=================================================================================================
+// Clause -- a simple class for representing a clause:
+
+
+typedef int ClauseId;     // (might have to use uint64 one day...)
+const   int ClauseId_NULL = INT_MIN;
+
+//- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+
+class Clause {
+    uint    size_learnt;
+    Lit     data[1];
+public:
+    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+    Clause(bool learnt, const vec<Lit>& ps, ClauseId id_ = ClauseId_NULL) {
+        size_learnt = (ps.size() << 1) | (int)learnt;
+        for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
+        if (learnt) activity() = 0;
+        if (id_ != ClauseId_NULL) id() = id_; }
+
+    // -- use this function instead:
+    friend Clause* Clause_new(bool, const vec<Lit>&, ClauseId);
+
+    int       size        ()      const { return size_learnt >> 1; }
+    bool      learnt      ()      const { return size_learnt & 1; }
+    Lit       operator [] (int i) const { return data[i]; }
+    Lit&      operator [] (int i)       { return data[i]; }
+    float&    activity    ()      const { return *((float*)&data[size()]); }
+    ClauseId& id          ()      const { return *((ClauseId*)&data[size() + (int)learnt()]); }
+};
+
+inline Clause* Clause_new(bool learnt, const vec<Lit>& ps, ClauseId id = ClauseId_NULL) {
+    assert(sizeof(Lit)      == sizeof(uint));
+    assert(sizeof(float)    == sizeof(uint));
+    assert(sizeof(ClauseId) == sizeof(uint));
+    void*   mem = xmalloc<char>(sizeof(Clause) + sizeof(uint)*(ps.size() + (int)learnt + (int)(id != ClauseId_NULL)));
+    return new (mem) Clause(learnt, ps, id); }
+
+
+//=================================================================================================
+// GClause -- Generalize clause:
+
+
+// Either a pointer to a clause or a literal.
+class GClause {
+    void*   data;
+    GClause(void* d) : data(d) {}
+public:
+    friend GClause GClause_new(Lit p);
+    friend GClause GClause_new(Clause* c);
+
+    bool        isLit    () const { return ((uintp)data & 1) == 1; }
+    Lit         lit      () const { return toLit(((intp)data) >> 1); }
+    Clause*     clause   () const { return (Clause*)data; }
+    bool        operator == (GClause c) const { return data == c.data; }
+    bool        operator != (GClause c) const { return data != c.data; }
+};
+inline GClause GClause_new(Lit p)     { return GClause((void*)(((intp)index(p) << 1) + 1)); }
+inline GClause GClause_new(Clause* c) { assert(((uintp)c & 1) == 0); return GClause((void*)c); }
+
+#define GClause_NULL GClause_new((Clause*)NULL)
+
+
+//=================================================================================================
+#endif

src/Sort.h

@@ -0,0 +1,131 @@
+/******************************************************************************************[Sort.h]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Sort_h
+#define Sort_h
+
+
+//=================================================================================================
+
+
+template<class T>
+struct LessThan_default {
+    bool operator () (T x, T y) { return x < y; }
+};
+
+
+//=================================================================================================
+
+
+template <class T, class LessThan>
+void selectionSort(T* array, int size, LessThan lt)
+{
+    int     i, j, best_i;
+    T       tmp;
+
+    for (i = 0; i < size-1; i++){
+        best_i = i;
+        for (j = i+1; j < size; j++){
+            if (lt(array[j], array[best_i]))
+                best_i = j;
+        }
+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+    }
+}
+template <class T> static inline void selectionSort(T* array, int size) {
+    selectionSort(array, size, LessThan_default<T>()); }
+
+
+template <class T, class LessThan>
+void sort(T* array, int size, LessThan lt, double& seed)
+{
+    if (size <= 15)
+        selectionSort(array, size, lt);
+
+    else{
+        T           pivot = array[irand(seed, size)];
+        T           tmp;
+        int         i = -1;
+        int         j = size;
+
+        for(;;){
+            do i++; while(lt(array[i], pivot));
+            do j--; while(lt(pivot, array[j]));
+
+            if (i >= j) break;
+
+            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+        }
+
+        sort(array    , i     , lt, seed);
+        sort(&array[i], size-i, lt, seed);
+    }
+}
+template <class T, class LessThan> void sort(T* array, int size, LessThan lt) {
+    double  seed = 91648253; sort(array, size, lt, seed); }
+template <class T> static inline void sort(T* array, int size) {
+    sort(array, size, LessThan_default<T>()); }
+
+
+template <class T, class LessThan>
+void sortUnique(T* array, int& size, LessThan lt)
+{
+    int         i, j;
+    T           last;
+
+    if (size == 0) return;
+
+    sort(array, size, lt);
+
+    i    = 1;
+    last = array[0];
+    for (j = 1; j < size; j++){
+        if (lt(last, array[j])){
+            last = array[i] = array[j];
+            i++; }
+    }
+
+    size = i;
+}
+template <class T> static inline void sortUnique(T* array, int& size) {
+    sortUnique(array, size, LessThan_default<T>()); }
+
+
+//=================================================================================================
+// For 'vec's:
+
+
+template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {
+    sort((T*)v, v.size(), lt); }
+template <class T> void sort(vec<T>& v) {
+    sort(v, LessThan_default<T>()); }
+
+
+template <class T, class LessThan> void sortUnique(vec<T>& v, LessThan lt) {
+    int     size = v.size();
+    T*      data = v.release();
+    sortUnique(data, size, lt);
+    v.~vec<T>();
+    new (&v) vec<T>(data, size); }
+template <class T> void sortUnique(vec<T>& v) {
+    sortUnique(v, LessThan_default<T>()); }
+
+
+//=================================================================================================
+#endif

src/VarOrder.h

@@ -0,0 +1,96 @@
+/**************************************************************************************[VarOrder.h]
+MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef VarOrder_h
+#define VarOrder_h
+
+#include "SolverTypes.h"
+#include "Heap.h"
+
+
+//=================================================================================================
+
+
+struct VarOrder_lt {
+    const vec<double>&  activity;
+    bool operator () (Var x, Var y) { return activity[x] > activity[y]; }
+    VarOrder_lt(const vec<double>&  act) : activity(act) { }
+};
+
+class VarOrder {
+    const vec<char>&    assigns;     // var->val. Pointer to external assignment table.
+    const vec<double>&  activity;    // var->act. Pointer to external activity table.
+    Heap<VarOrder_lt>   heap;
+    double              random_seed; // For the internal random number generator
+
+public:
+    VarOrder(const vec<char>& ass, const vec<double>& act) :
+        assigns(ass), activity(act), heap(VarOrder_lt(act)), random_seed(91648253)
+        { }
+
+    inline void newVar(void);
+    inline void update(Var x);                  // Called when variable increased in activity.
+    inline void undo(Var x);                    // Called when variable is unassigned and may be selected again.
+    inline Var  select(double random_freq =.0); // Selects a new, unassigned variable (or 'var_Undef' if none exists).
+};
+
+
+void VarOrder::newVar(void)
+{
+    heap.setBounds(assigns.size());
+    heap.insert(assigns.size()-1);
+}
+
+
+void VarOrder::update(Var x)
+{
+    if (heap.inHeap(x))
+        heap.increase(x);
+}
+
+
+void VarOrder::undo(Var x)
+{
+    if (!heap.inHeap(x))
+        heap.insert(x);
+}
+
+
+Var VarOrder::select(double random_var_freq)
+{
+    // Random decision:
+    if (drand(random_seed) < random_var_freq && !heap.empty()){
+        Var next = irand(random_seed,assigns.size());
+        if (toLbool(assigns[next]) == l_Undef)
+            return next;
+    }
+
+    // Activity based decision:
+    while (!heap.empty()){
+        Var next = heap.getmin();
+        if (toLbool(assigns[next]) == l_Undef)
+            return next;
+    }
+
+    return var_Undef;
+}
+
+
+//=================================================================================================
+#endif