add unpatched version of 1.14 source

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

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

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.

Main.C

@@ -0,0 +1,244 @@
+/******************************************************************************************[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 <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();
+    reportf("restarts              : %"I64_fmt"\n", stats.starts);
+    reportf("conflicts             : %-12"I64_fmt"   (%.0f /sec)\n", stats.conflicts   , stats.conflicts   /cpu_time);
+    reportf("decisions             : %-12"I64_fmt"   (%.0f /sec)\n", stats.decisions   , stats.decisions   /cpu_time);
+    reportf("propagations          : %-12"I64_fmt"   (%.0f /sec)\n", stats.propagations, stats.propagations/cpu_time);
+    reportf("conflict literals     : %-12"I64_fmt"   (%4.2f %% deleted)\n", stats.tot_literals, (stats.max_literals - stats.tot_literals)*100 / (double)stats.max_literals);
+    if (mem_used != 0) reportf("Memory used           : %.2f MB\n", mem_used / 1048576.0);
+    reportf("CPU time              : %g s\n", cpu_time);
+}
+
+Solver* solver;
+static void SIGINT_handler(int signum) {
+    reportf("\n"); reportf("*** INTERRUPTED ***\n");
+    printStats(solver->stats);
+    reportf("\n"); reportf("*** INTERRUPTED ***\n");
+    exit(1); }
+
+
+//=================================================================================================
+// Main:
+
+
+int main(int argc, char** argv)
+{
+    Solver      S;
+
+    if (argc == 2 && (strcmp(argv[1], "-h") == 0 || strcmp(argv[1], "--help") == 0))
+        reportf("USAGE: %s <input-file> <result-output-file>\n  where the input may be either in plain/gzipped DIMACS format or in BCNF.\n", argv[0]),
+        exit(0);
+
+    if (argc >= 2 && strlen(argv[1]) >= 5 && strcmp(&argv[1][strlen(argv[1])-5], ".bcnf") == 0)
+        parse_BCNF(argv[1], S);
+    else{
+        if (argc == 1)
+            reportf("Reading from standard input... Use '-h' or '--help' for help.\n");
+
+        gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
+        if (in == NULL)
+            fprintf(stderr, "ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]),
+            exit(1);
+        parse_DIMACS(in, S);
+        gzclose(in);
+    }
+    FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
+
+    if (!S.okay()){
+        if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
+        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);
+    }
+
+    exit(S.okay() ? 10 : 20);     // (faster than "return", which will invoke the destructor for 'Solver')
+}

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

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.

Solver.C

@@ -0,0 +1,781 @@
+/****************************************************************************************[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>
+
+
+//=================================================================================================
+// Helper functions:
+
+
+bool removeWatch(vec<GClause>& ws, GClause elem)    // Pre-condition: 'elem' must exists in 'ws' OR 'ws' must be empty.
+{
+    if (ws.size() == 0) return false;     // (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();
+    return true;
+}
+
+
+//=================================================================================================
+// Operations on clauses:
+
+
+/*_________________________________________________________________________________________________
+|
+|  newClause : (ps : const vec<Lit>&) (learnt : bool)  ->  [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.
+|  
+|  Effect:
+|    Activity heuristics are updated.
+|________________________________________________________________________________________________@*/
+void Solver::newClause(const vec<Lit>& ps_, bool learnt)
+{
+    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;
+        for (i = j = 0; i < qs.size(); i++)
+            if (value(qs[i]) != l_False)
+                qs[j++] = qs[i];
+        qs.shrink(i - j);
+    }
+    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 (!enqueue(ps[0]))
+            ok = false;
+
+    }else if (ps.size() == 2){
+        // Create special binary clause watch:
+        watches[index(~ps[0])].push(GClause_new(ps[1]));
+        watches[index(~ps[1])].push(GClause_new(ps[0]));
+
+        if (learnt){
+            check(enqueue(ps[0], GClause_new(~ps[1])));
+            stats.learnts_literals += ps.size();
+        }else
+            stats.clauses_literals += ps.size();
+        n_bin_clauses++;
+
+    }else{
+        // Allocate clause:
+        Clause* c   = Clause_new(learnt, ps);
+
+        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];
+
+            // Bump, enqueue, store clause:
+            claBumpActivity(c);         // (newly learnt clauses should be considered active)
+            check(enqueue((*c)[0], GClause_new(c)));
+            learnts.push(c);
+            stats.learnts_literals += c->size();
+        }else{
+            // Store clause:
+            clauses.push(c);
+            stats.clauses_literals += c->size();
+        }
+        // Watch clause:
+        watches[index(~(*c)[0])].push(GClause_new(c));
+        watches[index(~(*c)[1])].push(GClause_new(c));
+    }
+}
+
+
+// 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){
+        if (c->size() == 2)
+            removeWatch(watches[index(~(*c)[0])], GClause_new((*c)[1])),
+            removeWatch(watches[index(~(*c)[1])], GClause_new((*c)[0]));
+        else
+            removeWatch(watches[index(~(*c)[0])], GClause_new(c)),
+            removeWatch(watches[index(~(*c)[1])], GClause_new(c));
+    }
+
+    if (c->learnt()) stats.learnts_literals -= c->size();
+    else             stats.clauses_literals -= c->size();
+
+    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(GClause_NULL);
+    assigns     .push(toInt(l_Undef));
+    level       .push(-1);
+    activity    .push(0);
+    order       .newVar();
+    analyze_seen.push(0);
+    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] = GClause_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.
+|  
+|    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'.
+|  
+|  Effect:
+|    Will undo part of the trail, upto but not beyond the assumption of the current decision level.
+|________________________________________________________________________________________________@*/
+void Solver::analyze(Clause* _confl, vec<Lit>& out_learnt, int& out_btlevel)
+{
+    GClause confl = GClause_new(_confl);
+    vec<char>&     seen  = analyze_seen;
+    int            pathC = 0;
+    Lit            p     = lit_Undef;
+
+    // Generate conflict clause:
+    //
+    out_learnt.push();      // (leave room for the asserting literal)
+    out_btlevel = 0;
+    int index = trail.size()-1;
+    do{
+        assert(confl != GClause_NULL);          // (otherwise should be UIP)
+
+        Clause& c = confl.isLit() ? ((*analyze_tmpbin)[1] = confl.lit(), *analyze_tmpbin)
+                                  : *confl.clause();
+        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)] && 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)]);
+                }
+            }
+        }
+
+        // Select next clause to look at:
+        while (!seen[var(trail[index--])]);
+        p     = trail[index+1];
+        confl = reason[var(p)];
+        seen[var(p)] = 0;
+        pathC--;
+
+    }while (pathC > 0);
+    out_learnt[0] = ~p;
+
+    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)
+
+        out_learnt.copyTo(analyze_toclear);
+        for (i = j = 1; i < out_learnt.size(); i++)
+            if (reason[var(out_learnt[i])] == GClause_NULL || !analyze_removable(out_learnt[i], min_level))
+                out_learnt[j++] = out_learnt[i];
+    }else{
+        // Simplify conflict clause (a little):
+        //
+        out_learnt.copyTo(analyze_toclear);
+        for (i = j = 1; i < out_learnt.size(); i++){
+            GClause r = reason[var(out_learnt[i])];
+            if (r == GClause_NULL)
+                out_learnt[j++] = out_learnt[i];
+            else if (r.isLit()){
+                Lit q = r.lit();
+                if (!seen[var(q)] && level[var(q)] != 0)
+                    out_learnt[j++] = out_learnt[i];
+            }else{
+                Clause& c = *r.clause();
+                for (int k = 1; k < c.size(); k++)
+                    if (!seen[var(c[k])] && level[var(c[k])] != 0){
+                        out_learnt[j++] = out_learnt[i];
+                        break; }
+            }
+        }
+    }
+
+    stats.max_literals += out_learnt.size();
+    out_learnt.shrink(i - j);
+    stats.tot_literals += out_learnt.size();
+
+    for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
+}
+
+
+// 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)] != GClause_NULL);
+    analyze_stack.clear(); analyze_stack.push(p);
+    int top = analyze_toclear.size();
+    while (analyze_stack.size() > 0){
+        assert(reason[var(analyze_stack.last())] != GClause_NULL);
+        GClause r = reason[var(analyze_stack.last())]; analyze_stack.pop();
+        Clause& c = r.isLit() ? ((*analyze_tmpbin)[1] = r.lit(), *analyze_tmpbin)
+                              : *r.clause();
+        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)] != GClause_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;
+                }
+            }
+        }
+    }
+
+    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) return;
+
+    vec<char>&     seen  = analyze_seen;
+    for (int i = skip_first ? 1 : 0; i < confl->size(); i++){
+        Var     x = var((*confl)[i]);
+        if (level[x] > 0)
+            seen[x] = 1;
+    }
+
+    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]){
+            GClause r = reason[x];
+            if (r == GClause_NULL){
+                assert(level[x] > 0);
+                conflict.push(~trail[i]);
+            }else{
+                if (r.isLit()){
+                    Lit p = r.lit();
+                    if (level[var(p)] > 0)
+                        seen[var(p)] = 1;
+                }else{
+                    Clause& c = *r.clause();
+                    for (int j = 1; j < c.size(); j++)
+                        if (level[var(c[j])] > 0)
+                            seen[var(c[j])] = 1;
+                }
+            }
+            seen[x] = 0;
+        }
+    }
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  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, GClause from)
+{
+    if (value(p) != l_Undef)
+        return value(p) != l_False;
+    else{
+        assigns[var(p)] = toInt(lbool(!sign(p)));
+        level  [var(p)] = decisionLevel();
+        reason [var(p)] = 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.
+|  
+|    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<GClause>&  ws  = watches[index(p)];
+        GClause*       i,* j, *end;
+
+        for (i = j = (GClause*)ws, end = i + ws.size();  i != end;){
+            if (i->isLit()){
+                if (!enqueue(i->lit(), GClause_new(p))){
+                    if (decisionLevel() == 0)
+                        ok = false;
+                    confl = propagate_tmpbin;
+                    (*confl)[1] = ~p;
+                    (*confl)[0] = i->lit();
+
+                    qhead = trail.size();
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                }else
+                    *j++ = *i++;
+            }else{
+                Clause& c = *i->clause(); i++;
+                assert(c.size() > 2);
+                // 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++ = GClause_new(&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(GClause_new(&c));
+                            goto FoundWatch; }
+
+                    // Did not find watch -- clause is unit under assignment:
+                    *j++ = GClause_new(&c);
+                    if (!enqueue(first, GClause_new(&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];
+        vec<GClause>& ws = watches[index(~p)];
+        for (int j = 0; j < ws.size(); j++)
+            if (ws[j].isLit())
+                if (removeWatch(watches[index(~ws[j].lit())], GClause_new(p)))  // (remove binary GClause from "other" watcher list)
+                    n_bin_clauses--;
+        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]))  // (the test for 'locked()' is currently superfluous, but without it the reason-graph is not correctly maintained for decision level 0)
+                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);
+            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).
+|________________________________________________________________________________________________@*/
+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)){
+            GClause r = reason[var(p)];
+            if (r != GClause_NULL){
+                Clause* confl;
+                if (r.isLit()){
+                    confl = propagate_tmpbin;
+                    (*confl)[1] = ~p;
+                    (*confl)[0] = r.lit();
+                }else
+                    confl = r.clause();
+                analyzeFinal(confl, true);
+                conflict.push(~p);
+            }else
+                conflict.clear(),
+                conflict.push(~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);
+        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;
+}

