add unpatched version of 1.12b source

Constraints.C

@@ -0,0 +1,266 @@
+/**************************************************************************************************
+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 "Constraints.h"
+#include "Solver.h"
+#include "Sort.h"
+
+
+//=================================================================================================
+// Helpers:
+
+
+void removeWatch(vec<Constr*>& ws, Constr* elem)
+{
+    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();
+}
+
+
+//=================================================================================================
+// Clause constraint:
+
+
+// Returns FALSE if top-level conflict detected (must be handled); TRUE otherwise.
+// 'out_clause' may be set to NULL if clause is already satisfied by the top-level assignment.
+//
+bool Clause_new(Solver& S, const vec<Lit>& ps_, bool learnt, Clause*& out_clause)
+{
+    vec<Lit>    qs;
+    if (&out_clause != NULL) out_clause = NULL;
+
+    if (!learnt){
+        assert(S.decisionLevel() == 0);
+        ps_.copyTo(qs);             // Make a copy of the input vector.
+
+        // Remove false literals:
+        for (int i = 0; i < qs.size();){
+            if (S.value(qs[i]) != l_Undef){
+                if (S.value(qs[i]) == l_True)
+                    return true;    // Clause always true -- don't add anything.
+                else
+                    qs[i] = qs.last(),
+                    qs.pop();
+            }else
+                i++;
+        }
+
+        // Remove duplicates:
+        sortUnique(qs);
+        for (int i = 0; i < qs.size()-1; i++){
+            if (qs[i] == ~qs[i+1])
+                return true;        // Clause always true -- don't add anything.
+        }
+    }
+    const vec<Lit>& ps = learnt ? ps_ : qs;     // 'ps' is now the (possibly) reduced vector of literals.
+
+    if (ps.size() == 0)
+        return false;
+    else if (ps.size() == 1)
+        return S.enqueue(ps[0]);
+    else{
+        // Allocate clause:
+        assert(sizeof(Lit)   == sizeof(unsigned));
+        assert(sizeof(float) == sizeof(unsigned));
+        void*   mem = xmalloc<char>(sizeof(Clause) + sizeof(unsigned)*(ps.size() + (int)learnt));
+        Clause* c   = new (mem) Clause;
+
+        c->size_learnt = (int)learnt | (ps.size() << 1);
+        for (int i = 0; i < ps.size(); i++) c->data[i] = ps[i];
+        if (learnt) c->activity() = 0.0;
+
+        // For learnt clauses only:
+        if (learnt){
+            // Put the second watch on the literal with highest decision level:
+            int     max_i = 1;
+            int     max   = S.level[var(ps[1])];
+            for (int i = 2; i < ps.size(); i++)
+                if (S.level[var(ps[i])] > max)
+                    max   = S.level[var(ps[i])],
+                    max_i = i;
+            c->data[1]     = ps[max_i];
+            c->data[max_i] = ps[1];
+
+            // Bumping:
+            S.claBumpActivity(c); // (newly learnt clauses should be considered active)
+
+            S.stats.learnts++;
+            S.stats.learnts_literals += c->size();
+        }else{
+            S.stats.clauses++;
+            S.stats.clauses_literals += c->size();
+        }
+
+        // Store clause:
+        S.watches[index(~c->data[0])].push(c);
+        S.watches[index(~c->data[1])].push(c);
+        if (&out_clause != NULL) out_clause = c;
+
+        return true;
+    }
+}
+
+
+bool Clause::locked(const Solver& S) const {
+    return (const Clause *)S.reason[var(data[0])] == this; }
+
+
+void Clause::remove(Solver& S, bool just_dealloc)
+{
+    if (!just_dealloc){
+        removeWatch(S.watches[index(~data[0])], this);
+        removeWatch(S.watches[index(~data[1])], this); }
+
+    if (learnt()){
+        S.stats.learnts--;
+        S.stats.learnts_literals -= size();
+    }else{
+        S.stats.clauses--;
+        S.stats.clauses_literals -= size();
+    }
+
+    xfree(this);
+}
+
+
+// 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 Clause::simplify(Solver& S)
+{
+    assert(S.decisionLevel() == 0);
+    for (int i = 0; i < size(); i++){
+        if (S.value(data[i]) == l_True)
+            return true;
+    }
+    return false;
+}
+
+
+// 'p' is the literal that became TRUE
+bool Clause::propagate(Solver& S, Lit p, bool& keep_watch)
+{
+    // Make sure the false literal is data[1]:
+    Lit     false_lit = ~p;
+    if (data[0] == false_lit)
+        data[0] = data[1], data[1] = false_lit;
+    assert(data[1] == false_lit);
+
+    // If 0th watch is true, then clause is already satisfied.
+    if (S.value(data[0]) == l_True){
+        keep_watch = true;
+        return true; }
+
+    // Look for new watch:
+    for (int i = 2; i < size(); i++){
+        if (S.value(data[i]) != l_False){
+            data[1] = data[i], data[i] = false_lit;
+            S.watches[index(~data[1])].push(this);
+            return true; } }
+
+    // Clause is unit under assignment:
+    keep_watch = true;
+    return S.enqueue(data[0], this);
+}
+
+
+// Can assume 'out_reason' to be empty.
+// Calculate reason for 'p'. If 'p == lit_Undef', calculate reason for conflict.
+//
+void Clause::calcReason(Solver& S, Lit p, vec<Lit>& out_reason)
+{
+    assert(p == lit_Undef || p == data[0]);
+    for (int i = ((p == lit_Undef) ? 0 : 1); i < size(); i++)
+        assert(S.value(data[i]) == l_False),
+        out_reason.push(~data[i]);
+    if (learnt()) S.claBumpActivity(this);
+}
+
+
+//=================================================================================================
+// AtMost constraint -- An example of extending MiniSat:
+
+
+// Pre-condition: All variables must be distinct and unbound. (To lift this pre-condition,
+// any fact immediately derivable from the new constraint should be enqueued by 'enqueue()'.
+// If the constraint is already satisfied under the current top-level assignment, it should
+// not be constructed at all.)
+//
+bool AtMost_new(Solver& S, const vec<Lit>& ps, int n, AtMost*& out)
+{
+    assert(S.decisionLevel() == 0);
+
+    void* mem    = (void*)xmalloc<char>(sizeof(AtMost) + sizeof(Lit) * ps.size());
+    out          = new (mem) AtMost;
+    out->size    = ps.size();
+    out->n       = n;
+    out->counter = 0;
+    for (int i = 0; i < ps.size(); i++) out->lits[i] = ps[i];
+    for (int i = 0; i < ps.size(); i++) S.watches[index(ps[i])].push(out);
+
+    return true;
+}
+
+
+void AtMost::remove(Solver& S, bool just_dealloc) {
+    if (!just_dealloc)
+        for (int i = 0; i < size; i++)
+            removeWatch(S.watches[index(lits[i])], this);
+    xfree(this);
+}
+
+
+bool AtMost::simplify(Solver& S) {
+    return false; }
+
+
+bool AtMost::propagate(Solver& S, Lit p, bool& keep_watch)
+{
+    keep_watch = true;
+    if (counter == n) return false;
+
+    counter++;
+    S.undos[var(p)].push(this);
+
+    // If no more can be true, enqueue the negation of the rest:
+    if (counter == n)
+        for (int i = 0; i < size; i++)
+            if (!S.enqueue(~lits[i], this))
+                return false;
+    return true;
+}
+
+
+void AtMost::undo(Solver& S, Lit p) {
+    counter--; }
+
+
+void AtMost::calcReason(Solver& S, Lit p, vec<Lit>& out_reason)
+{
+    int     c = (p == lit_Undef) ? -1 : 0;
+    for (int i = 0; i < size; i++){
+        if (S.value(lits[i]) == l_True){
+            out_reason.push(lits[i]);
+            if (++c == n) return;
+        }
+    }
+}

Constraints.h

@@ -0,0 +1,95 @@
+/**************************************************************************************************
+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 Constraints_h
+#define Constraints_h
+
+#include "SolverTypes.h"
+
+
+//=================================================================================================
+// Constraint abstraction:
+
+
+class Solver;
+
+struct Constr {
+    virtual void remove    (Solver& S, bool just_dealloc = false) = 0;
+    virtual bool propagate (Solver& S, Lit p, bool& keep_watch) = 0;    // ('keep_watch' is set to FALSE beftore call to this method)
+    virtual bool simplify  (Solver& S) { return false; };
+    virtual void undo      (Solver& S, Lit p) { };
+    virtual void calcReason(Solver& S, Lit p, vec<Lit>& out_reason) = 0;
+
+    virtual ~Constr(void) { };  // (not used, just to keep the compiler happy)
+};
+
+
+//=================================================================================================
+// Clauses:
+
+
+class Clause : public Constr {
+    unsigned    size_learnt;
+    Lit         data[0];
+
+public:
+    int  size        (void)      const { return size_learnt >> 1; }
+    bool learnt      (void)      const { return size_learnt & 1; }
+    Lit  operator [] (int index) const { return data[index]; }
+
+    // Constructor -- creates a new clause and add it to watcher lists. 
+    friend bool Clause_new(Solver& S, const vec<Lit>& ps, bool learnt, Clause*& out_clause);
+
+    // Learnt clauses only:
+    bool    locked  (const Solver& S) const;
+    float&  activity(void) const { return *((float*)&data[size()]); }
+
+    // Constraint interface:
+    void remove    (Solver& S, bool just_dealloc = false);
+    bool propagate (Solver& S, Lit p, bool& keep_watch);
+    bool simplify  (Solver& S);
+    void calcReason(Solver& S, Lit p, vec<Lit>& out_reason);
+};
+
+
+//=================================================================================================
+// AtMost:
+
+
+class AtMost : public Constr {
+    int     n;
+    int     counter;
+    int     size;
+    Lit     lits[0];
+
+public:
+    // Constructor -- creates a new AtMost-constraint and add it to watcher lists.
+    friend bool AtMost_new(Solver& S, const vec<Lit>& ps, int n, AtMost*& out);
+
+    // Constraint interface:
+    void remove    (Solver& S, bool just_dealloc = false);
+    bool propagate (Solver& S, Lit p, bool& keep_watch);
+    bool simplify  (Solver& S);
+    void undo      (Solver& S, Lit p);
+    void calcReason(Solver& S, Lit p, vec<Lit>& out_reason);
+};
+
+
+//=================================================================================================
+#endif

Global.h

@@ -0,0 +1,236 @@
+/**************************************************************************************************
+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;
+#define I64_fmt "I64d"
+#else
+typedef long long   int64;
+#define I64_fmt "lld"
+#endif
+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:
+
+
+#ifdef _MSC_VER
+#include <ctime>
+static inline double cpuTime(void) {
+    return (double)clock() / CLOCKS_PER_SEC; }
+#else
+#include <sys/time.h>
+#include <sys/resource.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; }
+#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);
+
+    // 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,96 @@
+/**************************************************************************************************
+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__
+#define __HEAP__
+
+static inline int left (int i)  { return i * 2; }
+static inline int right(int i)  { return i * 2 + 1; }
+static inline int parent(int i) { return i / 2; }
+
+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     (void)     { return heap.size() == 1; }
+
+    void insert(int n) {
+        assert(ok(n));
+        indices[n] = heap.size();
+        heap.push(n);
+        percolateUp(indices[n]);
+    }
+
+    int  getmin(void) {
+        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(void) { 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,168 @@
+/**************************************************************************************************
+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>
+
+//=================================================================================================
+// Helpers:
+
+
+// Reads an input stream to end-of-file and returns the result as a 'char*' terminated by '\0'
+// (dynamic allocation in case 'in' is standard input).
+//
+char* readFile(gzFile in)
+{
+    char*   data = xmalloc<char>(65536);
+    int     cap  = 65536;
+    int     size = 0;
+
+    while (!gzeof(in)){
+        if (size == cap){
+            cap *= 2;
+            data = xrealloc(data, cap); }
+        size += gzread(in, &data[size], 65536);
+    }
+    data = xrealloc(data, size+1);
+    data[size] = '\0';
+
+    return data;
+}
+
+
+//=================================================================================================
+// DIMACS Parser:
+
+
+static void skipWhitespace(char*& in) {
+    while ((*in >= 9 && *in <= 13) || *in == 32)
+        in++; }
+
+static void skipLine(char*& in) {
+    for (;;){
+        if (*in == 0) return;
+        if (*in == '\n') { in++; return; }
+        in++; } }
+
+static int parseInt(char*& 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(1);
+    while (*in >= '0' && *in <= '9')
+        val = val*10 + (*in - '0'),
+        in++;
+    return neg ? -val : val; }
+
+static void readClause(char*& 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) );
+    }
+}
+
+static bool parse_DIMACS_main(char* in, Solver& S) {
+    vec<Lit>    lits;
+    for (;;){
+        skipWhitespace(in);
+        if (*in == 0)
+            break;
+        else if (*in == 'c' || *in == 'p')
+            skipLine(in);
+        else{
+            readClause(in, S, lits);
+            S.addClause(lits);
+            if (!S.okay())
+                return false;
+        }
+    }
+    S.simplifyDB();
+    return S.okay();
+}
+
+
+// Inserts problem into solver. Returns FALSE upon immediate conflict.
+//
+bool parse_DIMACS(gzFile in, Solver& S) {
+    char* text = readFile(in);
+    bool ret = parse_DIMACS_main(text, S);
+    free(text);
+    return ret; }
+
+
+//=================================================================================================
+
+
+void printStats(SolverStats& stats, double cpu_time)
+{
+    printf("restarts              : %"I64_fmt"\n", stats.starts);
+    printf("conflicts             : %-12"I64_fmt"   (%.0f /sec)\n", stats.conflicts   , stats.conflicts   /cpu_time);
+    printf("decisions             : %-12"I64_fmt"   (%.0f /sec)\n", stats.decisions   , stats.decisions   /cpu_time);
+    printf("propagations          : %-12"I64_fmt"   (%.0f /sec)\n", stats.propagations, stats.propagations/cpu_time);
+    printf("inspects              : %-12"I64_fmt"   (%.0f /sec)\n", stats.inspects    , stats.inspects    /cpu_time);
+    printf("CPU time              : %g s\n", cpu_time);
+}
+
+Solver* solver;
+static void SIGINT_handler(int signum) {
+    printf("\n"); printf("*** INTERRUPTED ***\n");
+    printStats(solver->stats, cpuTime());
+    printf("\n"); printf("*** INTERRUPTED ***\n");
+    exit(0); }
+
+
+//=================================================================================================
+
+
+int main(int argc, char** argv)
+{
+    Solver      S;
+    bool        st;
+
+    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);
+    st = parse_DIMACS(in, S);
+    gzclose(in);
+
+    if (!st)
+        printf("Trivial problem\nUNSATISFIABLE\n"),
+        exit(20);
+
+    S.verbosity = 1;
+    solver = &S;
+    signal(SIGINT,SIGINT_handler);
+    st = S.solve();
+    printStats(S.stats, cpuTime());
+    printf("\n");
+    printf(st ? "SATISFIABLE\n" : "UNSATISFIABLE\n");
+
+    return 0;
+}

Makefile

@@ -0,0 +1,85 @@
+##
+##  Makefile for Standard, Profile, Debug, and Release version of MiniSat
+##
+
+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
+COPTIMIZE = -O3 -fomit-frame-pointer
+
+
+.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

Queue.h

@@ -0,0 +1,45 @@
+/**************************************************************************************************
+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 Queue_h
+#define Queue_h
+
+
+//=================================================================================================
+
+
+template <class T>
+class Queue {
+    vec<T>  elems;
+    int     first;
+
+public:
+    Queue(void) : first(0) { }
+
+    void insert(T x)   { elems.push(x); }
+    T    dequeue(void) { return elems[first++]; }
+    void clear(void)   { elems.clear(); first = 0; }
+    int  size(void)    { return elems.size() - first; }
+
+    bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; }
+};
+
+
+//=================================================================================================
+#endif

README

@@ -0,0 +1,10 @@
+MiniSat v1.12b
+========================================
+
+This is the last version where arbitrary boolean constraints are
+supported. Later versions of MiniSat only supports clauses. However,
+don't be discouraged; the improvements made in v1.13 and v1.14 are
+quite easily back-ported to this version, so if you really need the
+functionality provided by this release, go ahead and use it (and send
+us the upgrades if you make them!)
+

README~

@@ -0,0 +1,10 @@
+MiniSat v1.12b
+========================================
+
+This is the last version where arbitrary boolean constraints are
+supported.  Later versions of MiniSat only supports clauses. However,
+don't be discouraged; the improvements made in v1.13 and v1.14 are
+quite easily back-ported to this version, so if you really need
+the functionality provided by this release, go ahead and use it
+(and send us the upgrades if you make them!)
+

Solver.C

@@ -0,0 +1,496 @@
+/**************************************************************************************************
+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>
+
+
+//=================================================================================================
+// Debug:
+
+
+// For derivation output (verbosity level 2)
+#define L_IND    "%-*d"
+#define L_ind    decisionLevel()*3+3,decisionLevel()
+#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); }
+
+
+//=================================================================================================
+// 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(void)
+{
+    int     index;
+    index = nVars();
+    watches .push();          // (list for positive literal)
+    watches .push();          // (list for negative literal)
+    undos   .push();
+    reason  .push(NULL);
+    assigns .push(toInt(l_Undef));
+    level   .push(-1);
+    activity.push(0);
+    order   .newVar();
+    return index;
+}
+
+
+// Returns FALSE if immediate conflict.
+bool Solver::assume(Lit p) {
+    assert(propQ.size() == 0);
+    if (verbosity >= 2) printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(p));
+    trail_lim.push(trail.size());
+    return enqueue(p); }
+
+
+// Revert one variable binding on the trail.
+//
+inline void Solver::undoOne(void)
+{
+    if (verbosity >= 2){ Lit p = trail.last(); printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(p)); }
+    Lit     p  = trail.last(); trail.pop();
+    Var     x  = var(p);
+    assigns[x] = toInt(l_Undef);
+    reason [x] = NULL;
+    order.undo(x);
+    while (undos[x].size() > 0)
+        undos[x].last()->undo(*this, p),
+        undos[x].pop();
+}
+
+
+// Reverts to the state before last 'assume()'.
+//
+void Solver::cancel(void)
+{
+    assert(propQ.size() == 0);
+    if (verbosity >= 2){ if (trail.size() != trail_lim.last()){ Lit p = trail[trail_lim.last()]; printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(p)); } }
+    for (int c = trail.size() - trail_lim.last(); c != 0; c--)
+        undoOne();
+    trail_lim.pop();
+}
+
+
+// Revert to the state at given level.
+//
+void Solver::cancelUntil(int level) {
+    while (decisionLevel() > level) cancel(); }
+
+
+// Record a clause and drive backtracking. 'clause[0]' must contain the asserting literal.
+//
+void Solver::record(const vec<Lit>& clause)
+{
+    assert(clause.size() != 0);
+    Clause* c;
+    check(Clause_new(*this, clause, true, c));
+    check(ok);
+    check(enqueue(clause[0], c));
+    if (c != NULL) learnts.push(c);
+}
+
+
+//=================================================================================================
+// Major methods:
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyze : (confl : Constr*) (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(Constr* confl, vec<Lit>& out_learnt, int& out_btlevel)
+{
+    vec<char>&  seen = analyze_seen;
+    int         pathC    = 0;
+    Lit         p = lit_Undef;
+    vec<Lit>    p_reason;
+    seen.growTo(nVars(), 0);
+
+    // Generate conflict clause:
+    //
+    out_learnt.push();      // (leave room for the asserting literal)
+    out_btlevel = 0;
+    do{
+        assert(confl != NULL);          // (otherwise should be UIP)
+
+        p_reason.clear();
+        confl->calcReason(*this, p, p_reason);
+
+        for (int j = 0; j < p_reason.size(); j++){
+            Lit q = p_reason[j];
+            if (!seen[var(q)] && level[var(q)] > 0){
+                seen[var(q)] = 1;
+                varBumpActivity(q);
+                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:
+        do{
+            p = trail.last();
+            confl = reason[var(p)];
+            undoOne();
+        }while (!seen[var(p)]);
+        pathC--;
+    seen[var(p)] = 0;
+    }while (pathC > 0);
+    out_learnt[0] = ~p;
+
+    for (int j = 0; j < out_learnt.size(); j++) seen[var(out_learnt[j])] = 0;    // ('seen[]' is now cleared)
+
+    if (verbosity >= 2){
+        printf(L_IND"Learnt {", L_ind);
+        for (int i = 0; i < out_learnt.size(); i++) printf(" "L_LIT, L_lit(out_learnt[i]));
+        printf(" } at level %d\n", out_btlevel); }
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  enqueue : (p : Lit) (from : Constr*)  ->  [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, Constr* from)
+{
+   if (value(p) != l_Undef){
+        if (value(p) == l_False){
+            // Conflicting enqueued assignment
+            if (decisionLevel() == 0)
+                ok = false;
+            return false;
+        }else{
+            // Existing consistent assignment -- don't enqueue
+            return true;
+        }
+    }else{
+        // New fact -- store it.
+        if (verbosity >= 2) printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(p));
+        assigns[var(p)] = toInt(lbool(!sign(p)));
+        level  [var(p)] = decisionLevel();
+        reason [var(p)] = from;
+        trail.push(p);
+        propQ.insert(p);
+        return true;
+    }
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  propagate : [void]  ->  [Constr*]
+|  
+|  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.
+|________________________________________________________________________________________________@*/
+Constr* Solver::propagate(void)
+{
+    Constr* confl = NULL;
+    while (propQ.size() > 0){
+        stats.propagations++;
+        Lit           p  = propQ.dequeue();        // 'p' is enqueued fact to propagate.
+        vec<Constr*>& ws = watches[index(p)];
+        bool          keep_watch;
+        Constr        **i, **j, **end = (Constr**)ws + ws.size();
+        for (i = j = (Constr**)ws; confl == NULL && i < end; i++){
+            stats.inspects++;
+            keep_watch = false;
+            if (!(*i)->propagate(*this, p, keep_watch))
+                confl = *i,
+                propQ.clear();
+            if (keep_watch)
+                *j++ = *i;
+        }
+
+        // Copy the remaining watches:
+        while (i < end)
+            *j++ = *i++;
+
+        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 a some assignment.
+|________________________________________________________________________________________________@*/
+struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->activity() < y->activity(); } };
+void Solver::reduceDB(void)
+{
+    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]->locked(*this))
+            learnts[i]->remove(*this);
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < learnts.size(); i++){
+        if (!learnts[i]->locked(*this) && learnts[i]->activity() < extra_lim)
+            learnts[i]->remove(*this);
+        else
+            learnts[j++] = learnts[i];
+    }
+    learnts.shrink(i - j);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  simplifyDB : [void]  ->  [bool]
+|  
+|  Description:
+|    Simplify all constraints according to the current top-level assigment (redundant constraints
+|    may be removed altogether).
+|________________________________________________________________________________________________@*/
+void Solver::simplifyDB(void)
+{
+    if (!ok) return;    // GUARD (public method)
+    assert(decisionLevel() == 0);
+
+    if (propagate() != NULL){
+        ok = false;
+        return; }
+    if (nAssigns() == last_simplify)
+        return;
+
+    last_simplify = nAssigns();
+
+    for (int type = 0; type < 2; type++){
+        vec<Constr*>& cs = type ? (vec<Constr*>&)learnts : constrs;
+
+        int     j = 0;
+        for (int i = 0; i < cs.size(); i++){
+            if (cs[i]->simplify(*this))
+                cs[i]->remove(*this);
+            else
+                cs[j++] = cs[i];
+        }
+        cs.shrink(cs.size()-j);
+    }
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  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 (;;){
+        Constr* confl = propagate();
+        if (confl != NULL){
+            // CONFLICT
+
+            if (verbosity >= 2) printf(L_IND"**CONFLICT**\n", L_ind);
+            stats.conflicts++; conflictC++;
+            vec<Lit>    learnt_clause;
+            int         backtrack_level;
+            if (decisionLevel() == root_level)
+                return l_False;
+            analyze(confl, learnt_clause, backtrack_level);
+            cancelUntil(max(backtrack_level, root_level));
+            record(learnt_clause);
+            varDecayActivity(); claDecayActivity();
+
+        }else{
+            // NO CONFLICT
+
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+                // Reached bound on number of conflicts:
+                progress_estimate = progressEstimate();
+                propQ.clear();
+                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(void)
+{
+    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(void)
+{
+    for (int i = 0; i < nVars(); i++)
+        activity[i] *= 1e-100;
+    var_inc *= 1e-100;
+}
+
+
+// Divide all constraint activities by 1e100.
+//
+void Solver::claRescaleActivity(void)
+{
+    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(0.95, 0.999, 0.02);
+    double  nof_conflicts = 100;
+    double  nof_learnts   = nConstrs() / 3;
+    lbool   status        = l_Undef;
+
+    for (int i = 0; i < assumps.size(); i++)
+        if (!assume(assumps[i]) || propagate() != NULL){
+            propQ.clear();
+            cancelUntil(0);
+            return false; }
+    root_level = decisionLevel();
+
+    if (verbosity >= 1){
+        printf("==================================[MINISAT]===================================\n");
+        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
+        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
+        printf("==============================================================================\n");
+    }
+
+    while (status == l_Undef){
+        if (verbosity >= 1){
+            printf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nConstrs(), (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)
+        printf("==============================================================================\n");
+
+    cancelUntil(0);
+    return status == l_True;
+}

Solver.h

@@ -0,0 +1,164 @@
+/**************************************************************************************************
+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 "Constraints.h"
+#include "Queue.h"
+#include "VarOrder.h"
+
+
+//=================================================================================================
+// Solver -- the main class:
+
+
+struct SolverStats {
+    int64   starts, decisions, propagations, inspects, conflicts;
+    int64   clauses, clauses_literals, learnts, learnts_literals;
+    SolverStats(void) : starts(0), decisions(0), propagations(0), inspects(0), conflicts(0)
+        , clauses(0), clauses_literals(0), learnts(0), learnts_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:
+    bool                ok;             // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
+    vec<Constr*>        constrs;        // List of problem constraints.
+    vec<Clause*>        learnts;        // List of learnt clauses.
+    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<Constr*> >  watches;        // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+    vec<vec<Constr*> >  undos;          // 'undos[var]' is a list of constraints that will be called when 'var' becomes unbound.
+    Queue<Lit>          propQ;          // Propagation queue.
+
+    vec<char>           assigns;        // The current assignments (lbool:s stored as char:s).
+    vec<Lit>            trail;          // List of assignments made. 
+    vec<int>            trail_lim;      // Separator indices for different decision levels in 'trail'.
+    vec<Constr*>        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                 last_simplify;  // Number of top-level assignments at last 'simplifyDB()'.
+
+    // Temporaries (to reduce allocation overhead):
+    //
+    vec<char>           analyze_seen;
+
+    // Main internal methods:
+    //
+    bool        assume       (Lit p);
+    void        undoOne      (void);
+    void        cancel       (void);
+    void        cancelUntil  (int level);
+    void        record       (const vec<Lit>& clause);
+
+    void        analyze      (Constr* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
+    bool        enqueue      (Lit fact, Constr* from = NULL);
+    Constr*     propagate    (void);
+    void        reduceDB     (void);
+    Lit         pickBranchLit(const SearchParams& params);
+    lbool       search       (int nof_conflicts, int nof_learnts, const SearchParams& params);
+    double      progressEstimate(void);
+
+    // 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(void) { if (var_decay >= 0) var_inc *= var_decay; }
+    void    varRescaleActivity(void);
+
+    void    claBumpActivity(Clause* c) { if ( (c->activity() += cla_inc) > 1e20 ) claRescaleActivity(); }
+    void    claDecayActivity(void) { cla_inc *= cla_decay; }
+    void    claRescaleActivity(void);
+
+    int     decisionLevel(void) { return trail_lim.size(); }
+
+public:
+    Solver(void) : ok               (true)
+                 , cla_inc          (1)
+                 , cla_decay        (1)
+                 , var_inc          (1)
+                 , var_decay        (1)
+                 , order            (assigns, activity)
+                 , last_simplify    (-1)
+                 , progress_estimate(0)
+                 , verbosity(0)
+                 { }
+   ~Solver(void) {
+        for (int i = 0; i < learnts.size(); i++) learnts[i]->remove(*this, true);
+        for (int i = 0; i < constrs.size(); i++) constrs[i]->remove(*this, true); }
+
+    // Helpers: (semi-internal)
+    //
+    lbool   value(Var x) { return toLbool(assigns[x]); }
+    lbool   value(Lit p) { return sign(p) ? ~toLbool(assigns[var(p)]) : toLbool(assigns[var(p)]); }
+
+    int     nAssigns(void) { return trail.size(); }
+    int     nConstrs(void) { return constrs.size(); }
+    int     nLearnts(void) { return learnts.size(); }
+
+    // Statistics: (read-only member variable)
+    //
+    SolverStats stats;
+
+    // Problem specification:
+    //
+    Var     newVar (void);
+    int     nVars  (void)  { return assigns.size(); }
+    void    addUnit(Lit p) { if (ok) enqueue(p); }
+
+    // -- constraints:
+    friend class Clause;
+    friend class AtMost;
+    friend bool Clause_new(Solver& S, const vec<Lit>& ps, bool learnt, Clause*& out_clause);
+    friend bool AtMost_new(Solver& S, const vec<Lit>& ps, int  max   , AtMost*& out_constr);
+
+    void    addClause(const vec<Lit>& ps)        { if (ok){ Clause* c; ok = Clause_new(*this, ps, false, c); if (c != NULL) constrs.push(c); } }
+    void    addAtMost(const vec<Lit>& ps, int n) { if (ok){ AtMost* c; ok = AtMost_new(*this, ps, n    , c); if (c != NULL) constrs.push(c); } }
+
+    // Solving:
+    //
+    bool    okay(void) { return ok; }
+    void    simplifyDB(void);
+    bool    solve(const vec<Lit>& assumps);
+    bool    solve(void) { vec<Lit> tmp; return solve(tmp); }
+
+    double      progress_estimate;  // Set by 'search()'.
+    vec<lbool>  model;              // If problem is solved, this vector contains the model (if any).
+    int         verbosity;          // Verbosity level. 0=silent, 1=some progress report, 2=everything
+};
+
+
+//=================================================================================================
+#endif

SolverTypes.h

@@ -0,0 +1,61 @@
+/**************************************************************************************************
+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:
+
+
+// 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(void)   /* unspecifed value allowed for efficiency */      { }
+    explicit Lit(Var var, bool sign = false) : x((var+var) + sign) { }
+    friend Lit operator ~ (Lit p) { Lit q; q.x = p.x ^ 1; return q; }
+
+    friend bool sign (Lit p) { return p.x & 1; }
+    friend int  var  (Lit p) { return p.x >> 1; }
+    friend int  index(Lit p) { return p.x; }        // A "toInt" method that guarantees small, positive integers suitable for array indexing.
+    friend Lit  toLit(int i) { Lit p; p.x = i; return p; }
+
+    friend bool operator == (Lit p, Lit q) { return index(p) == index(q); }
+    friend 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 );  // }
+
+
+//=================================================================================================
+#endif

Sort.h

@@ -0,0 +1,134 @@
+/**************************************************************************************************
+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
+
+//#include <cstdlib>
+
+
+//=================================================================================================
+
+
+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

VarOrder.h

@@ -0,0 +1,94 @@
+/**************************************************************************************************
+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){
+        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

compile.sh

@@ -0,0 +1,3 @@
+# In case the Makefile doesn't work for you, try this script.
+
+g++ -ggdb -D DEBUG -O3 Main.C Solver.C Constraints.C VarOrder.C -o minisat