Solver.h

@@ -0,0 +1,206 @@
+/****************************************************************************************[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"
+
+// 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.
+    int                 n_bin_clauses;    // Keep track of number of binary clauses "inlined" into the watcher lists (we do this primarily to get identical behavior to the version without the binary clauses trick).
+    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<GClause> >  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<GClause>        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.
+    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;
+    Clause*             solve_tmpunit;
+    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, GClause from = GClause_new((Clause*)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);
+    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 { GClause r = reason[var((*c)[0])]; return !r.isLit() && r.clause() == c; }
+    bool     simplify        (Clause* c) const;
+
+    int      decisionLevel() const { return trail_lim.size(); }
+
+public:
+    Solver() : ok               (true)
+             , n_bin_clauses    (0)
+             , 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)
+             , verbosity        (0)
+             , progress_estimate(0)
+             {
+                vec<Lit> dummy(2,lit_Undef);
+                propagate_tmpbin = Clause_new(false, dummy);
+                analyze_tmpbin   = Clause_new(false, dummy);
+                dummy.pop();
+                solve_tmpunit    = Clause_new(false, dummy);
+                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); }
+
+    // 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() + n_bin_clauses; }   // (minor difference from MiniSat without the GClause trick: learnt binary clauses will be counted as original clauses)
+    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.
+    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)               { if (ok) ok = enqueue(p); }
+    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 (possibly under assumptions), this vector represent the conflict clause expressed in the assumptions.
+};
+
+
+//=================================================================================================
+// Debug:
+
+
+#define L_LIT    "%sx%d"
+#define L_lit(p) sign(p)?"~":"", var(p)
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+inline void check(bool expr) { assert(expr); }
+
+
+//=================================================================================================
+#endif

SolverTypes.h

@@ -0,0 +1,130 @@
+/***********************************************************************************[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:
+
+
+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) {
+        size_learnt = (ps.size() << 1) | (int)learnt;
+        for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
+        if (learnt) activity() = 0; }
+
+    // -- use this function instead:
+    friend Clause* Clause_new(bool learnt, const vec<Lit>& ps);
+
+    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()]); }
+};
+inline Clause* Clause_new(bool learnt, const vec<Lit>& ps) {
+    assert(sizeof(Lit)      == sizeof(uint));
+    assert(sizeof(float)    == sizeof(uint));
+    void*   mem = xmalloc<char>(sizeof(Clause) - sizeof(Lit) + sizeof(uint)*(ps.size() + (int)learnt));
+    return new (mem) Clause(learnt, ps); }
+
+
+//=================================================================================================
+// 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

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

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.

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