Added libs/minisat (copy of minisat git master)

28 files changed, 5025 insertions, 28 deletions

diff --git a/Makefile b/Makefile
index abb473ba9..0acc0d0e4 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,6 @@ CONFIG := clang-debug
 # features (the more the better)
 ENABLE_TCL := 1
 ENABLE_QT4 := 1
-ENABLE_MINISAT := 1
 ENABLE_ABC := 1
 ENABLE_VERIFIC := 0
 
@@ -95,11 +94,11 @@ OBJS += libs/sha1/sha1.o
 OBJS += libs/subcircuit/subcircuit.o
 OBJS += libs/ezsat/ezsat.o
 
-ifeq ($(ENABLE_MINISAT),1)
-CXXFLAGS += -DYOSYS_ENABLE_MINISAT
 OBJS += libs/ezsat/ezminisat.o
-LDLIBS += -lminisat
-endif
+OBJS += libs/minisat/Options.o
+OBJS += libs/minisat/SimpSolver.o
+OBJS += libs/minisat/Solver.o
+OBJS += libs/minisat/System.o
 
 include frontends/*/Makefile.inc
 include passes/*/Makefile.inc
diff --git a/README b/README
index 45febc2f9..5a48a207c 100644
--- a/README
+++ b/README
@@ -280,21 +280,6 @@ Verilog Attributes and non-standard features
   must be put in parentheses. Examples: WIDTH'd42, (4+2)'b101010
 
 
-Workarounds for known build problems
-====================================
-
-You might get an error message like this one during build when building with
-a recent version of gcc:
-
-	/usr/include/minisat/utils/Options.h:285:29: error:
-	unable to find string literal operator ‘operator"" PRIi64’
-
-This is a bug in the minisat header. It can be fixed by adding spaces before
-and after each occurrence of PRIi64 in the header file:
-
-	 sudo sed -i -e 's/PRIi64/ & /' /usr/include/minisat/utils/Options.h
-
-
 Roadmap / Large-scale TODOs
 ===========================
 
diff --git a/kernel/satgen.h b/kernel/satgen.h
index bf72a31cb..81d029295 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -24,13 +24,8 @@
 #include "kernel/sigtools.h"
 #include "kernel/celltypes.h"
 
-#ifdef YOSYS_ENABLE_MINISAT
-#  include "libs/ezsat/ezminisat.h"
+#include "libs/ezsat/ezminisat.h"
 typedef ezMiniSAT ezDefaultSAT;
-#else
-#  include "libs/ezsat/ezsat.h"
-typedef ezSAT ezDefaultSAT;
-#endif
 
 struct SatGen
 {
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 4677f68bd..caee73f88 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -28,8 +28,13 @@
 #include <csignal>
 #include <cinttypes>
 
-#include <minisat/core/Solver.h>
-#include <minisat/simp/SimpSolver.h>
+#ifdef _YOSYS_
+#  include "libs/minisat/Solver.h"
+#  include "libs/minisat/SimpSolver.h"
+#else
+#  include <minisat/core/Solver.h>
+#  include <minisat/simp/SimpSolver.h>
+#endif
 
 ezMiniSAT::ezMiniSAT() : minisatSolver(NULL)
 {
diff --git a/libs/minisat/Alg.h b/libs/minisat/Alg.h
new file mode 100644
index 000000000..7f7eac61f
--- /dev/null
+++ b/libs/minisat/Alg.h
@@ -0,0 +1,84 @@
+/*******************************************************************************************[Alg.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Alg_h
+#define Minisat_Alg_h
+
+#include "libs/minisat/Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Useful functions on vector-like types:
+
+//=================================================================================================
+// Removing and searching for elements:
+//
+
+template<class V, class T>
+static inline void remove(V& ts, const T& t)
+{
+    int j = 0;
+    for (; j < (int)ts.size() && ts[j] != t; j++);
+    assert(j < (int)ts.size());
+    for (; j < (int)ts.size()-1; j++) ts[j] = ts[j+1];
+    ts.pop();
+}
+
+
+template<class V, class T>
+static inline bool find(V& ts, const T& t)
+{
+    int j = 0;
+    for (; j < (int)ts.size() && ts[j] != t; j++);
+    return j < (int)ts.size();
+}
+
+
+//=================================================================================================
+// Copying vectors with support for nested vector types:
+//
+
+// Base case:
+template<class T>
+static inline void copy(const T& from, T& to)
+{
+    to = from;
+}
+
+// Recursive case:
+template<class T>
+static inline void copy(const vec<T>& from, vec<T>& to, bool append = false)
+{
+    if (!append)
+        to.clear();
+    for (int i = 0; i < from.size(); i++){
+        to.push();
+        copy(from[i], to.last());
+    }
+}
+
+template<class T>
+static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Alloc.h b/libs/minisat/Alloc.h
new file mode 100644
index 000000000..0de4f07ca
--- /dev/null
+++ b/libs/minisat/Alloc.h
@@ -0,0 +1,131 @@
+/*****************************************************************************************[Alloc.h]
+Copyright (c) 2008-2010, 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 Minisat_Alloc_h
+#define Minisat_Alloc_h
+
+#include "libs/minisat/XAlloc.h"
+#include "libs/minisat/Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple Region-based memory allocator:
+
+template<class T>
+class RegionAllocator
+{
+    T*        memory;
+    uint32_t  sz;
+    uint32_t  cap;
+    uint32_t  wasted_;
+
+    void capacity(uint32_t min_cap);
+
+ public:
+    // TODO: make this a class for better type-checking?
+    typedef uint32_t Ref;
+    enum { Ref_Undef = UINT32_MAX };
+    enum { Unit_Size = sizeof(T) };
+
+    explicit RegionAllocator(uint32_t start_cap = 1024*1024) : memory(NULL), sz(0), cap(0), wasted_(0){ capacity(start_cap); }
+    ~RegionAllocator()
+    {
+        if (memory != NULL)
+            ::free(memory);
+    }
+
+
+    uint32_t size      () const      { return sz; }
+    uint32_t wasted    () const      { return wasted_; }
+
+    Ref      alloc     (int size); 
+    void     free      (int size)    { wasted_ += size; }
+
+    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
+    T&       operator[](Ref r)       { assert(r < sz); return memory[r]; }
+    const T& operator[](Ref r) const { assert(r < sz); return memory[r]; }
+
+    T*       lea       (Ref r)       { assert(r < sz); return &memory[r]; }
+    const T* lea       (Ref r) const { assert(r < sz); return &memory[r]; }
+    Ref      ael       (const T* t)  { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]);
+        return  (Ref)(t - &memory[0]); }
+
+    void     moveTo(RegionAllocator& to) {
+        if (to.memory != NULL) ::free(to.memory);
+        to.memory = memory;
+        to.sz = sz;
+        to.cap = cap;
+        to.wasted_ = wasted_;
+
+        memory = NULL;
+        sz = cap = wasted_ = 0;
+    }
+
+
+};
+
+template<class T>
+void RegionAllocator<T>::capacity(uint32_t min_cap)
+{
+    if (cap >= min_cap) return;
+
+    uint32_t prev_cap = cap;
+    while (cap < min_cap){
+        // NOTE: Multiply by a factor (13/8) without causing overflow, then add 2 and make the
+        // result even by clearing the least significant bit. The resulting sequence of capacities
+        // is carefully chosen to hit a maximum capacity that is close to the '2^32-1' limit when
+        // using 'uint32_t' as indices so that as much as possible of this space can be used.
+        uint32_t delta = ((cap >> 1) + (cap >> 3) + 2) & ~1;
+        cap += delta;
+
+        if (cap <= prev_cap)
+            throw OutOfMemoryException();
+    }
+    // printf(" .. (%p) cap = %u\n", this, cap);
+
+    assert(cap > 0);
+    memory = (T*)xrealloc(memory, sizeof(T)*cap);
+}
+
+
+template<class T>
+typename RegionAllocator<T>::Ref
+RegionAllocator<T>::alloc(int size)
+{ 
+    // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout);
+    assert(size > 0);
+    capacity(sz + size);
+
+    uint32_t prev_sz = sz;
+    sz += size;
+    
+    // Handle overflow:
+    if (sz < prev_sz)
+        throw OutOfMemoryException();
+
+    return prev_sz;
+}
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Dimacs.h b/libs/minisat/Dimacs.h
new file mode 100644
index 000000000..383e894be
--- /dev/null
+++ b/libs/minisat/Dimacs.h
@@ -0,0 +1,87 @@
+/****************************************************************************************[Dimacs.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Dimacs_h
+#define Minisat_Dimacs_h
+
+#include <stdio.h>
+
+#include "libs/minisat/ParseUtils.h"
+#include "libs/minisat/SolverTypes.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// DIMACS Parser:
+
+template<class B, class Solver>
+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) ? mkLit(var) : ~mkLit(var) );
+    }
+}
+
+template<class B, class Solver>
+static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) {
+    vec<Lit> lits;
+    int vars    = 0;
+    int clauses = 0;
+    int cnt     = 0;
+    for (;;){
+        skipWhitespace(in);
+        if (*in == EOF) break;
+        else if (*in == 'p'){
+            if (eagerMatch(in, "p cnf")){
+                vars    = parseInt(in);
+                clauses = parseInt(in);
+                // SATRACE'06 hack
+                // if (clauses > 4000000)
+                //     S.eliminate(true);
+            }else{
+                printf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
+            }
+        } else if (*in == 'c' || *in == 'p')
+            skipLine(in);
+        else{
+            cnt++;
+            readClause(in, S, lits);
+            S.addClause_(lits); }
+    }
+    if (strictp && cnt != clauses)
+        printf("PARSE ERROR! DIMACS header mismatch: wrong number of clauses\n");
+}
+
+// Inserts problem into solver.
+//
+template<class Solver>
+static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
+    StreamBuffer in(input_stream);
+    parse_DIMACS_main(in, S, strictp); }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Heap.h b/libs/minisat/Heap.h
new file mode 100644
index 000000000..a75124627
--- /dev/null
+++ b/libs/minisat/Heap.h
@@ -0,0 +1,168 @@
+/******************************************************************************************[Heap.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Heap_h
+#define Minisat_Heap_h
+
+#include "libs/minisat/Vec.h"
+#include "libs/minisat/IntMap.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// A heap implementation with support for decrease/increase key.
+
+
+template<class K, class Comp, class MkIndex = MkIndexDefault<K> >
+class Heap {
+    vec<K>                heap;     // Heap of Keys
+    IntMap<K,int,MkIndex> indices;  // Each Key's position (index) in the Heap
+    Comp                  lt;       // The heap is a minimum-heap with respect to this comparator
+
+    // Index "traversal" functions
+    static inline int left  (int i) { return i*2+1; }
+    static inline int right (int i) { return (i+1)*2; }
+    static inline int parent(int i) { return (i-1) >> 1; }
+
+
+    void percolateUp(int i)
+    {
+        K   x  = heap[i];
+        int p  = parent(i);
+        
+        while (i != 0 && lt(x, heap[p])){
+            heap[i]          = heap[p];
+            indices[heap[p]] = i;
+            i                = p;
+            p                = parent(p);
+        }
+        heap   [i] = x;
+        indices[x] = i;
+    }
+
+
+    void percolateDown(int i)
+    {
+        K x = heap[i];
+        while (left(i) < heap.size()){
+            int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
+            if (!lt(heap[child], x)) break;
+            heap[i]          = heap[child];
+            indices[heap[i]] = i;
+            i                = child;
+        }
+        heap   [i] = x;
+        indices[x] = i;
+    }
+
+
+  public:
+    Heap(const Comp& c, MkIndex _index = MkIndex()) : indices(_index), lt(c) {}
+
+    int  size      ()          const { return heap.size(); }
+    bool empty     ()          const { return heap.size() == 0; }
+    bool inHeap    (K k)       const { return indices.has(k) && indices[k] >= 0; }
+    int  operator[](int index) const { assert(index < heap.size()); return heap[index]; }
+
+    void decrease  (K k) { assert(inHeap(k)); percolateUp  (indices[k]); }
+    void increase  (K k) { assert(inHeap(k)); percolateDown(indices[k]); }
+
+
+    // Safe variant of insert/decrease/increase:
+    void update(K k)
+    {
+        if (!inHeap(k))
+            insert(k);
+        else {
+            percolateUp(indices[k]);
+            percolateDown(indices[k]); }
+    }
+
+
+    void insert(K k)
+    {
+        indices.reserve(k, -1);
+        assert(!inHeap(k));
+
+        indices[k] = heap.size();
+        heap.push(k);
+        percolateUp(indices[k]);
+    }
+
+
+    void remove(K k)
+    {
+        assert(inHeap(k));
+
+        int k_pos  = indices[k];
+        indices[k] = -1;
+
+        if (k_pos < heap.size()-1){
+            heap[k_pos]          = heap.last();
+            indices[heap[k_pos]] = k_pos;
+            heap.pop();
+            percolateDown(k_pos);
+        }else
+            heap.pop();
+    }
+
+
+    K removeMin()
+    {
+        K x              = heap[0];
+        heap[0]          = heap.last();
+        indices[heap[0]] = 0;
+        indices[x]       = -1;
+        heap.pop();
+        if (heap.size() > 1) percolateDown(0);
+        return x; 
+    }
+
+
+    // Rebuild the heap from scratch, using the elements in 'ns':
+    void build(const vec<K>& ns) {
+        for (int i = 0; i < heap.size(); i++)
+            indices[heap[i]] = -1;
+        heap.clear();
+
+        for (int i = 0; i < ns.size(); i++){
+            // TODO: this should probably call reserve instead of relying on it being reserved already.
+            assert(indices.has(ns[i]));
+            indices[ns[i]] = i;
+            heap.push(ns[i]); }
+
+        for (int i = heap.size() / 2 - 1; i >= 0; i--)
+            percolateDown(i);
+    }
+
+    void clear(bool dispose = false) 
+    { 
+        // TODO: shouldn't the 'indices' map also be dispose-cleared?
+        for (int i = 0; i < heap.size(); i++)
+            indices[heap[i]] = -1;
+        heap.clear(dispose); 
+    }
+};
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/IntMap.h b/libs/minisat/IntMap.h
new file mode 100644
index 000000000..61dd0f679
--- /dev/null
+++ b/libs/minisat/IntMap.h
@@ -0,0 +1,106 @@
+/****************************************************************************************[IntMap.h]
+Copyright (c) 2011, 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 Minisat_IntMap_h
+#define Minisat_IntMap_h
+
+#include "libs/minisat/Vec.h"
+
+namespace Minisat {
+
+    template<class T> struct MkIndexDefault {
+        typename vec<T>::Size operator()(T t) const { return (typename vec<T>::Size)t; }
+    };
+    
+    template<class K, class V, class MkIndex = MkIndexDefault<K> >
+    class IntMap {
+        vec<V>   map;
+        MkIndex  index;
+    public:
+        explicit IntMap(MkIndex _index = MkIndex()) : index(_index){}
+        
+        bool     has       (K k) const { return index(k) < map.size(); }
+
+        const V& operator[](K k) const { assert(has(k)); return map[index(k)]; }
+        V&       operator[](K k)       { assert(has(k)); return map[index(k)]; }
+
+        const V* begin  () const { return &map[0]; }
+        const V* end    () const { return &map[map.size()]; }
+        V*       begin  ()       { return &map[0]; }
+        V*       end    ()       { return &map[map.size()]; }
+
+        void     reserve(K key, V pad)       { map.growTo(index(key)+1, pad); }
+        void     reserve(K key)              { map.growTo(index(key)+1); }
+        void     insert (K key, V val, V pad){ reserve(key, pad); operator[](key) = val; }
+        void     insert (K key, V val)       { reserve(key); operator[](key) = val; }
+
+        void     clear  (bool dispose = false) { map.clear(dispose); }
+        void     moveTo (IntMap& to)           { map.moveTo(to.map); to.index = index; }
+        void     copyTo (IntMap& to) const     { map.copyTo(to.map); to.index = index; }
+    };
+
+
+    template<class K, class MkIndex = MkIndexDefault<K> >
+    class IntSet
+    {
+        IntMap<K, char, MkIndex> in_set;
+        vec<K>                   xs;
+        
+    public:
+        // Size operations:
+        int      size        (void)      const  { return xs.size(); }
+        void     clear       (bool free = false){
+            if (free)
+                in_set.clear(true); 
+            else
+                for (int i = 0; i < xs.size(); i++)
+                    in_set[xs[i]] = 0;
+            xs.clear(free);
+        }
+
+        // Allow inspecting the internal vector:
+        const vec<K>&
+                 toVec       ()          const  { return xs; }
+        
+        // Vector interface:
+        K        operator [] (int index) const  { return xs[index]; }
+        
+        
+        void     insert      (K k) { in_set.reserve(k, 0); if (!in_set[k]) { in_set[k] = 1; xs.push(k); } }
+        bool     has         (K k) { in_set.reserve(k, 0); return in_set[k]; }
+    };
+
+    #if 0
+    template<class K, class V, V nil, class MkIndex = MkIndexDefault<K> >
+    class IntMapNil {
+        vec<V> map;
+        V      nil;
+
+    public:
+        IntMap(){}
+        
+        void     reserve(K);
+        V&       find   (K);
+        const V& operator[](K k) const;
+
+    };
+    #endif
+
+//=================================================================================================
+} // namespace Minisat
+#endif
diff --git a/libs/minisat/IntTypes.h b/libs/minisat/IntTypes.h
new file mode 100644
index 000000000..c48816284
--- /dev/null
+++ b/libs/minisat/IntTypes.h
@@ -0,0 +1,42 @@
+/**************************************************************************************[IntTypes.h]
+Copyright (c) 2009-2010, 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 Minisat_IntTypes_h
+#define Minisat_IntTypes_h
+
+#ifdef __sun
+    // Not sure if there are newer versions that support C99 headers. The
+    // needed features are implemented in the headers below though:
+
+#   include <sys/int_types.h>
+#   include <sys/int_fmtio.h>
+#   include <sys/int_limits.h>
+
+#else
+
+#   include <stdint.h>
+#   include <inttypes.h>
+
+#endif
+
+#include <limits.h>
+
+//=================================================================================================
+
+#endif
diff --git a/libs/minisat/LICENSE b/libs/minisat/LICENSE
new file mode 100644
index 000000000..22816ff39
--- /dev/null
+++ b/libs/minisat/LICENSE
@@ -0,0 +1,21 @@
+MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+           Copyright (c) 2007-2010  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.
diff --git a/libs/minisat/Map.h b/libs/minisat/Map.h
new file mode 100644
index 000000000..93b6da31c
--- /dev/null
+++ b/libs/minisat/Map.h
@@ -0,0 +1,193 @@
+/*******************************************************************************************[Map.h]
+Copyright (c) 2006-2010, 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 Minisat_Map_h
+#define Minisat_Map_h
+
+#include "libs/minisat/IntTypes.h"
+#include "libs/minisat/Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Default hash/equals functions
+//
+
+template<class K> struct Hash  { uint32_t operator()(const K& k)               const { return hash(k);  } };
+template<class K> struct Equal { bool     operator()(const K& k1, const K& k2) const { return k1 == k2; } };
+
+template<class K> struct DeepHash  { uint32_t operator()(const K* k)               const { return hash(*k);  } };
+template<class K> struct DeepEqual { bool     operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
+
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
+
+//=================================================================================================
+// Some primes
+//
+
+static const int nprimes          = 25;
+static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 };
+
+//=================================================================================================
+// Hash table implementation of Maps
+//
+
+template<class K, class D, class H = Hash<K>, class E = Equal<K> >
+class Map {
+ public:
+    struct Pair { K key; D data; };
+
+ private:
+    H          hash;
+    E          equals;
+
+    vec<Pair>* table;
+    int        cap;
+    int        size;
+
+    // Don't allow copying (error prone):
+    Map<K,D,H,E>&  operator = (Map<K,D,H,E>& other);
+                   Map        (Map<K,D,H,E>& other);
+
+    bool    checkCap(int new_size) const { return new_size > cap; }
+
+    int32_t index  (const K& k) const { return hash(k) % cap; }
+    void   _insert (const K& k, const D& d) { 
+        vec<Pair>& ps = table[index(k)];
+        ps.push(); ps.last().key = k; ps.last().data = d; }
+
+    void    rehash () {
+        const vec<Pair>* old = table;
+
+        int old_cap = cap;
+        int newsize = primes[0];
+        for (int i = 1; newsize <= cap && i < nprimes; i++)
+           newsize = primes[i];
+
+        table = new vec<Pair>[newsize];
+        cap   = newsize;
+
+        for (int i = 0; i < old_cap; i++){
+            for (int j = 0; j < old[i].size(); j++){
+                _insert(old[i][j].key, old[i][j].data); }}
+
+        delete [] old;
+
+        // printf(" --- rehashing, old-cap=%d, new-cap=%d\n", cap, newsize);
+    }
+
+    
+ public:
+
+    Map () : table(NULL), cap(0), size(0) {}
+    Map (const H& h, const E& e) : hash(h), equals(e), table(NULL), cap(0), size(0){}
+    ~Map () { delete [] table; }
+
+    // PRECONDITION: the key must already exist in the map.
+    const D& operator [] (const K& k) const
+    {
+        assert(size != 0);
+        const D*         res = NULL;
+        const vec<Pair>& ps  = table[index(k)];
+        for (int i = 0; i < ps.size(); i++)
+            if (equals(ps[i].key, k))
+                res = &ps[i].data;
+        assert(res != NULL);
+        return *res;
+    }
+
+    // PRECONDITION: the key must already exist in the map.
+    D& operator [] (const K& k)
+    {
+        assert(size != 0);
+        D*         res = NULL;
+        vec<Pair>& ps  = table[index(k)];
+        for (int i = 0; i < ps.size(); i++)
+            if (equals(ps[i].key, k))
+                res = &ps[i].data;
+        assert(res != NULL);
+        return *res;
+    }
+
+    // PRECONDITION: the key must *NOT* exist in the map.
+    void insert (const K& k, const D& d) { if (checkCap(size+1)) rehash(); _insert(k, d); size++; }
+    bool peek   (const K& k, D& d) const {
+        if (size == 0) return false;
+        const vec<Pair>& ps = table[index(k)];
+        for (int i = 0; i < ps.size(); i++)
+            if (equals(ps[i].key, k)){
+                d = ps[i].data;
+                return true; } 
+        return false;
+    }
+
+    bool has   (const K& k) const {
+        if (size == 0) return false;
+        const vec<Pair>& ps = table[index(k)];
+        for (int i = 0; i < ps.size(); i++)
+            if (equals(ps[i].key, k))
+                return true;
+        return false;
+    }
+
+    // PRECONDITION: the key must exist in the map.
+    void remove(const K& k) {
+        assert(table != NULL);
+        vec<Pair>& ps = table[index(k)];
+        int j = 0;
+        for (; j < ps.size() && !equals(ps[j].key, k); j++);
+        assert(j < ps.size());
+        ps[j] = ps.last();
+        ps.pop();
+        size--;
+    }
+
+    void clear  () {
+        cap = size = 0;
+        delete [] table;
+        table = NULL;
+    }
+
+    int  elems() const { return size; }
+    int  bucket_count() const { return cap; }
+
+    // NOTE: the hash and equality objects are not moved by this method:
+    void moveTo(Map& other){
+        delete [] other.table;
+
+        other.table = table;
+        other.cap   = cap;
+        other.size  = size;
+
+        table = NULL;
+        size = cap = 0;
+    }
+
+    // NOTE: given a bit more time, I could make a more C++-style iterator out of this:
+    const vec<Pair>& bucket(int i) const { return table[i]; }
+};
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Options.cc b/libs/minisat/Options.cc
new file mode 100644
index 000000000..b1b3e31ba
--- /dev/null
+++ b/libs/minisat/Options.cc
@@ -0,0 +1,94 @@
+#define __STDC_FORMAT_MACROS
+#define __STDC_LIMIT_MACROS
+/**************************************************************************************[Options.cc]
+Copyright (c) 2008-2010, 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 "libs/minisat/Sort.h"
+#include "libs/minisat/Options.h"
+#include "libs/minisat/ParseUtils.h"
+
+using namespace Minisat;
+
+void Minisat::parseOptions(int& argc, char** argv, bool strict)
+{
+    int i, j;
+    for (i = j = 1; i < argc; i++){
+        const char* str = argv[i];
+        if (match(str, "--") && match(str, Option::getHelpPrefixString()) && match(str, "help")){
+            if (*str == '\0')
+                printUsageAndExit(argc, argv);
+            else if (match(str, "-verb"))
+                printUsageAndExit(argc, argv, true);
+        } else {
+            bool parsed_ok = false;
+        
+            for (int k = 0; !parsed_ok && k < Option::getOptionList().size(); k++){
+                parsed_ok = Option::getOptionList()[k]->parse(argv[i]);
+
+                // fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip");
+            }
+
+            if (!parsed_ok){
+                if (strict && match(argv[i], "-"))
+                    fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1);
+                else
+                    argv[j++] = argv[i];
+            }
+        }
+    }
+
+    argc -= (i - j);
+}
+
+
+void Minisat::setUsageHelp      (const char* str){ Option::getUsageString() = str; }
+void Minisat::setHelpPrefixStr  (const char* str){ Option::getHelpPrefixString() = str; }
+void Minisat::printUsageAndExit (int /*argc*/, char** argv, bool verbose)
+{
+    const char* usage = Option::getUsageString();
+    if (usage != NULL)
+        fprintf(stderr, usage, argv[0]);
+
+    sort(Option::getOptionList(), Option::OptionLt());
+
+    const char* prev_cat  = NULL;
+    const char* prev_type = NULL;
+
+    for (int i = 0; i < Option::getOptionList().size(); i++){
+        const char* cat  = Option::getOptionList()[i]->category;
+        const char* type = Option::getOptionList()[i]->type_name;
+
+        if (cat != prev_cat)
+            fprintf(stderr, "\n%s OPTIONS:\n\n", cat);
+        else if (type != prev_type)
+            fprintf(stderr, "\n");
+
+        Option::getOptionList()[i]->help(verbose);
+
+        prev_cat  = Option::getOptionList()[i]->category;
+        prev_type = Option::getOptionList()[i]->type_name;
+    }
+
+    fprintf(stderr, "\nHELP OPTIONS:\n\n");
+    fprintf(stderr, "  --%shelp        Print help message.\n", Option::getHelpPrefixString());
+    fprintf(stderr, "  --%shelp-verb   Print verbose help message.\n", Option::getHelpPrefixString());
+    fprintf(stderr, "\n");
+    exit(0);
+}
+
diff --git a/libs/minisat/Options.h b/libs/minisat/Options.h
new file mode 100644
index 000000000..7d140a1ff
--- /dev/null
+++ b/libs/minisat/Options.h
@@ -0,0 +1,386 @@
+/***************************************************************************************[Options.h]
+Copyright (c) 2008-2010, 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 Minisat_Options_h
+#define Minisat_Options_h
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <math.h>
+#include <string.h>
+
+#include "libs/minisat/IntTypes.h"
+#include "libs/minisat/Vec.h"
+#include "libs/minisat/ParseUtils.h"
+
+namespace Minisat {
+
+//==================================================================================================
+// Top-level option parse/help functions:
+
+
+extern void parseOptions     (int& argc, char** argv, bool strict = false);
+extern void printUsageAndExit(int  argc, char** argv, bool verbose = false);
+extern void setUsageHelp     (const char* str);
+extern void setHelpPrefixStr (const char* str);
+
+
+//==================================================================================================
+// Options is an abstract class that gives the interface for all types options:
+
+
+class Option
+{
+ protected:
+    const char* name;
+    const char* description;
+    const char* category;
+    const char* type_name;
+
+    static vec<Option*>& getOptionList () { static vec<Option*> options; return options; }
+    static const char*&  getUsageString() { static const char* usage_str; return usage_str; }
+    static const char*&  getHelpPrefixString() { static const char* help_prefix_str = ""; return help_prefix_str; }
+
+    struct OptionLt {
+        bool operator()(const Option* x, const Option* y) {
+            int test1 = strcmp(x->category, y->category);
+            return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
+        }
+    };
+
+    Option(const char* name_, 
+           const char* desc_,
+           const char* cate_,
+           const char* type_) : 
+      name       (name_)
+    , description(desc_)
+    , category   (cate_)
+    , type_name  (type_)
+    { 
+        getOptionList().push(this); 
+    }
+
+ public:
+    virtual ~Option() {}
+
+    virtual bool parse             (const char* str)      = 0;
+    virtual void help              (bool verbose = false) = 0;
+
+    friend  void parseOptions      (int& argc, char** argv, bool strict);
+    friend  void printUsageAndExit (int  argc, char** argv, bool verbose);
+    friend  void setUsageHelp      (const char* str);
+    friend  void setHelpPrefixStr  (const char* str);
+};
+
+
+//==================================================================================================
+// Range classes with specialization for floating types:
+
+
+struct IntRange {
+    int begin;
+    int end;
+    IntRange(int b, int e) : begin(b), end(e) {}
+};
+
+struct Int64Range {
+    int64_t begin;
+    int64_t end;
+    Int64Range(int64_t b, int64_t e) : begin(b), end(e) {}
+};
+
+struct DoubleRange {
+    double begin;
+    double end;
+    bool  begin_inclusive;
+    bool  end_inclusive;
+    DoubleRange(double b, bool binc, double e, bool einc) : begin(b), end(e), begin_inclusive(binc), end_inclusive(einc) {}
+};
+
+
+//==================================================================================================
+// Double options:
+
+
+class DoubleOption : public Option
+{
+ protected:
+    DoubleRange range;
+    double      value;
+
+ public:
+    DoubleOption(const char* c, const char* n, const char* d, double def = double(), DoubleRange r = DoubleRange(-HUGE_VAL, false, HUGE_VAL, false))
+        : Option(n, d, c, "<double>"), range(r), value(def) {
+        // FIXME: set LC_NUMERIC to "C" to make sure that strtof/strtod parses decimal point correctly.
+    }
+
+    operator      double   (void) const { return value; }
+    operator      double&  (void)       { return value; }
+    DoubleOption& operator=(double x)   { value = x; return *this; }
+
+    virtual bool parse(const char* str){
+        const char* span = str; 
+
+        if (!match(span, "-") || !match(span, name) || !match(span, "="))
+            return false;
+
+        char*  end;
+        double tmp = strtod(span, &end);
+
+        if (end == NULL) 
+            return false;
+        else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){
+            fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
+            exit(1);
+        }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){
+            fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
+            exit(1); }
+
+        value = tmp;
+        // fprintf(stderr, "READ VALUE: %g\n", value);
+
+        return true;
+    }
+
+    virtual void help (bool verbose = false){
+        fprintf(stderr, "  -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n", 
+                name, type_name, 
+                range.begin_inclusive ? '[' : '(', 
+                range.begin,
+                range.end,
+                range.end_inclusive ? ']' : ')', 
+                value);
+        if (verbose){
+            fprintf(stderr, "\n        %s\n", description);
+            fprintf(stderr, "\n");
+        }
+    }
+};
+
+
+//==================================================================================================
+// Int options:
+
+
+class IntOption : public Option
+{
+ protected:
+    IntRange range;
+    int32_t  value;
+
+ public:
+    IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX))
+        : Option(n, d, c, "<int32>"), range(r), value(def) {}
+ 
+    operator   int32_t   (void) const { return value; }
+    operator   int32_t&  (void)       { return value; }
+    IntOption& operator= (int32_t x)  { value = x; return *this; }
+
+    virtual bool parse(const char* str){
+        const char* span = str; 
+
+        if (!match(span, "-") || !match(span, name) || !match(span, "="))
+            return false;
+
+        char*   end;
+        int32_t tmp = strtol(span, &end, 10);
+
+        if (end == NULL) 
+            return false;
+        else if (tmp > range.end){
+            fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
+            exit(1);
+        }else if (tmp < range.begin){
+            fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
+            exit(1); }
+
+        value = tmp;
+
+        return true;
+    }
+
+    virtual void help (bool verbose = false){
+        fprintf(stderr, "  -%-12s = %-8s [", name, type_name);
+        if (range.begin == INT32_MIN)
+            fprintf(stderr, "imin");
+        else
+            fprintf(stderr, "%4d", range.begin);
+
+        fprintf(stderr, " .. ");
+        if (range.end == INT32_MAX)
+            fprintf(stderr, "imax");
+        else
+            fprintf(stderr, "%4d", range.end);
+
+        fprintf(stderr, "] (default: %d)\n", value);
+        if (verbose){
+            fprintf(stderr, "\n        %s\n", description);
+            fprintf(stderr, "\n");
+        }
+    }
+};
+
+
+// Leave this out for visual C++ until Microsoft implements C99 and gets support for strtoll.
+#ifndef _MSC_VER
+
+class Int64Option : public Option
+{
+ protected:
+    Int64Range range;
+    int64_t  value;
+
+ public:
+    Int64Option(const char* c, const char* n, const char* d, int64_t def = int64_t(), Int64Range r = Int64Range(INT64_MIN, INT64_MAX))
+        : Option(n, d, c, "<int64>"), range(r), value(def) {}
+ 
+    operator     int64_t   (void) const { return value; }
+    operator     int64_t&  (void)       { return value; }
+    Int64Option& operator= (int64_t x)  { value = x; return *this; }
+
+    virtual bool parse(const char* str){
+        const char* span = str; 
+
+        if (!match(span, "-") || !match(span, name) || !match(span, "="))
+            return false;
+
+        char*   end;
+        int64_t tmp = strtoll(span, &end, 10);
+
+        if (end == NULL) 
+            return false;
+        else if (tmp > range.end){
+            fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
+            exit(1);
+        }else if (tmp < range.begin){
+            fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
+            exit(1); }
+
+        value = tmp;
+
+        return true;
+    }
+
+    virtual void help (bool verbose = false){
+        fprintf(stderr, "  -%-12s = %-8s [", name, type_name);
+        if (range.begin == INT64_MIN)
+            fprintf(stderr, "imin");
+        else
+            fprintf(stderr, "%4" PRIi64 , range.begin);
+
+        fprintf(stderr, " .. ");
+        if (range.end == INT64_MAX)
+            fprintf(stderr, "imax");
+        else
+            fprintf(stderr, "%4" PRIi64 , range.end);
+
+        fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
+        if (verbose){
+            fprintf(stderr, "\n        %s\n", description);
+            fprintf(stderr, "\n");
+        }
+    }
+};
+#endif
+
+//==================================================================================================
+// String option:
+
+
+class StringOption : public Option
+{
+    const char* value;
+ public:
+    StringOption(const char* c, const char* n, const char* d, const char* def = NULL) 
+        : Option(n, d, c, "<string>"), value(def) {}
+
+    operator      const char*  (void) const     { return value; }
+    operator      const char*& (void)           { return value; }
+    StringOption& operator=    (const char* x)  { value = x; return *this; }
+
+    virtual bool parse(const char* str){
+        const char* span = str; 
+
+        if (!match(span, "-") || !match(span, name) || !match(span, "="))
+            return false;
+
+        value = span;
+        return true;
+    }
+
+    virtual void help (bool verbose = false){
+        fprintf(stderr, "  -%-10s = %8s\n", name, type_name);
+        if (verbose){
+            fprintf(stderr, "\n        %s\n", description);
+            fprintf(stderr, "\n");
+        }
+    }    
+};
+
+
+//==================================================================================================
+// Bool option:
+
+
+class BoolOption : public Option
+{
+    bool value;
+
+ public:
+    BoolOption(const char* c, const char* n, const char* d, bool v) 
+        : Option(n, d, c, "<bool>"), value(v) {}
+
+    operator    bool     (void) const { return value; }
+    operator    bool&    (void)       { return value; }
+    BoolOption& operator=(bool b)     { value = b; return *this; }
+
+    virtual bool parse(const char* str){
+        const char* span = str; 
+        
+        if (match(span, "-")){
+            bool b = !match(span, "no-");
+
+            if (strcmp(span, name) == 0){
+                value = b;
+                return true; }
+        }
+
+        return false;
+    }
+
+    virtual void help (bool verbose = false){
+
+        fprintf(stderr, "  -%s, -no-%s", name, name);
+
+        for (uint32_t i = 0; i < 32 - strlen(name)*2; i++)
+            fprintf(stderr, " ");
+
+        fprintf(stderr, " ");
+        fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
+        if (verbose){
+            fprintf(stderr, "\n        %s\n", description);
+            fprintf(stderr, "\n");
+        }
+    }
+};
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/ParseUtils.h b/libs/minisat/ParseUtils.h
new file mode 100644
index 000000000..7b2ddc554
--- /dev/null
+++ b/libs/minisat/ParseUtils.h
@@ -0,0 +1,129 @@
+/************************************************************************************[ParseUtils.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_ParseUtils_h
+#define Minisat_ParseUtils_h
+
+#include <stdlib.h>
+#include <stdio.h>
+
+#include <zlib.h>
+
+#include "libs/minisat/XAlloc.h"
+
+namespace Minisat {
+
+//-------------------------------------------------------------------------------------------------
+// A simple buffered character stream class:
+
+
+
+class StreamBuffer {
+    gzFile         in;
+    unsigned char* buf;
+    int            pos;
+    int            size;
+
+    enum { buffer_size = 64*1024 };
+
+    void assureLookahead() {
+        if (pos >= size) {
+            pos  = 0;
+            size = gzread(in, buf, buffer_size); } }
+
+public:
+    explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0){
+        buf = (unsigned char*)xrealloc(NULL, buffer_size);
+        assureLookahead();
+    }
+    ~StreamBuffer() { free(buf); }
+
+    int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
+    void operator ++ ()       { pos++; assureLookahead(); }
+    int  position    () const { return pos; }
+};
+
+
+//-------------------------------------------------------------------------------------------------
+// End-of-file detection functions for StreamBuffer and char*:
+
+
+static inline bool isEof(StreamBuffer& in) { return *in == EOF;  }
+static inline bool isEof(const char*   in) { return *in == '\0'; }
+
+//-------------------------------------------------------------------------------------------------
+// Generic parse functions parametrized over the input-stream type.
+
+
+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 (isEof(in)) 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; }
+
+
+// String matching: in case of a match the input iterator will be advanced the corresponding
+// number of characters.
+template<class B>
+static bool match(B& in, const char* str) {
+    int i;
+    for (i = 0; str[i] != '\0'; i++)
+        if (in[i] != str[i])
+            return false;
+
+    in += i;
+
+    return true; 
+}
+
+// String matching: consumes characters eagerly, but does not require random access iterator.
+template<class B>
+static bool eagerMatch(B& in, const char* str) {
+    for (; *str != '\0'; ++str, ++in)
+        if (*str != *in)
+            return false;
+    return true; }
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Queue.h b/libs/minisat/Queue.h
new file mode 100644
index 000000000..1cae4f5ad
--- /dev/null
+++ b/libs/minisat/Queue.h
@@ -0,0 +1,69 @@
+/*****************************************************************************************[Queue.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Queue_h
+#define Minisat_Queue_h
+
+#include "libs/minisat/Vec.h"
+
+namespace Minisat {
+
+//=================================================================================================
+
+template<class T>
+class Queue {
+    vec<T>  buf;
+    int     first;
+    int     end;
+
+public:
+    typedef T Key;
+
+    Queue() : buf(1), first(0), end(0) {}
+
+    void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; }
+    int  size  () const { return (end >= first) ? end - first : end - first + buf.size(); }
+
+    const T& operator [] (int index) const  { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+    T&       operator [] (int index)        { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; }
+
+    T    peek  () const { assert(first != end); return buf[first]; }
+    void pop   () { assert(first != end); first++; if (first == buf.size()) first = 0; }
+    void insert(T elem) {   // INVARIANT: buf[end] is always unused
+        buf[end++] = elem;
+        if (end == buf.size()) end = 0;
+        if (first == end){  // Resize:
+            vec<T>  tmp((buf.size()*3 + 1) >> 1);
+            //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0);
+            int     i = 0;
+            for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j];
+            for (int j = 0    ; j < end       ; j++) tmp[i++] = buf[j];
+            first = 0;
+            end   = buf.size();
+            tmp.moveTo(buf);
+        }
+    }
+};
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Rnd.h b/libs/minisat/Rnd.h
new file mode 100644
index 000000000..cf7061014
--- /dev/null
+++ b/libs/minisat/Rnd.h
@@ -0,0 +1,67 @@
+/*******************************************************************************************[Rnd.h]
+Copyright (c) 2012, 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 Minisat_Rnd_h
+#define Minisat_Rnd_h
+
+#include "libs/minisat/Vec.h"
+
+namespace Minisat {
+
+// Generate a random double:
+static inline double drand(double& seed)
+{
+    seed *= 1389796;
+    int q = (int)(seed / 2147483647);
+    seed -= (double)q * 2147483647;
+    return seed / 2147483647;
+}
+
+
+// Generate a random integer:
+static inline int irand(double& seed, int size) { return (int)(drand(seed) * size); }
+
+
+// Randomly shuffle the contents of a vector:
+template<class T>
+static void randomShuffle(double& seed, vec<T>& xs)
+{
+    for (int i = 0; i < xs.size(); i++){
+        int pick = i + irand(seed, xs.size() - i);
+        T tmp = xs[i];
+        xs[i] = xs[pick];
+        xs[pick] = tmp;
+    }
+}
+
+// Randomly shuffle a vector of a vector (ugly)
+template<class T>
+static void randomShuffle(double& seed, vec<vec<T> >& xs)
+{
+    for (int i = 0; i < xs.size(); i++){
+        int pick = i + irand(seed, xs.size() - i);
+        vec<T> tmp; xs[i].moveTo(tmp);
+        xs[pick].moveTo(xs[i]);
+        tmp.moveTo(xs[pick]);
+    }
+}
+
+
+//=================================================================================================
+} // namespace Minisat
+#endif
diff --git a/libs/minisat/SimpSolver.cc b/libs/minisat/SimpSolver.cc
new file mode 100644
index 000000000..232368106
--- /dev/null
+++ b/libs/minisat/SimpSolver.cc
@@ -0,0 +1,727 @@
+#define __STDC_FORMAT_MACROS
+#define __STDC_LIMIT_MACROS
+/***********************************************************************************[SimpSolver.cc]
+Copyright (c) 2006,      Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 "libs/minisat/Sort.h"
+#include "libs/minisat/SimpSolver.h"
+#include "libs/minisat/System.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+// Options:
+
+
+static const char* _cat = "SIMP";
+
+static BoolOption   opt_use_asymm        (_cat, "asymm",        "Shrink clauses by asymmetric branching.", false);
+static BoolOption   opt_use_rcheck       (_cat, "rcheck",       "Check if a clause is already implied. (costly)", false);
+static BoolOption   opt_use_elim         (_cat, "elim",         "Perform variable elimination.", true);
+static IntOption    opt_grow             (_cat, "grow",         "Allow a variable elimination step to grow by a number of clauses.", 0);
+static IntOption    opt_clause_lim       (_cat, "cl-lim",       "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20,   IntRange(-1, INT32_MAX));
+static IntOption    opt_subsumption_lim  (_cat, "sub-lim",      "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
+static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.",  0.5, DoubleRange(0, false, HUGE_VAL, false));
+
+
+//=================================================================================================
+// Constructor/Destructor:
+
+
+SimpSolver::SimpSolver() :
+    grow               (opt_grow)
+  , clause_lim         (opt_clause_lim)
+  , subsumption_lim    (opt_subsumption_lim)
+  , simp_garbage_frac  (opt_simp_garbage_frac)
+  , use_asymm          (opt_use_asymm)
+  , use_rcheck         (opt_use_rcheck)
+  , use_elim           (opt_use_elim)
+  , extend_model       (true)
+  , merges             (0)
+  , asymm_lits         (0)
+  , eliminated_vars    (0)
+  , elimorder          (1)
+  , use_simplification (true)
+  , occurs             (ClauseDeleted(ca))
+  , elim_heap          (ElimLt(n_occ))
+  , bwdsub_assigns     (0)
+  , n_touched          (0)
+{
+    vec<Lit> dummy(1,lit_Undef);
+    ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
+    bwdsub_tmpunit        = ca.alloc(dummy);
+    remove_satisfied      = false;
+}
+
+
+SimpSolver::~SimpSolver()
+{
+}
+
+
+Var SimpSolver::newVar(lbool upol, bool dvar) {
+    Var v = Solver::newVar(upol, dvar);
+
+    frozen    .insert(v, (char)false);
+    eliminated.insert(v, (char)false);
+
+    if (use_simplification){
+        n_occ     .insert( mkLit(v), 0);
+        n_occ     .insert(~mkLit(v), 0);
+        occurs    .init  (v);
+        touched   .insert(v, 0);
+        elim_heap .insert(v);
+    }
+    return v; }
+
+
+void SimpSolver::releaseVar(Lit l)
+{
+    assert(!isEliminated(var(l)));
+    if (!use_simplification && var(l) >= max_simp_var)
+        // Note: Guarantees that no references to this variable is
+        // left in model extension datastructure. Could be improved!
+        Solver::releaseVar(l);
+    else
+        // Otherwise, don't allow variable to be reused.
+        Solver::addClause(l);
+}
+
+
+lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
+{
+    vec<Var> extra_frozen;
+    lbool    result = l_True;
+
+    do_simp &= use_simplification;
+
+    if (do_simp){
+        // Assumptions must be temporarily frozen to run variable elimination:
+        for (int i = 0; i < assumptions.size(); i++){
+            Var v = var(assumptions[i]);
+
+            // If an assumption has been eliminated, remember it.
+            assert(!isEliminated(v));
+
+            if (!frozen[v]){
+                // Freeze and store.
+                setFrozen(v, true);
+                extra_frozen.push(v);
+            } }
+
+        result = lbool(eliminate(turn_off_simp));
+    }
+
+    if (result == l_True)
+        result = Solver::solve_();
+    else if (verbosity >= 1)
+        printf("===============================================================================\n");
+
+    if (result == l_True && extend_model)
+        extendModel();
+
+    if (do_simp)
+        // Unfreeze the assumptions that were frozen:
+        for (int i = 0; i < extra_frozen.size(); i++)
+            setFrozen(extra_frozen[i], false);
+
+    return result;
+}
+
+
+
+bool SimpSolver::addClause_(vec<Lit>& ps)
+{
+#ifndef NDEBUG
+    for (int i = 0; i < ps.size(); i++)
+        assert(!isEliminated(var(ps[i])));
+#endif
+
+    int nclauses = clauses.size();
+
+    if (use_rcheck && implied(ps))
+        return true;
+
+    if (!Solver::addClause_(ps))
+        return false;
+
+    if (use_simplification && clauses.size() == nclauses + 1){
+        CRef          cr = clauses.last();
+        const Clause& c  = ca[cr];
+
+        // NOTE: the clause is added to the queue immediately and then
+        // again during 'gatherTouchedClauses()'. If nothing happens
+        // in between, it will only be checked once. Otherwise, it may
+        // be checked twice unnecessarily. This is an unfortunate
+        // consequence of how backward subsumption is used to mimic
+        // forward subsumption.
+        subsumption_queue.insert(cr);
+        for (int i = 0; i < c.size(); i++){
+            occurs[var(c[i])].push(cr);
+            n_occ[c[i]]++;
+            touched[var(c[i])] = 1;
+            n_touched++;
+            if (elim_heap.inHeap(var(c[i])))
+                elim_heap.increase(var(c[i]));
+        }
+    }
+
+    return true;
+}
+
+
+void SimpSolver::removeClause(CRef cr)
+{
+    const Clause& c = ca[cr];
+
+    if (use_simplification)
+        for (int i = 0; i < c.size(); i++){
+            n_occ[c[i]]--;
+            updateElimHeap(var(c[i]));
+            occurs.smudge(var(c[i]));
+        }
+
+    Solver::removeClause(cr);
+}
+
+
+bool SimpSolver::strengthenClause(CRef cr, Lit l)
+{
+    Clause& c = ca[cr];
+    assert(decisionLevel() == 0);
+    assert(use_simplification);
+
+    // FIX: this is too inefficient but would be nice to have (properly implemented)
+    // if (!find(subsumption_queue, &c))
+    subsumption_queue.insert(cr);
+
+    if (c.size() == 2){
+        removeClause(cr);
+        c.strengthen(l);
+    }else{
+        detachClause(cr, true);
+        c.strengthen(l);
+        attachClause(cr);
+        remove(occurs[var(l)], cr);
+        n_occ[l]--;
+        updateElimHeap(var(l));
+    }
+
+    return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
+}
+
+
+// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
+{
+    merges++;
+    out_clause.clear();
+
+    bool  ps_smallest = _ps.size() < _qs.size();
+    const Clause& ps  =  ps_smallest ? _qs : _ps;
+    const Clause& qs  =  ps_smallest ? _ps : _qs;
+
+    for (int i = 0; i < qs.size(); i++){
+        if (var(qs[i]) != v){
+            for (int j = 0; j < ps.size(); j++)
+                if (var(ps[j]) == var(qs[i])){
+                    if (ps[j] == ~qs[i])
+                        return false;
+                    else
+                        goto next;
+                }
+            out_clause.push(qs[i]);
+        }
+        next:;
+    }
+
+    for (int i = 0; i < ps.size(); i++)
+        if (var(ps[i]) != v)
+            out_clause.push(ps[i]);
+
+    return true;
+}
+
+
+// Returns FALSE if clause is always satisfied.
+bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
+{
+    merges++;
+
+    bool  ps_smallest = _ps.size() < _qs.size();
+    const Clause& ps  =  ps_smallest ? _qs : _ps;
+    const Clause& qs  =  ps_smallest ? _ps : _qs;
+    const Lit*  __ps  = (const Lit*)ps;
+    const Lit*  __qs  = (const Lit*)qs;
+
+    size = ps.size()-1;
+
+    for (int i = 0; i < qs.size(); i++){
+        if (var(__qs[i]) != v){
+            for (int j = 0; j < ps.size(); j++)
+                if (var(__ps[j]) == var(__qs[i])){
+                    if (__ps[j] == ~__qs[i])
+                        return false;
+                    else
+                        goto next;
+                }
+            size++;
+        }
+        next:;
+    }
+
+    return true;
+}
+
+
+void SimpSolver::gatherTouchedClauses()
+{
+    if (n_touched == 0) return;
+
+    int i,j;
+    for (i = j = 0; i < subsumption_queue.size(); i++)
+        if (ca[subsumption_queue[i]].mark() == 0)
+            ca[subsumption_queue[i]].mark(2);
+
+    for (i = 0; i < nVars(); i++)
+        if (touched[i]){
+            const vec<CRef>& cs = occurs.lookup(i);
+            for (j = 0; j < cs.size(); j++)
+                if (ca[cs[j]].mark() == 0){
+                    subsumption_queue.insert(cs[j]);
+                    ca[cs[j]].mark(2);
+                }
+            touched[i] = 0;
+        }
+
+    for (i = 0; i < subsumption_queue.size(); i++)
+        if (ca[subsumption_queue[i]].mark() == 2)
+            ca[subsumption_queue[i]].mark(0);
+
+    n_touched = 0;
+}
+
+
+bool SimpSolver::implied(const vec<Lit>& c)
+{
+    assert(decisionLevel() == 0);
+
+    trail_lim.push(trail.size());
+    for (int i = 0; i < c.size(); i++)
+        if (value(c[i]) == l_True){
+            cancelUntil(0);
+            return true;
+        }else if (value(c[i]) != l_False){
+            assert(value(c[i]) == l_Undef);
+            uncheckedEnqueue(~c[i]);
+        }
+
+    bool result = propagate() != CRef_Undef;
+    cancelUntil(0);
+    return result;
+}
+
+
+// Backward subsumption + backward subsumption resolution
+bool SimpSolver::backwardSubsumptionCheck(bool verbose)
+{
+    int cnt = 0;
+    int subsumed = 0;
+    int deleted_literals = 0;
+    assert(decisionLevel() == 0);
+
+    while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
+
+        // Empty subsumption queue and return immediately on user-interrupt:
+        if (asynch_interrupt){
+            subsumption_queue.clear();
+            bwdsub_assigns = trail.size();
+            break; }
+
+        // Check top-level assignments by creating a dummy clause and placing it in the queue:
+        if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
+            Lit l = trail[bwdsub_assigns++];
+            ca[bwdsub_tmpunit][0] = l;
+            ca[bwdsub_tmpunit].calcAbstraction();
+            subsumption_queue.insert(bwdsub_tmpunit); }
+
+        CRef    cr = subsumption_queue.peek(); subsumption_queue.pop();
+        Clause& c  = ca[cr];
+
+        if (c.mark()) continue;
+
+        if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
+            printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
+
+        assert(c.size() > 1 || value(c[0]) == l_True);    // Unit-clauses should have been propagated before this point.
+
+        // Find best variable to scan:
+        Var best = var(c[0]);
+        for (int i = 1; i < c.size(); i++)
+            if (occurs[var(c[i])].size() < occurs[best].size())
+                best = var(c[i]);
+
+        // Search all candidates:
+        vec<CRef>& _cs = occurs.lookup(best);
+        CRef*       cs = (CRef*)_cs;
+
+        for (int j = 0; j < _cs.size(); j++)
+            if (c.mark())
+                break;
+            else if (!ca[cs[j]].mark() &&  cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
+                Lit l = c.subsumes(ca[cs[j]]);
+
+                if (l == lit_Undef)
+                    subsumed++, removeClause(cs[j]);
+                else if (l != lit_Error){
+                    deleted_literals++;
+
+                    if (!strengthenClause(cs[j], ~l))
+                        return false;
+
+                    // Did current candidate get deleted from cs? Then check candidate at index j again:
+                    if (var(l) == best)
+                        j--;
+                }
+            }
+    }
+
+    return true;
+}
+
+
+bool SimpSolver::asymm(Var v, CRef cr)
+{
+    Clause& c = ca[cr];
+    assert(decisionLevel() == 0);
+
+    if (c.mark() || satisfied(c)) return true;
+
+    trail_lim.push(trail.size());
+    Lit l = lit_Undef;
+    for (int i = 0; i < c.size(); i++)
+        if (var(c[i]) != v && value(c[i]) != l_False)
+            uncheckedEnqueue(~c[i]);
+        else
+            l = c[i];
+
+    if (propagate() != CRef_Undef){
+        cancelUntil(0);
+        asymm_lits++;
+        if (!strengthenClause(cr, l))
+            return false;
+    }else
+        cancelUntil(0);
+
+    return true;
+}
+
+
+bool SimpSolver::asymmVar(Var v)
+{
+    assert(use_simplification);
+
+    const vec<CRef>& cls = occurs.lookup(v);
+
+    if (value(v) != l_Undef || cls.size() == 0)
+        return true;
+
+    for (int i = 0; i < cls.size(); i++)
+        if (!asymm(v, cls[i]))
+            return false;
+
+    return backwardSubsumptionCheck();
+}
+
+
+static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
+{
+    elimclauses.push(toInt(x));
+    elimclauses.push(1);
+}
+
+
+static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
+{
+    int first = elimclauses.size();
+    int v_pos = -1;
+
+    // Copy clause to elimclauses-vector. Remember position where the
+    // variable 'v' occurs:
+    for (int i = 0; i < c.size(); i++){
+        elimclauses.push(toInt(c[i]));
+        if (var(c[i]) == v)
+            v_pos = i + first;
+    }
+    assert(v_pos != -1);
+
+    // Swap the first literal with the 'v' literal, so that the literal
+    // containing 'v' will occur first in the clause:
+    uint32_t tmp = elimclauses[v_pos];
+    elimclauses[v_pos] = elimclauses[first];
+    elimclauses[first] = tmp;
+
+    // Store the length of the clause last:
+    elimclauses.push(c.size());
+}
+
+
+
+bool SimpSolver::eliminateVar(Var v)
+{
+    assert(!frozen[v]);
+    assert(!isEliminated(v));
+    assert(value(v) == l_Undef);
+
+    // Split the occurrences into positive and negative:
+    //
+    const vec<CRef>& cls = occurs.lookup(v);
+    vec<CRef>        pos, neg;
+    for (int i = 0; i < cls.size(); i++)
+        (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
+
+    // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
+    // clause must exceed the limit on the maximal clause size (if it is set):
+    //
+    int cnt         = 0;
+    int clause_size = 0;
+
+    for (int i = 0; i < pos.size(); i++)
+        for (int j = 0; j < neg.size(); j++)
+            if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) && 
+                (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
+                return true;
+
+    // Delete and store old clauses:
+    eliminated[v] = true;
+    setDecisionVar(v, false);
+    eliminated_vars++;
+
+    if (pos.size() > neg.size()){
+        for (int i = 0; i < neg.size(); i++)
+            mkElimClause(elimclauses, v, ca[neg[i]]);
+        mkElimClause(elimclauses, mkLit(v));
+    }else{
+        for (int i = 0; i < pos.size(); i++)
+            mkElimClause(elimclauses, v, ca[pos[i]]);
+        mkElimClause(elimclauses, ~mkLit(v));
+    }
+
+    for (int i = 0; i < cls.size(); i++)
+        removeClause(cls[i]); 
+
+    // Produce clauses in cross product:
+    vec<Lit>& resolvent = add_tmp;
+    for (int i = 0; i < pos.size(); i++)
+        for (int j = 0; j < neg.size(); j++)
+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
+                return false;
+
+    // Free occurs list for this variable:
+    occurs[v].clear(true);
+    
+    // Free watchers lists for this variable, if possible:
+    if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
+    if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
+
+    return backwardSubsumptionCheck();
+}
+
+
+bool SimpSolver::substitute(Var v, Lit x)
+{
+    assert(!frozen[v]);
+    assert(!isEliminated(v));
+    assert(value(v) == l_Undef);
+
+    if (!ok) return false;
+
+    eliminated[v] = true;
+    setDecisionVar(v, false);
+    const vec<CRef>& cls = occurs.lookup(v);
+    
+    vec<Lit>& subst_clause = add_tmp;
+    for (int i = 0; i < cls.size(); i++){
+        Clause& c = ca[cls[i]];
+
+        subst_clause.clear();
+        for (int j = 0; j < c.size(); j++){
+            Lit p = c[j];
+            subst_clause.push(var(p) == v ? x ^ sign(p) : p);
+        }
+
+        removeClause(cls[i]);
+
+        if (!addClause_(subst_clause))
+            return ok = false;
+    }
+
+    return true;
+}
+
+
+void SimpSolver::extendModel()
+{
+    int i, j;
+    Lit x;
+
+    for (i = elimclauses.size()-1; i > 0; i -= j){
+        for (j = elimclauses[i--]; j > 1; j--, i--)
+            if (modelValue(toLit(elimclauses[i])) != l_False)
+                goto next;
+
+        x = toLit(elimclauses[i]);
+        model[var(x)] = lbool(!sign(x));
+    next:;
+    }
+}
+
+
+bool SimpSolver::eliminate(bool turn_off_elim)
+{
+    if (!simplify())
+        return false;
+    else if (!use_simplification)
+        return true;
+
+    // Main simplification loop:
+    //
+    while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
+
+        gatherTouchedClauses();
+        // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
+        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && 
+            !backwardSubsumptionCheck(true)){
+            ok = false; goto cleanup; }
+
+        // Empty elim_heap and return immediately on user-interrupt:
+        if (asynch_interrupt){
+            assert(bwdsub_assigns == trail.size());
+            assert(subsumption_queue.size() == 0);
+            assert(n_touched == 0);
+            elim_heap.clear();
+            goto cleanup; }
+
+        // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
+        for (int cnt = 0; !elim_heap.empty(); cnt++){
+            Var elim = elim_heap.removeMin();
+            
+            if (asynch_interrupt) break;
+
+            if (isEliminated(elim) || value(elim) != l_Undef) continue;
+
+            if (verbosity >= 2 && cnt % 100 == 0)
+                printf("elimination left: %10d\r", elim_heap.size());
+
+            if (use_asymm){
+                // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
+                bool was_frozen = frozen[elim];
+                frozen[elim] = true;
+                if (!asymmVar(elim)){
+                    ok = false; goto cleanup; }
+                frozen[elim] = was_frozen; }
+
+            // At this point, the variable may have been set by assymetric branching, so check it
+            // again. Also, don't eliminate frozen variables:
+            if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
+                ok = false; goto cleanup; }
+
+            checkGarbage(simp_garbage_frac);
+        }
+
+        assert(subsumption_queue.size() == 0);
+    }
+ cleanup:
+
+    // If no more simplification is needed, free all simplification-related data structures:
+    if (turn_off_elim){
+        touched  .clear(true);
+        occurs   .clear(true);
+        n_occ    .clear(true);
+        elim_heap.clear(true);
+        subsumption_queue.clear(true);
+
+        use_simplification    = false;
+        remove_satisfied      = true;
+        ca.extra_clause_field = false;
+        max_simp_var          = nVars();
+
+        // Force full cleanup (this is safe and desirable since it only happens once):
+        rebuildOrderHeap();
+        garbageCollect();
+    }else{
+        // Cheaper cleanup:
+        checkGarbage();
+    }
+
+    if (verbosity >= 1 && elimclauses.size() > 0)
+        printf("|  Eliminated clauses:     %10.2f Mb                                      |\n", 
+               double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+
+    return ok;
+}
+
+
+//=================================================================================================
+// Garbage Collection methods:
+
+
+void SimpSolver::relocAll(ClauseAllocator& to)
+{
+    if (!use_simplification) return;
+
+    // All occurs lists:
+    //
+    for (int i = 0; i < nVars(); i++){
+        occurs.clean(i);
+        vec<CRef>& cs = occurs[i];
+        for (int j = 0; j < cs.size(); j++)
+            ca.reloc(cs[j], to);
+    }
+
+    // Subsumption queue:
+    //
+    for (int i = subsumption_queue.size(); i > 0; i--){
+        CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
+        if (ca[cr].mark()) continue;
+        ca.reloc(cr, to);
+        subsumption_queue.insert(cr);
+    }
+        
+    // Temporary clause:
+    //
+    ca.reloc(bwdsub_tmpunit, to);
+}
+
+
+void SimpSolver::garbageCollect()
+{
+    // Initialize the next region to a size corresponding to the estimated utilization degree. This
+    // is not precise but should avoid some unnecessary reallocations for the new region:
+    ClauseAllocator to(ca.size() - ca.wasted()); 
+
+    to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
+    relocAll(to);
+    Solver::relocAll(to);
+    if (verbosity >= 2)
+        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
+               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+    to.moveTo(ca);
+}
diff --git a/libs/minisat/SimpSolver.h b/libs/minisat/SimpSolver.h
new file mode 100644
index 000000000..fc9bb4391
--- /dev/null
+++ b/libs/minisat/SimpSolver.h
@@ -0,0 +1,222 @@
+/************************************************************************************[SimpSolver.h]
+Copyright (c) 2006,      Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_SimpSolver_h
+#define Minisat_SimpSolver_h
+
+#include "libs/minisat/Queue.h"
+#include "libs/minisat/Solver.h"
+
+
+namespace Minisat {
+
+//=================================================================================================
+
+
+class SimpSolver : public Solver {
+ public:
+    // Constructor/Destructor:
+    //
+    SimpSolver();
+    ~SimpSolver();
+
+    // Problem specification:
+    //
+    Var     newVar    (lbool upol = l_Undef, bool dvar = true);
+    void    releaseVar(Lit l);
+    bool    addClause (const vec<Lit>& ps);
+    bool    addEmptyClause();                // Add the empty clause to the solver.
+    bool    addClause (Lit p);               // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q);        // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, Lit s); // Add a quaternary clause to the solver. 
+    bool    addClause_(      vec<Lit>& ps);
+    bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
+
+    // Variable mode:
+    // 
+    void    setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
+    bool    isEliminated(Var v) const;
+
+    // Alternative freeze interface (may replace 'setFrozen()'):
+    void    freezeVar (Var v);         // Freeze one variable so it will not be eliminated.
+    void    thaw      ();              // Thaw all frozen variables.
+
+
+    // Solving:
+    //
+    bool    solve       (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+    lbool   solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+    bool    solve       (                     bool do_simp = true, bool turn_off_simp = false);
+    bool    solve       (Lit p       ,        bool do_simp = true, bool turn_off_simp = false);       
+    bool    solve       (Lit p, Lit q,        bool do_simp = true, bool turn_off_simp = false);
+    bool    solve       (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
+    bool    eliminate   (bool turn_off_elim = false);  // Perform variable elimination based simplification. 
+
+    // Memory managment:
+    //
+    virtual void garbageCollect();
+
+
+    // Generate a (possibly simplified) DIMACS file:
+    //
+#if 0
+    void    toDimacs  (const char* file, const vec<Lit>& assumps);
+    void    toDimacs  (const char* file);
+    void    toDimacs  (const char* file, Lit p);
+    void    toDimacs  (const char* file, Lit p, Lit q);
+    void    toDimacs  (const char* file, Lit p, Lit q, Lit r);
+#endif
+
+    // Mode of operation:
+    //
+    int     grow;              // Allow a variable elimination step to grow by a number of clauses (default to zero).
+    int     clause_lim;        // Variables are not eliminated if it produces a resolvent with a length above this limit.
+                               // -1 means no limit.
+    int     subsumption_lim;   // Do not check if subsumption against a clause larger than this. -1 means no limit.
+    double  simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
+
+    bool    use_asymm;         // Shrink clauses by asymmetric branching.
+    bool    use_rcheck;        // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
+    bool    use_elim;          // Perform variable elimination.
+    bool    extend_model;      // Flag to indicate whether the user needs to look at the full model.
+
+    // Statistics:
+    //
+    int     merges;
+    int     asymm_lits;
+    int     eliminated_vars;
+
+ protected:
+
+    // Helper structures:
+    //
+    struct ElimLt {
+        const LMap<int>& n_occ;
+        explicit ElimLt(const LMap<int>& no) : n_occ(no) {}
+
+        // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
+        // 32-bit implementation instead then, but this will have to do for now.
+        uint64_t cost  (Var x)        const { return (uint64_t)n_occ[mkLit(x)] * (uint64_t)n_occ[~mkLit(x)]; }
+        bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
+        
+        // TODO: investigate this order alternative more.
+        // bool operator()(Var x, Var y) const { 
+        //     int c_x = cost(x);
+        //     int c_y = cost(y);
+        //     return c_x < c_y || c_x == c_y && x < y; }
+    };
+
+    struct ClauseDeleted {
+        const ClauseAllocator& ca;
+        explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
+        bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
+
+    // Solver state:
+    //
+    int                 elimorder;
+    bool                use_simplification;
+    Var                 max_simp_var;        // Max variable at the point simplification was turned off.
+    vec<uint32_t>       elimclauses;
+    VMap<char>          touched;
+    OccLists<Var, vec<CRef>, ClauseDeleted>
+                        occurs;
+    LMap<int>           n_occ;
+    Heap<Var,ElimLt>    elim_heap;
+    Queue<CRef>         subsumption_queue;
+    VMap<char>          frozen;
+    vec<Var>            frozen_vars;
+    VMap<char>          eliminated;
+    int                 bwdsub_assigns;
+    int                 n_touched;
+
+    // Temporaries:
+    //
+    CRef                bwdsub_tmpunit;
+
+    // Main internal methods:
+    //
+    lbool         solve_                   (bool do_simp = true, bool turn_off_simp = false);
+    bool          asymm                    (Var v, CRef cr);
+    bool          asymmVar                 (Var v);
+    void          updateElimHeap           (Var v);
+    void          gatherTouchedClauses     ();
+    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
+    bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, int& size);
+    bool          backwardSubsumptionCheck (bool verbose = false);
+    bool          eliminateVar             (Var v);
+    void          extendModel              ();
+
+    void          removeClause             (CRef cr);
+    bool          strengthenClause         (CRef cr, Lit l);
+    bool          implied                  (const vec<Lit>& c);
+    void          relocAll                 (ClauseAllocator& to);
+};
+
+
+//=================================================================================================
+// Implementation of inline methods:
+
+
+inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
+inline void SimpSolver::updateElimHeap(Var v) {
+    assert(use_simplification);
+    // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
+    if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
+        elim_heap.update(v); }
+
+
+inline bool SimpSolver::addClause    (const vec<Lit>& ps)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }
+inline bool SimpSolver::addEmptyClause()                     { add_tmp.clear(); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause    (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause    (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, Lit s){ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); add_tmp.push(s); return addClause_(add_tmp); }
+inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
+
+inline void SimpSolver::freezeVar(Var v){
+    if (!frozen[v]){
+        frozen[v] = 1;
+        frozen_vars.push(v); 
+    } }
+
+inline void SimpSolver::thaw(){
+    for (int i = 0; i < frozen_vars.size(); i++){
+        Var v = frozen_vars[i];
+        frozen[v] = 0;
+        if (use_simplification)
+            updateElimHeap(v);
+    }
+    frozen_vars.clear(); }
+
+inline bool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p       ,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p, Lit q,        bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
+inline bool SimpSolver::solve        (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
+    budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
+
+inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){ 
+    assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Solver.cc b/libs/minisat/Solver.cc
new file mode 100644
index 000000000..ebca294a7
--- /dev/null
+++ b/libs/minisat/Solver.cc
@@ -0,0 +1,1068 @@
+#define __STDC_FORMAT_MACROS
+#define __STDC_LIMIT_MACROS
+/***************************************************************************************[Solver.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 <math.h>
+
+#include "libs/minisat/Alg.h"
+#include "libs/minisat/Sort.h"
+#include "libs/minisat/System.h"
+#include "libs/minisat/Solver.h"
+
+using namespace Minisat;
+
+//=================================================================================================
+// Options:
+
+
+static const char* _cat = "CORE";
+
+static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
+static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
+static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
+static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));
+static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 2, IntRange(0, 2));
+static IntOption     opt_phase_saving      (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
+static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
+static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
+static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 100, IntRange(1, INT32_MAX));
+static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false));
+static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));
+static IntOption     opt_min_learnts_lim   (_cat, "min-learnts", "Minimum learnt clause limit",  0, IntRange(0, INT32_MAX));
+
+
+//=================================================================================================
+// Constructor/Destructor:
+
+
+Solver::Solver() :
+
+    // Parameters (user settable):
+    //
+    verbosity        (0)
+  , var_decay        (opt_var_decay)
+  , clause_decay     (opt_clause_decay)
+  , random_var_freq  (opt_random_var_freq)
+  , random_seed      (opt_random_seed)
+  , luby_restart     (opt_luby_restart)
+  , ccmin_mode       (opt_ccmin_mode)
+  , phase_saving     (opt_phase_saving)
+  , rnd_pol          (false)
+  , rnd_init_act     (opt_rnd_init_act)
+  , garbage_frac     (opt_garbage_frac)
+  , min_learnts_lim  (opt_min_learnts_lim)
+  , restart_first    (opt_restart_first)
+  , restart_inc      (opt_restart_inc)
+
+    // Parameters (the rest):
+    //
+  , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)
+
+    // Parameters (experimental):
+    //
+  , learntsize_adjust_start_confl (100)
+  , learntsize_adjust_inc         (1.5)
+
+    // Statistics: (formerly in 'SolverStats')
+    //
+  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
+  , dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
+
+  , watches            (WatcherDeleted(ca))
+  , order_heap         (VarOrderLt(activity))
+  , ok                 (true)
+  , cla_inc            (1)
+  , var_inc            (1)
+  , qhead              (0)
+  , simpDB_assigns     (-1)
+  , simpDB_props       (0)
+  , progress_estimate  (0)
+  , remove_satisfied   (true)
+  , next_var           (0)
+
+    // Resource constraints:
+    //
+  , conflict_budget    (-1)
+  , propagation_budget (-1)
+  , asynch_interrupt   (false)
+{}
+
+
+Solver::~Solver()
+{
+}
+
+
+//=================================================================================================
+// Minor methods:
+
+
+// Creates a new SAT variable in the solver. If 'decision' 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(lbool upol, bool dvar)
+{
+    Var v;
+    if (free_vars.size() > 0){
+        v = free_vars.last();
+        free_vars.pop();
+    }else
+        v = next_var++;
+
+    watches  .init(mkLit(v, false));
+    watches  .init(mkLit(v, true ));
+    assigns  .insert(v, l_Undef);
+    vardata  .insert(v, mkVarData(CRef_Undef, 0));
+    activity .insert(v, rnd_init_act ? drand(random_seed) * 0.00001 : 0);
+    seen     .insert(v, 0);
+    polarity .insert(v, true);
+    user_pol .insert(v, upol);
+    decision .reserve(v);
+    trail    .capacity(v+1);
+    setDecisionVar(v, dvar);
+    return v;
+}
+
+
+// Note: at the moment, only unassigned variable will be released (this is to avoid duplicate
+// releases of the same variable).
+void Solver::releaseVar(Lit l)
+{
+    if (value(l) == l_Undef){
+        addClause(l);
+        released_vars.push(var(l));
+    }
+}
+
+
+bool Solver::addClause_(vec<Lit>& ps)
+{
+    assert(decisionLevel() == 0);
+    if (!ok) return false;
+
+    // Check if clause is satisfied and remove false/duplicate literals:
+    sort(ps);
+    Lit p; int i, j;
+    for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
+        if (value(ps[i]) == l_True || ps[i] == ~p)
+            return true;
+        else if (value(ps[i]) != l_False && ps[i] != p)
+            ps[j++] = p = ps[i];
+    ps.shrink(i - j);
+
+    if (ps.size() == 0)
+        return ok = false;
+    else if (ps.size() == 1){
+        uncheckedEnqueue(ps[0]);
+        return ok = (propagate() == CRef_Undef);
+    }else{
+        CRef cr = ca.alloc(ps, false);
+        clauses.push(cr);
+        attachClause(cr);
+    }
+
+    return true;
+}
+
+
+void Solver::attachClause(CRef cr){
+    const Clause& c = ca[cr];
+    assert(c.size() > 1);
+    watches[~c[0]].push(Watcher(cr, c[1]));
+    watches[~c[1]].push(Watcher(cr, c[0]));
+    if (c.learnt()) num_learnts++, learnts_literals += c.size();
+    else            num_clauses++, clauses_literals += c.size();
+}
+
+
+void Solver::detachClause(CRef cr, bool strict){
+    const Clause& c = ca[cr];
+    assert(c.size() > 1);
+    
+    // Strict or lazy detaching:
+    if (strict){
+        remove(watches[~c[0]], Watcher(cr, c[1]));
+        remove(watches[~c[1]], Watcher(cr, c[0]));
+    }else{
+        watches.smudge(~c[0]);
+        watches.smudge(~c[1]);
+    }
+
+    if (c.learnt()) num_learnts--, learnts_literals -= c.size();
+    else            num_clauses--, clauses_literals -= c.size();
+}
+
+
+void Solver::removeClause(CRef cr) {
+    Clause& c = ca[cr];
+    detachClause(cr);
+    // Don't leave pointers to free'd memory!
+    if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
+    c.mark(1); 
+    ca.free(cr);
+}
+
+
+bool Solver::satisfied(const Clause& c) const {
+    for (int i = 0; i < c.size(); i++)
+        if (value(c[i]) == l_True)
+            return true;
+    return false; }
+
+
+// Revert to the state at given level (keeping all assignment at 'level' but not beyond).
+//
+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] = l_Undef;
+            if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last()))
+                polarity[x] = sign(trail[c]);
+            insertVarOrder(x); }
+        qhead = trail_lim[level];
+        trail.shrink(trail.size() - trail_lim[level]);
+        trail_lim.shrink(trail_lim.size() - level);
+    } }
+
+
+//=================================================================================================
+// Major methods:
+
+
+Lit Solver::pickBranchLit()
+{
+    Var next = var_Undef;
+
+    // Random decision:
+    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
+        next = order_heap[irand(random_seed,order_heap.size())];
+        if (value(next) == l_Undef && decision[next])
+            rnd_decisions++; }
+
+    // Activity based decision:
+    while (next == var_Undef || value(next) != l_Undef || !decision[next])
+        if (order_heap.empty()){
+            next = var_Undef;
+            break;
+        }else
+            next = order_heap.removeMin();
+
+    // Choose polarity based on different polarity modes (global or per-variable):
+    if (next == var_Undef)
+        return lit_Undef;
+    else if (user_pol[next] != l_Undef)
+        return mkLit(next, user_pol[next] == l_True);
+    else if (rnd_pol)
+        return mkLit(next, drand(random_seed) < 0.5);
+    else
+        return mkLit(next, polarity[next]);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  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'.
+|      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the 
+|        rest of literals. There may be others from the same level though.
+|  
+|________________________________________________________________________________________________@*/
+void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
+{
+    int pathC = 0;
+    Lit p     = lit_Undef;
+
+    // Generate conflict clause:
+    //
+    out_learnt.push();      // (leave room for the asserting literal)
+    int index   = trail.size() - 1;
+
+    do{
+        assert(confl != CRef_Undef); // (otherwise should be UIP)
+        Clause& c = ca[confl];
+
+        if (c.learnt())
+            claBumpActivity(c);
+
+        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
+            Lit q = c[j];
+
+            if (!seen[var(q)] && level(var(q)) > 0){
+                varBumpActivity(var(q));
+                seen[var(q)] = 1;
+                if (level(var(q)) >= decisionLevel())
+                    pathC++;
+                else
+                    out_learnt.push(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;
+
+    // Simplify conflict clause:
+    //
+    int i, j;
+    out_learnt.copyTo(analyze_toclear);
+    if (ccmin_mode == 2){
+        for (i = j = 1; i < out_learnt.size(); i++)
+            if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i]))
+                out_learnt[j++] = out_learnt[i];
+        
+    }else if (ccmin_mode == 1){
+        for (i = j = 1; i < out_learnt.size(); i++){
+            Var x = var(out_learnt[i]);
+
+            if (reason(x) == CRef_Undef)
+                out_learnt[j++] = out_learnt[i];
+            else{
+                Clause& c = ca[reason(var(out_learnt[i]))];
+                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; }
+            }
+        }
+    }else
+        i = j = out_learnt.size();
+
+    max_literals += out_learnt.size();
+    out_learnt.shrink(i - j);
+    tot_literals += out_learnt.size();
+
+    // Find correct backtrack level:
+    //
+    if (out_learnt.size() == 1)
+        out_btlevel = 0;
+    else{
+        int max_i = 1;
+        // Find the first literal assigned at the next-highest level:
+        for (int i = 2; i < out_learnt.size(); i++)
+            if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
+                max_i = i;
+        // Swap-in this literal at index 1:
+        Lit p             = out_learnt[max_i];
+        out_learnt[max_i] = out_learnt[1];
+        out_learnt[1]     = p;
+        out_btlevel       = level(var(p));
+    }
+
+    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 from a conflict clause.
+bool Solver::litRedundant(Lit p)
+{
+    enum { seen_undef = 0, seen_source = 1, seen_removable = 2, seen_failed = 3 };
+    assert(seen[var(p)] == seen_undef || seen[var(p)] == seen_source);
+    assert(reason(var(p)) != CRef_Undef);
+
+    Clause*               c     = &ca[reason(var(p))];
+    vec<ShrinkStackElem>& stack = analyze_stack;
+    stack.clear();
+
+    for (uint32_t i = 1; ; i++){
+        if (i < (uint32_t)c->size()){
+            // Checking 'p'-parents 'l':
+            Lit l = (*c)[i];
+            
+            // Variable at level 0 or previously removable:
+            if (level(var(l)) == 0 || seen[var(l)] == seen_source || seen[var(l)] == seen_removable){
+                continue; }
+            
+            // Check variable can not be removed for some local reason:
+            if (reason(var(l)) == CRef_Undef || seen[var(l)] == seen_failed){
+                stack.push(ShrinkStackElem(0, p));
+                for (int i = 0; i < stack.size(); i++)
+                    if (seen[var(stack[i].l)] == seen_undef){
+                        seen[var(stack[i].l)] = seen_failed;
+                        analyze_toclear.push(stack[i].l);
+                    }
+                    
+                return false;
+            }
+
+            // Recursively check 'l':
+            stack.push(ShrinkStackElem(i, p));
+            i  = 0;
+            p  = l;
+            c  = &ca[reason(var(p))];
+        }else{
+            // Finished with current element 'p' and reason 'c':
+            if (seen[var(p)] == seen_undef){
+                seen[var(p)] = seen_removable;
+                analyze_toclear.push(p);
+            }
+
+            // Terminate with success if stack is empty:
+            if (stack.size() == 0) break;
+            
+            // Continue with top element on stack:
+            i  = stack.last().i;
+            p  = stack.last().l;
+            c  = &ca[reason(var(p))];
+
+            stack.pop();
+        }
+    }
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  analyzeFinal : (p : Lit)  ->  [void]
+|  
+|  Description:
+|    Specialized analysis procedure to express the final conflict in terms of assumptions.
+|    Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
+|    stores the result in 'out_conflict'.
+|________________________________________________________________________________________________@*/
+void Solver::analyzeFinal(Lit p, LSet& out_conflict)
+{
+    out_conflict.clear();
+    out_conflict.insert(p);
+
+    if (decisionLevel() == 0)
+        return;
+
+    seen[var(p)] = 1;
+
+    for (int i = trail.size()-1; i >= trail_lim[0]; i--){
+        Var x = var(trail[i]);
+        if (seen[x]){
+            if (reason(x) == CRef_Undef){
+                assert(level(x) > 0);
+                out_conflict.insert(~trail[i]);
+            }else{
+                Clause& c = ca[reason(x)];
+                for (int j = 1; j < c.size(); j++)
+                    if (level(var(c[j])) > 0)
+                        seen[var(c[j])] = 1;
+            }
+            seen[x] = 0;
+        }
+    }
+
+    seen[var(p)] = 0;
+}
+
+
+void Solver::uncheckedEnqueue(Lit p, CRef from)
+{
+    assert(value(p) == l_Undef);
+    assigns[var(p)] = lbool(!sign(p));
+    vardata[var(p)] = mkVarData(from, decisionLevel());
+    trail.push_(p);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  propagate : [void]  ->  [Clause*]
+|  
+|  Description:
+|    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
+|    otherwise CRef_Undef.
+|  
+|    Post-conditions:
+|      * the propagation queue is empty, even if there was a conflict.
+|________________________________________________________________________________________________@*/
+CRef Solver::propagate()
+{
+    CRef    confl     = CRef_Undef;
+    int     num_props = 0;
+
+    while (qhead < trail.size()){
+        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
+        vec<Watcher>&  ws  = watches.lookup(p);
+        Watcher        *i, *j, *end;
+        num_props++;
+
+        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
+            // Try to avoid inspecting the clause:
+            Lit blocker = i->blocker;
+            if (value(blocker) == l_True){
+                *j++ = *i++; continue; }
+
+            // Make sure the false literal is data[1]:
+            CRef     cr        = i->cref;
+            Clause&  c         = ca[cr];
+            Lit      false_lit = ~p;
+            if (c[0] == false_lit)
+                c[0] = c[1], c[1] = false_lit;
+            assert(c[1] == false_lit);
+            i++;
+
+            // If 0th watch is true, then clause is already satisfied.
+            Lit     first = c[0];
+            Watcher w     = Watcher(cr, first);
+            if (first != blocker && value(first) == l_True){
+                *j++ = w; continue; }
+
+            // 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[~c[1]].push(w);
+                    goto NextClause; }
+
+            // Did not find watch -- clause is unit under assignment:
+            *j++ = w;
+            if (value(first) == l_False){
+                confl = cr;
+                qhead = trail.size();
+                // Copy the remaining watches:
+                while (i < end)
+                    *j++ = *i++;
+            }else
+                uncheckedEnqueue(first, cr);
+
+        NextClause:;
+        }
+        ws.shrink(i - j);
+    }
+    propagations += num_props;
+    simpDB_props -= num_props;
+
+    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 { 
+    ClauseAllocator& ca;
+    reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
+    bool operator () (CRef x, CRef y) { 
+        return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[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(ca));
+    // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
+    // and clauses with activity smaller than 'extra_lim':
+    for (i = j = 0; i < learnts.size(); i++){
+        Clause& c = ca[learnts[i]];
+        if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))
+            removeClause(learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    learnts.shrink(i - j);
+    checkGarbage();
+}
+
+
+void Solver::removeSatisfied(vec<CRef>& cs)
+{
+    int i, j;
+    for (i = j = 0; i < cs.size(); i++){
+        Clause& c = ca[cs[i]];
+        if (satisfied(c))
+            removeClause(cs[i]);
+        else{
+            // Trim clause:
+            assert(value(c[0]) == l_Undef && value(c[1]) == l_Undef);
+            for (int k = 2; k < c.size(); k++)
+                if (value(c[k]) == l_False){
+                    c[k--] = c[c.size()-1];
+                    c.pop();
+                }
+            cs[j++] = cs[i];
+        }
+    }
+    cs.shrink(i - j);
+}
+
+
+void Solver::rebuildOrderHeap()
+{
+    vec<Var> vs;
+    for (Var v = 0; v < nVars(); v++)
+        if (decision[v] && value(v) == l_Undef)
+            vs.push(v);
+    order_heap.build(vs);
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  simplify : [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.
+|________________________________________________________________________________________________@*/
+bool Solver::simplify()
+{
+    assert(decisionLevel() == 0);
+
+    if (!ok || propagate() != CRef_Undef)
+        return ok = false;
+
+    if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
+        return true;
+
+    // Remove satisfied clauses:
+    removeSatisfied(learnts);
+    if (remove_satisfied){       // Can be turned off.
+        removeSatisfied(clauses);
+
+        // TODO: what todo in if 'remove_satisfied' is false?
+
+        // Remove all released variables from the trail:
+        for (int i = 0; i < released_vars.size(); i++){
+            assert(seen[released_vars[i]] == 0);
+            seen[released_vars[i]] = 1;
+        }
+
+        int i, j;
+        for (i = j = 0; i < trail.size(); i++)
+            if (seen[var(trail[i])] == 0)
+                trail[j++] = trail[i];
+        trail.shrink(i - j);
+        //printf("trail.size()= %d, qhead = %d\n", trail.size(), qhead);
+        qhead = trail.size();
+
+        for (int i = 0; i < released_vars.size(); i++)
+            seen[released_vars[i]] = 0;
+
+        // Released variables are now ready to be reused:
+        append(released_vars, free_vars);
+        released_vars.clear();
+    }
+    checkGarbage();
+    rebuildOrderHeap();
+
+    simpDB_assigns = nAssigns();
+    simpDB_props   = clauses_literals + learnts_literals;   // (shouldn't depend on stats really, but it will do for now)
+
+    return true;
+}
+
+
+/*_________________________________________________________________________________________________
+|
+|  search : (nof_conflicts : int) (params : const SearchParams&)  ->  [lbool]
+|  
+|  Description:
+|    Search for a model the specified number of conflicts. 
+|    NOTE! Use negative value for 'nof_conflicts' 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)
+{
+    assert(ok);
+    int         backtrack_level;
+    int         conflictC = 0;
+    vec<Lit>    learnt_clause;
+    starts++;
+
+    for (;;){
+        CRef confl = propagate();
+        if (confl != CRef_Undef){
+            // CONFLICT
+            conflicts++; conflictC++;
+            if (decisionLevel() == 0) return l_False;
+
+            learnt_clause.clear();
+            analyze(confl, learnt_clause, backtrack_level);
+            cancelUntil(backtrack_level);
+
+            if (learnt_clause.size() == 1){
+                uncheckedEnqueue(learnt_clause[0]);
+            }else{
+                CRef cr = ca.alloc(learnt_clause, true);
+                learnts.push(cr);
+                attachClause(cr);
+                claBumpActivity(ca[cr]);
+                uncheckedEnqueue(learnt_clause[0], cr);
+            }
+
+            varDecayActivity();
+            claDecayActivity();
+
+            if (--learntsize_adjust_cnt == 0){
+                learntsize_adjust_confl *= learntsize_adjust_inc;
+                learntsize_adjust_cnt    = (int)learntsize_adjust_confl;
+                max_learnts             *= learntsize_inc;
+
+                if (verbosity >= 1)
+                    printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", 
+                           (int)conflicts, 
+                           (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 
+                           (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
+            }
+
+        }else{
+            // NO CONFLICT
+            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
+                // Reached bound on number of conflicts:
+                progress_estimate = progressEstimate();
+                cancelUntil(0);
+                return l_Undef; }
+
+            // Simplify the set of problem clauses:
+            if (decisionLevel() == 0 && !simplify())
+                return l_False;
+
+            if (learnts.size()-nAssigns() >= max_learnts)
+                // Reduce the set of learnt clauses:
+                reduceDB();
+
+            Lit next = lit_Undef;
+            while (decisionLevel() < assumptions.size()){
+                // Perform user provided assumption:
+                Lit p = assumptions[decisionLevel()];
+                if (value(p) == l_True){
+                    // Dummy decision level:
+                    newDecisionLevel();
+                }else if (value(p) == l_False){
+                    analyzeFinal(~p, conflict);
+                    return l_False;
+                }else{
+                    next = p;
+                    break;
+                }
+            }
+
+            if (next == lit_Undef){
+                // New variable decision:
+                decisions++;
+                next = pickBranchLit();
+
+                if (next == lit_Undef)
+                    // Model found:
+                    return l_True;
+            }
+
+            // Increase decision level and enqueue 'next'
+            newDecisionLevel();
+            uncheckedEnqueue(next);
+        }
+    }
+}
+
+
+double Solver::progressEstimate() const
+{
+    double  progress = 0;
+    double  F = 1.0 / nVars();
+
+    for (int i = 0; i <= decisionLevel(); i++){
+        int beg = i == 0 ? 0 : trail_lim[i - 1];
+        int end = i == decisionLevel() ? trail.size() : trail_lim[i];
+        progress += pow(F, i) * (end - beg);
+    }
+
+    return progress / nVars();
+}
+
+/*
+  Finite subsequences of the Luby-sequence:
+
+  0: 1
+  1: 1 1 2
+  2: 1 1 2 1 1 2 4
+  3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
+  ...
+
+
+ */
+
+static double luby(double y, int x){
+
+    // Find the finite subsequence that contains index 'x', and the
+    // size of that subsequence:
+    int size, seq;
+    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
+
+    while (size-1 != x){
+        size = (size-1)>>1;
+        seq--;
+        x = x % size;
+    }
+
+    return pow(y, seq);
+}
+
+// NOTE: assumptions passed in member-variable 'assumptions'.
+lbool Solver::solve_()
+{
+    model.clear();
+    conflict.clear();
+    if (!ok) return l_False;
+
+    solves++;
+
+    max_learnts = nClauses() * learntsize_factor;
+    if (max_learnts < min_learnts_lim)
+        max_learnts = min_learnts_lim;
+
+    learntsize_adjust_confl   = learntsize_adjust_start_confl;
+    learntsize_adjust_cnt     = (int)learntsize_adjust_confl;
+    lbool   status            = l_Undef;
+
+    if (verbosity >= 1){
+        printf("============================[ Search Statistics ]==============================\n");
+        printf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
+        printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
+        printf("===============================================================================\n");
+    }
+
+    // Search:
+    int curr_restarts = 0;
+    while (status == l_Undef){
+        double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
+        status = search(rest_base * restart_first);
+        if (!withinBudget()) break;
+        curr_restarts++;
+    }
+
+    if (verbosity >= 1)
+        printf("===============================================================================\n");
+
+
+    if (status == l_True){
+        // Extend & copy model:
+        model.growTo(nVars());
+        for (int i = 0; i < nVars(); i++) model[i] = value(i);
+    }else if (status == l_False && conflict.size() == 0)
+        ok = false;
+
+    cancelUntil(0);
+    return status;
+}
+
+
+bool Solver::implies(const vec<Lit>& assumps, vec<Lit>& out)
+{
+    trail_lim.push(trail.size());
+    for (int i = 0; i < assumps.size(); i++){
+        Lit a = assumps[i];
+
+        if (value(a) == l_False){
+            cancelUntil(0);
+            return false;
+        }else if (value(a) == l_Undef)
+            uncheckedEnqueue(a);
+    }
+
+    unsigned trail_before = trail.size();
+    bool     ret          = true;
+    if (propagate() == CRef_Undef){
+        out.clear();
+        for (int j = trail_before; j < trail.size(); j++)
+            out.push(trail[j]);
+    }else
+        ret = false;
+    
+    cancelUntil(0);
+    return ret;
+}
+
+//=================================================================================================
+// Writing CNF to DIMACS:
+// 
+// FIXME: this needs to be rewritten completely.
+
+static Var mapVar(Var x, vec<Var>& map, Var& max)
+{
+    if (map.size() <= x || map[x] == -1){
+        map.growTo(x+1, -1);
+        map[x] = max++;
+    }
+    return map[x];
+}
+
+
+void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
+{
+    if (satisfied(c)) return;
+
+    for (int i = 0; i < c.size(); i++)
+        if (value(c[i]) != l_False)
+            fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
+    fprintf(f, "0\n");
+}
+
+
+void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
+{
+    FILE* f = fopen(file, "wr");
+    if (f == NULL)
+        fprintf(stderr, "could not open file %s\n", file), exit(1);
+    toDimacs(f, assumps);
+    fclose(f);
+}
+
+
+void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
+{
+    // Handle case when solver is in contradictory state:
+    if (!ok){
+        fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
+        return; }
+
+    vec<Var> map; Var max = 0;
+
+    // Cannot use removeClauses here because it is not safe
+    // to deallocate them at this point. Could be improved.
+    int cnt = 0;
+    for (int i = 0; i < clauses.size(); i++)
+        if (!satisfied(ca[clauses[i]]))
+            cnt++;
+        
+    for (int i = 0; i < clauses.size(); i++)
+        if (!satisfied(ca[clauses[i]])){
+            Clause& c = ca[clauses[i]];
+            for (int j = 0; j < c.size(); j++)
+                if (value(c[j]) != l_False)
+                    mapVar(var(c[j]), map, max);
+        }
+
+    // Assumptions are added as unit clauses:
+    cnt += assumps.size();
+
+    fprintf(f, "p cnf %d %d\n", max, cnt);
+
+    for (int i = 0; i < assumps.size(); i++){
+        assert(value(assumps[i]) != l_False);
+        fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1);
+    }
+
+    for (int i = 0; i < clauses.size(); i++)
+        toDimacs(f, ca[clauses[i]], map, max);
+
+    if (verbosity > 0)
+        printf("Wrote DIMACS with %d variables and %d clauses.\n", max, cnt);
+}
+
+
+void Solver::printStats() const
+{
+    double cpu_time = cpuTime();
+    double mem_used = memUsedPeak();
+    printf("restarts              : %"PRIu64"\n", starts);
+    printf("conflicts             : %-12"PRIu64"   (%.0f /sec)\n", conflicts   , conflicts   /cpu_time);
+    printf("decisions             : %-12"PRIu64"   (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions   /cpu_time);
+    printf("propagations          : %-12"PRIu64"   (%.0f /sec)\n", propagations, propagations/cpu_time);
+    printf("conflict literals     : %-12"PRIu64"   (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
+    if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
+    printf("CPU time              : %g s\n", cpu_time);
+}
+
+
+//=================================================================================================
+// Garbage Collection methods:
+
+void Solver::relocAll(ClauseAllocator& to)
+{
+    // All watchers:
+    //
+    watches.cleanAll();
+    for (int v = 0; v < nVars(); v++)
+        for (int s = 0; s < 2; s++){
+            Lit p = mkLit(v, s);
+            vec<Watcher>& ws = watches[p];
+            for (int j = 0; j < ws.size(); j++)
+                ca.reloc(ws[j].cref, to);
+        }
+
+    // All reasons:
+    //
+    for (int i = 0; i < trail.size(); i++){
+        Var v = var(trail[i]);
+
+        // Note: it is not safe to call 'locked()' on a relocated clause. This is why we keep
+        // 'dangling' reasons here. It is safe and does not hurt.
+        if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))){
+            assert(!isRemoved(reason(v)));
+            ca.reloc(vardata[v].reason, to);
+        }
+    }
+
+    // All learnt:
+    //
+    int i, j;
+    for (i = j = 0; i < learnts.size(); i++)
+        if (!isRemoved(learnts[i])){
+            ca.reloc(learnts[i], to);
+            learnts[j++] = learnts[i];
+        }
+    learnts.shrink(i - j);
+
+    // All original:
+    //
+    for (i = j = 0; i < clauses.size(); i++)
+        if (!isRemoved(clauses[i])){
+            ca.reloc(clauses[i], to);
+            clauses[j++] = clauses[i];
+        }
+    clauses.shrink(i - j);
+}
+
+
+void Solver::garbageCollect()
+{
+    // Initialize the next region to a size corresponding to the estimated utilization degree. This
+    // is not precise but should avoid some unnecessary reallocations for the new region:
+    ClauseAllocator to(ca.size() - ca.wasted()); 
+
+    relocAll(to);
+    if (verbosity >= 2)
+        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
+               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+    to.moveTo(ca);
+}
diff --git a/libs/minisat/Solver.h b/libs/minisat/Solver.h
new file mode 100644
index 000000000..73fc7d4cf
--- /dev/null
+++ b/libs/minisat/Solver.h
@@ -0,0 +1,409 @@
+/****************************************************************************************[Solver.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Solver_h
+#define Minisat_Solver_h
+
+#include "libs/minisat/Vec.h"
+#include "libs/minisat/Heap.h"
+#include "libs/minisat/Alg.h"
+#include "libs/minisat/IntMap.h"
+#include "libs/minisat/Options.h"
+#include "libs/minisat/SolverTypes.h"
+
+
+namespace Minisat {
+
+//=================================================================================================
+// Solver -- the main class:
+
+class Solver {
+public:
+
+    // Constructor/Destructor:
+    //
+    Solver();
+    virtual ~Solver();
+
+    // Problem specification:
+    //
+    Var     newVar    (lbool upol = l_Undef, bool dvar = true); // Add a new variable with parameters specifying variable mode.
+    void    releaseVar(Lit l);                                  // Make literal true and promise to never refer to variable again.
+
+    bool    addClause (const vec<Lit>& ps);                     // Add a clause to the solver. 
+    bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.
+    bool    addClause (Lit p);                                  // Add a unit clause to the solver. 
+    bool    addClause (Lit p, Lit q);                           // Add a binary clause to the solver. 
+    bool    addClause (Lit p, Lit q, Lit r);                    // Add a ternary clause to the solver. 
+    bool    addClause (Lit p, Lit q, Lit r, Lit s);             // Add a quaternary clause to the solver. 
+    bool    addClause_(      vec<Lit>& ps);                     // Add a clause to the solver without making superflous internal copy. Will
+                                                                // change the passed vector 'ps'.
+
+    // Solving:
+    //
+    bool    simplify     ();                        // Removes already satisfied clauses.
+    bool    solve        (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
+    lbool   solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
+    bool    solve        ();                        // Search without assumptions.
+    bool    solve        (Lit p);                   // Search for a model that respects a single assumption.
+    bool    solve        (Lit p, Lit q);            // Search for a model that respects two assumptions.
+    bool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
+    bool    okay         () const;                  // FALSE means solver is in a conflicting state
+
+    bool    implies      (const vec<Lit>& assumps, vec<Lit>& out);
+
+    // Iterate over clauses and top-level assignments:
+    ClauseIterator clausesBegin() const;
+    ClauseIterator clausesEnd()   const;
+    TrailIterator  trailBegin()   const;
+    TrailIterator  trailEnd  ()   const;
+
+    void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
+    void    toDimacs     (const char *file, const vec<Lit>& assumps);
+    void    toDimacs     (FILE* f, Clause& c, vec<Var>& map, Var& max);
+
+    // Convenience versions of 'toDimacs()':
+    void    toDimacs     (const char* file);
+    void    toDimacs     (const char* file, Lit p);
+    void    toDimacs     (const char* file, Lit p, Lit q);
+    void    toDimacs     (const char* file, Lit p, Lit q, Lit r);
+    
+    // Variable mode:
+    // 
+    void    setPolarity    (Var v, lbool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
+    void    setDecisionVar (Var v, bool b);  // Declare if a variable should be eligible for selection in the decision heuristic.
+
+    // Read state:
+    //
+    lbool   value      (Var x) const;       // The current value of a variable.
+    lbool   value      (Lit p) const;       // The current value of a literal.
+    lbool   modelValue (Var x) const;       // The value of a variable in the last model. The last call to solve must have been satisfiable.
+    lbool   modelValue (Lit p) const;       // The value of a literal in the last model. The last call to solve must have been satisfiable.
+    int     nAssigns   ()      const;       // The current number of assigned literals.
+    int     nClauses   ()      const;       // The current number of original clauses.
+    int     nLearnts   ()      const;       // The current number of learnt clauses.
+    int     nVars      ()      const;       // The current number of variables.
+    int     nFreeVars  ()      const;
+    void    printStats ()      const;       // Print some current statistics to standard output.
+
+    // Resource contraints:
+    //
+    void    setConfBudget(int64_t x);
+    void    setPropBudget(int64_t x);
+    void    budgetOff();
+    void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
+    void    clearInterrupt();     // Clear interrupt indicator flag.
+
+    // Memory managment:
+    //
+    virtual void garbageCollect();
+    void    checkGarbage(double gf);
+    void    checkGarbage();
+
+    // Extra results: (read-only member variable)
+    //
+    vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
+    LSet       conflict;          // If problem is unsatisfiable (possibly under assumptions),
+                                  // this vector represent the final conflict clause expressed in the assumptions.
+
+    // Mode of operation:
+    //
+    int       verbosity;
+    double    var_decay;
+    double    clause_decay;
+    double    random_var_freq;
+    double    random_seed;
+    bool      luby_restart;
+    int       ccmin_mode;         // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
+    int       phase_saving;       // Controls the level of phase saving (0=none, 1=limited, 2=full).
+    bool      rnd_pol;            // Use random polarities for branching heuristics.
+    bool      rnd_init_act;       // Initialize variable activities with a small random value.
+    double    garbage_frac;       // The fraction of wasted memory allowed before a garbage collection is triggered.
+    int       min_learnts_lim;    // Minimum number to set the learnts limit to.
+
+    int       restart_first;      // The initial restart limit.                                                                (default 100)
+    double    restart_inc;        // The factor with which the restart limit is multiplied in each restart.                    (default 1.5)
+    double    learntsize_factor;  // The intitial limit for learnt clauses is a factor of the original clauses.                (default 1 / 3)
+    double    learntsize_inc;     // The limit for learnt clauses is multiplied with this factor each restart.                 (default 1.1)
+
+    int       learntsize_adjust_start_confl;
+    double    learntsize_adjust_inc;
+
+    // Statistics: (read-only member variable)
+    //
+    uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
+    uint64_t dec_vars, num_clauses, num_learnts, clauses_literals, learnts_literals, max_literals, tot_literals;
+
+protected:
+
+    // Helper structures:
+    //
+    struct VarData { CRef reason; int level; };
+    static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
+
+    struct Watcher {
+        CRef cref;
+        Lit  blocker;
+        Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
+        bool operator==(const Watcher& w) const { return cref == w.cref; }
+        bool operator!=(const Watcher& w) const { return cref != w.cref; }
+    };
+
+    struct WatcherDeleted
+    {
+        const ClauseAllocator& ca;
+        WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
+        bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
+    };
+
+    struct VarOrderLt {
+        const IntMap<Var, double>&  activity;
+        bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
+        VarOrderLt(const IntMap<Var, double>&  act) : activity(act) { }
+    };
+
+    struct ShrinkStackElem {
+        uint32_t i;
+        Lit      l;
+        ShrinkStackElem(uint32_t _i, Lit _l) : i(_i), l(_l){}
+    };
+
+    // Solver state:
+    //
+    vec<CRef>           clauses;          // List of problem clauses.
+    vec<CRef>           learnts;          // List of learnt clauses.
+    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<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
+
+    VMap<double>        activity;         // A heuristic measurement of the activity of a variable.
+    VMap<lbool>         assigns;          // The current assignments.
+    VMap<char>          polarity;         // The preferred polarity of each variable.
+    VMap<lbool>         user_pol;         // The users preferred polarity of each variable.
+    VMap<char>          decision;         // Declares if a variable is eligible for selection in the decision heuristic.
+    VMap<VarData>       vardata;          // Stores reason and level for each variable.
+    OccLists<Lit, vec<Watcher>, WatcherDeleted, MkIndexLit>
+                        watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+
+    Heap<Var,VarOrderLt>order_heap;       // A priority queue of variables ordered with respect to the variable activity.
+
+    bool                ok;               // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
+    double              cla_inc;          // Amount to bump next clause with.
+    double              var_inc;          // Amount to bump next variable with.
+    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 'simplify()'.
+    int64_t             simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplify()'.
+    double              progress_estimate;// Set by 'search()'.
+    bool                remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
+    Var                 next_var;         // Next variable to be created.
+    ClauseAllocator     ca;
+
+    vec<Var>            released_vars;
+    vec<Var>            free_vars;
+
+    // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
+    // used, exept 'seen' wich is used in several places.
+    //
+    VMap<char>          seen;
+    vec<ShrinkStackElem>analyze_stack;
+    vec<Lit>            analyze_toclear;
+    vec<Lit>            add_tmp;
+
+    double              max_learnts;
+    double              learntsize_adjust_confl;
+    int                 learntsize_adjust_cnt;
+
+    // Resource contraints:
+    //
+    int64_t             conflict_budget;    // -1 means no budget.
+    int64_t             propagation_budget; // -1 means no budget.
+    bool                asynch_interrupt;
+
+    // Main internal methods:
+    //
+    void     insertVarOrder   (Var x);                                                 // Insert a variable in the decision order priority queue.
+    Lit      pickBranchLit    ();                                                      // Return the next decision variable.
+    void     newDecisionLevel ();                                                      // Begins a new decision level.
+    void     uncheckedEnqueue (Lit p, CRef from = CRef_Undef);                         // Enqueue a literal. Assumes value of literal is undefined.
+    bool     enqueue          (Lit p, CRef from = CRef_Undef);                         // Test if fact 'p' contradicts current state, enqueue otherwise.
+    CRef     propagate        ();                                                      // Perform unit propagation. Returns possibly conflicting clause.
+    void     cancelUntil      (int level);                                             // Backtrack until a certain level.
+    void     analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel);    // (bt = backtrack)
+    void     analyzeFinal     (Lit p, LSet& out_conflict);                             // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
+    bool     litRedundant     (Lit p);                                                 // (helper method for 'analyze()')
+    lbool    search           (int nof_conflicts);                                     // Search for a given number of conflicts.
+    lbool    solve_           ();                                                      // Main solve method (assumptions given in 'assumptions').
+    void     reduceDB         ();                                                      // Reduce the set of learnt clauses.
+    void     removeSatisfied  (vec<CRef>& cs);                                         // Shrink 'cs' to contain only non-satisfied clauses.
+    void     rebuildOrderHeap ();
+
+    // Maintaining Variable/Clause activity:
+    //
+    void     varDecayActivity ();                      // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
+    void     varBumpActivity  (Var v, double inc);     // Increase a variable with the current 'bump' value.
+    void     varBumpActivity  (Var v);                 // Increase a variable with the current 'bump' value.
+    void     claDecayActivity ();                      // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
+    void     claBumpActivity  (Clause& c);             // Increase a clause with the current 'bump' value.
+
+    // Operations on clauses:
+    //
+    void     attachClause     (CRef cr);               // Attach a clause to watcher lists.
+    void     detachClause     (CRef cr, bool strict = false); // Detach a clause to watcher lists.
+    void     removeClause     (CRef cr);               // Detach and free a clause.
+    bool     isRemoved        (CRef cr) const;         // Test if a clause has been removed.
+    bool     locked           (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
+    bool     satisfied        (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
+
+    // Misc:
+    //
+    int      decisionLevel    ()      const; // Gives the current decisionlevel.
+    uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
+    CRef     reason           (Var x) const;
+    int      level            (Var x) const;
+    double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
+    bool     withinBudget     ()      const;
+    void     relocAll         (ClauseAllocator& to);
+
+    // Static helpers:
+    //
+
+    // 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); }
+};
+
+
+//=================================================================================================
+// Implementation of inline methods:
+
+inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
+inline int  Solver::level (Var x) const { return vardata[x].level; }
+
+inline void Solver::insertVarOrder(Var x) {
+    if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
+
+inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
+inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
+inline void Solver::varBumpActivity(Var v, double inc) {
+    if ( (activity[v] += inc) > 1e100 ) {
+        // Rescale:
+        for (int i = 0; i < nVars(); i++)
+            activity[i] *= 1e-100;
+        var_inc *= 1e-100; }
+
+    // Update order_heap with respect to new activity:
+    if (order_heap.inHeap(v))
+        order_heap.decrease(v); }
+
+inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
+inline void Solver::claBumpActivity (Clause& c) {
+        if ( (c.activity() += cla_inc) > 1e20 ) {
+            // Rescale:
+            for (int i = 0; i < learnts.size(); i++)
+                ca[learnts[i]].activity() *= 1e-20;
+            cla_inc *= 1e-20; } }
+
+inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
+inline void Solver::checkGarbage(double gf){
+    if (ca.wasted() > ca.size() * gf)
+        garbageCollect(); }
+
+// NOTE: enqueue does not set the ok flag! (only public methods do)
+inline bool     Solver::enqueue         (Lit p, CRef from)      { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
+inline bool     Solver::addClause       (const vec<Lit>& ps)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }
+inline bool     Solver::addEmptyClause  ()                      { add_tmp.clear(); return addClause_(add_tmp); }
+inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
+inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
+inline bool     Solver::addClause       (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline bool     Solver::addClause       (Lit p, Lit q, Lit r, Lit s){ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); add_tmp.push(s); return addClause_(add_tmp); }
+
+inline bool     Solver::isRemoved       (CRef cr)         const { return ca[cr].mark() == 1; }
+inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
+
+inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
+inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
+inline lbool    Solver::value         (Var x) const   { return assigns[x]; }
+inline lbool    Solver::value         (Lit p) const   { return assigns[var(p)] ^ sign(p); }
+inline lbool    Solver::modelValue    (Var x) const   { return model[x]; }
+inline lbool    Solver::modelValue    (Lit p) const   { return model[var(p)] ^ sign(p); }
+inline int      Solver::nAssigns      ()      const   { return trail.size(); }
+inline int      Solver::nClauses      ()      const   { return num_clauses; }
+inline int      Solver::nLearnts      ()      const   { return num_learnts; }
+inline int      Solver::nVars         ()      const   { return next_var; }
+// TODO: nFreeVars() is not quite correct, try to calculate right instead of adapting it like below:
+inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
+inline void     Solver::setPolarity   (Var v, lbool b){ user_pol[v] = b; }
+inline void     Solver::setDecisionVar(Var v, bool b) 
+{ 
+    if      ( b && !decision[v]) dec_vars++;
+    else if (!b &&  decision[v]) dec_vars--;
+
+    decision[v] = b;
+    insertVarOrder(v);
+}
+inline void     Solver::setConfBudget(int64_t x){ conflict_budget    = conflicts    + x; }
+inline void     Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
+inline void     Solver::interrupt(){ asynch_interrupt = true; }
+inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
+inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
+inline bool     Solver::withinBudget() const {
+    return !asynch_interrupt &&
+           (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
+           (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
+
+// FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
+// pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
+// all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
+inline bool     Solver::solve         ()                    { budgetOff(); assumptions.clear(); return solve_() == l_True; }
+inline bool     Solver::solve         (Lit p)               { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
+inline bool     Solver::solve         (Lit p, Lit q)        { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
+inline bool     Solver::solve         (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }
+inline bool     Solver::solve         (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
+inline lbool    Solver::solveLimited  (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
+inline bool     Solver::okay          ()      const   { return ok; }
+
+inline ClauseIterator Solver::clausesBegin() const { return ClauseIterator(ca, &clauses[0]); }
+inline ClauseIterator Solver::clausesEnd  () const { return ClauseIterator(ca, &clauses[clauses.size()]); }
+inline TrailIterator  Solver::trailBegin  () const { return TrailIterator(&trail[0]); }
+inline TrailIterator  Solver::trailEnd    () const { 
+    return TrailIterator(&trail[decisionLevel() == 0 ? trail.size() : trail_lim[0]]); }
+
+inline void     Solver::toDimacs     (const char* file){ vec<Lit> as; toDimacs(file, as); }
+inline void     Solver::toDimacs     (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
+inline void     Solver::toDimacs     (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
+inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
+
+
+//=================================================================================================
+// Debug etc:
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/SolverTypes.h b/libs/minisat/SolverTypes.h
new file mode 100644
index 000000000..be40a4c37
--- /dev/null
+++ b/libs/minisat/SolverTypes.h
@@ -0,0 +1,478 @@
+/***********************************************************************************[SolverTypes.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_SolverTypes_h
+#define Minisat_SolverTypes_h
+
+#include <assert.h>
+
+#include "libs/minisat/IntTypes.h"
+#include "libs/minisat/Alg.h"
+#include "libs/minisat/Vec.h"
+#include "libs/minisat/IntMap.h"
+#include "libs/minisat/Map.h"
+#include "libs/minisat/Alloc.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Variables, literals, lifted booleans, clauses:
+
+
+// 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;
+#if defined(MINISAT_CONSTANTS_AS_MACROS)
+#define var_Undef (-1)
+#else
+  const Var var_Undef = -1;
+#endif
+
+
+struct Lit {
+    int     x;
+
+    // Use this as a constructor:
+    friend Lit mkLit(Var var, bool sign = false);
+
+    bool operator == (Lit p) const { return x == p.x; }
+    bool operator != (Lit p) const { return x != p.x; }
+    bool operator <  (Lit p) const { return x < p.x;  } // '<' makes p, ~p adjacent in the ordering.
+};
+
+
+inline  Lit  mkLit     (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
+inline  Lit  operator ~(Lit p)              { Lit q; q.x = p.x ^ 1; return q; }
+inline  Lit  operator ^(Lit p, bool b)      { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
+inline  bool sign      (Lit p)              { return p.x & 1; }
+inline  int  var       (Lit p)              { return p.x >> 1; }
+
+// Mapping Literals to and from compact integers suitable for array indexing:
+inline  int  toInt     (Var v)              { return v; } 
+inline  int  toInt     (Lit p)              { return p.x; } 
+inline  Lit  toLit     (int i)              { Lit p; p.x = i; return p; } 
+
+//const Lit lit_Undef = mkLit(var_Undef, false);  // }- Useful special constants.
+//const Lit lit_Error = mkLit(var_Undef, true );  // }
+
+const Lit lit_Undef = { -2 };  // }- Useful special constants.
+const Lit lit_Error = { -1 };  // }
+
+struct MkIndexLit { vec<Lit>::Size operator()(Lit l) const { return vec<Lit>::Size(l.x); } };
+
+template<class T> class VMap : public IntMap<Var, T>{};
+template<class T> class LMap : public IntMap<Lit, T, MkIndexLit>{};
+class LSet : public IntSet<Lit, MkIndexLit>{};
+
+//=================================================================================================
+// Lifted booleans:
+//
+// NOTE: this implementation is optimized for the case when comparisons between values are mostly
+//       between one variable and one constant. Some care had to be taken to make sure that gcc 
+//       does enough constant propagation to produce sensible code, and this appears to be somewhat
+//       fragile unfortunately.
+
+class lbool {
+    uint8_t value;
+
+public:
+    explicit lbool(uint8_t v) : value(v) { }
+
+    lbool()       : value(0) { }
+    explicit lbool(bool x) : value(!x) { }
+
+    bool  operator == (lbool b) const { return ((b.value&2) & (value&2)) | (!(b.value&2)&(value == b.value)); }
+    bool  operator != (lbool b) const { return !(*this == b); }
+    lbool operator ^  (bool  b) const { return lbool((uint8_t)(value^(uint8_t)b)); }
+
+    lbool operator && (lbool b) const { 
+        uint8_t sel = (this->value << 1) | (b.value << 3);
+        uint8_t v   = (0xF7F755F4 >> sel) & 3;
+        return lbool(v); }
+
+    lbool operator || (lbool b) const {
+        uint8_t sel = (this->value << 1) | (b.value << 3);
+        uint8_t v   = (0xFCFCF400 >> sel) & 3;
+        return lbool(v); }
+
+    friend int   toInt  (lbool l);
+    friend lbool toLbool(int   v);
+};
+inline int   toInt  (lbool l) { return l.value; }
+inline lbool toLbool(int   v) { return lbool((uint8_t)v);  }
+
+#if defined(MINISAT_CONSTANTS_AS_MACROS)
+  #define l_True  (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
+  #define l_False (lbool((uint8_t)1))
+  #define l_Undef (lbool((uint8_t)2))
+#else
+  const lbool l_True ((uint8_t)0);
+  const lbool l_False((uint8_t)1);
+  const lbool l_Undef((uint8_t)2);
+#endif
+
+
+//=================================================================================================
+// Clause -- a simple class for representing a clause:
+
+class Clause;
+typedef RegionAllocator<uint32_t>::Ref CRef;
+
+class Clause {
+    struct {
+        unsigned mark      : 2;
+        unsigned learnt    : 1;
+        unsigned has_extra : 1;
+        unsigned reloced   : 1;
+        unsigned size      : 27; }                        header;
+    union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
+
+    friend class ClauseAllocator;
+
+    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+    Clause(const vec<Lit>& ps, bool use_extra, bool learnt) {
+        header.mark      = 0;
+        header.learnt    = learnt;
+        header.has_extra = use_extra;
+        header.reloced   = 0;
+        header.size      = ps.size();
+
+        for (int i = 0; i < ps.size(); i++) 
+            data[i].lit = ps[i];
+
+        if (header.has_extra){
+            if (header.learnt)
+                data[header.size].act = 0;
+            else
+                calcAbstraction();
+    }
+    }
+
+    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+    Clause(const Clause& from, bool use_extra){
+        header           = from.header;
+        header.has_extra = use_extra;   // NOTE: the copied clause may lose the extra field.
+
+        for (int i = 0; i < from.size(); i++)
+            data[i].lit = from[i];
+
+        if (header.has_extra){
+            if (header.learnt)
+                data[header.size].act = from.data[header.size].act;
+            else 
+                data[header.size].abs = from.data[header.size].abs;
+    }
+    }
+
+public:
+    void calcAbstraction() {
+        assert(header.has_extra);
+        uint32_t abstraction = 0;
+        for (int i = 0; i < size(); i++)
+            abstraction |= 1 << (var(data[i].lit) & 31);
+        data[header.size].abs = abstraction;  }
+
+
+    int          size        ()      const   { return header.size; }
+    void         shrink      (int i)         { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
+    void         pop         ()              { shrink(1); }
+    bool         learnt      ()      const   { return header.learnt; }
+    bool         has_extra   ()      const   { return header.has_extra; }
+    uint32_t     mark        ()      const   { return header.mark; }
+    void         mark        (uint32_t m)    { header.mark = m; }
+    const Lit&   last        ()      const   { return data[header.size-1].lit; }
+
+    bool         reloced     ()      const   { return header.reloced; }
+    CRef         relocation  ()      const   { return data[0].rel; }
+    void         relocate    (CRef c)        { header.reloced = 1; data[0].rel = c; }
+
+    // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
+    //       subsumption operations to behave correctly.
+    Lit&         operator [] (int i)         { return data[i].lit; }
+    Lit          operator [] (int i) const   { return data[i].lit; }
+    operator const Lit* (void) const         { return (Lit*)data; }
+
+    float&       activity    ()              { assert(header.has_extra); return data[header.size].act; }
+    uint32_t     abstraction () const        { assert(header.has_extra); return data[header.size].abs; }
+
+    Lit          subsumes    (const Clause& other) const;
+    void         strengthen  (Lit p);
+};
+
+
+//=================================================================================================
+// ClauseAllocator -- a simple class for allocating memory for clauses:
+
+const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;
+class ClauseAllocator
+{
+    RegionAllocator<uint32_t> ra;
+
+    static uint32_t clauseWord32Size(int size, bool has_extra){
+        return (sizeof(Clause) + (sizeof(Lit) * (size + (int)has_extra))) / sizeof(uint32_t); }
+
+ public:
+    enum { Unit_Size = RegionAllocator<uint32_t>::Unit_Size };
+
+    bool extra_clause_field;
+
+    ClauseAllocator(uint32_t start_cap) : ra(start_cap), extra_clause_field(false){}
+    ClauseAllocator() : extra_clause_field(false){}
+
+    void moveTo(ClauseAllocator& to){
+        to.extra_clause_field = extra_clause_field;
+        ra.moveTo(to.ra); }
+
+    CRef alloc(const vec<Lit>& ps, bool learnt = false)
+    {
+        assert(sizeof(Lit)      == sizeof(uint32_t));
+        assert(sizeof(float)    == sizeof(uint32_t));
+        bool use_extra = learnt | extra_clause_field;
+        CRef cid       = ra.alloc(clauseWord32Size(ps.size(), use_extra));
+        new (lea(cid)) Clause(ps, use_extra, learnt);
+
+        return cid;
+    }
+
+    CRef alloc(const Clause& from)
+    {
+        bool use_extra = from.learnt() | extra_clause_field;
+        CRef cid       = ra.alloc(clauseWord32Size(from.size(), use_extra));
+        new (lea(cid)) Clause(from, use_extra);
+        return cid; }
+
+    uint32_t size      () const      { return ra.size(); }
+    uint32_t wasted    () const      { return ra.wasted(); }
+
+    // Deref, Load Effective Address (LEA), Inverse of LEA (AEL):
+    Clause&       operator[](CRef r)         { return (Clause&)ra[r]; }
+    const Clause& operator[](CRef r) const   { return (Clause&)ra[r]; }
+    Clause*       lea       (CRef r)         { return (Clause*)ra.lea(r); }
+    const Clause* lea       (CRef r) const   { return (Clause*)ra.lea(r);; }
+    CRef          ael       (const Clause* t){ return ra.ael((uint32_t*)t); }
+
+    void free(CRef cid)
+    {
+        Clause& c = operator[](cid);
+        ra.free(clauseWord32Size(c.size(), c.has_extra()));
+    }
+
+    void reloc(CRef& cr, ClauseAllocator& to)
+    {
+        Clause& c = operator[](cr);
+        
+        if (c.reloced()) { cr = c.relocation(); return; }
+        
+        cr = to.alloc(c);
+        c.relocate(cr);
+    }
+};
+
+//=================================================================================================
+// Simple iterator classes (for iterating over clauses and top-level assignments):
+
+class ClauseIterator {
+    const ClauseAllocator& ca;
+    const CRef*            crefs;
+public:
+    ClauseIterator(const ClauseAllocator& _ca, const CRef* _crefs) : ca(_ca), crefs(_crefs){}
+
+    void operator++(){ crefs++; }
+    const Clause& operator*() const { return ca[*crefs]; }
+
+    // NOTE: does not compare that references use the same clause-allocator:
+    bool operator==(const ClauseIterator& ci) const { return crefs == ci.crefs; }
+    bool operator!=(const ClauseIterator& ci) const { return crefs != ci.crefs; }
+};
+
+
+class TrailIterator {
+    const Lit* lits;
+public:
+    TrailIterator(const Lit* _lits) : lits(_lits){}
+
+    void operator++()   { lits++; }
+    Lit  operator*() const { return *lits; }
+
+    bool operator==(const TrailIterator& ti) const { return lits == ti.lits; }
+    bool operator!=(const TrailIterator& ti) const { return lits != ti.lits; }
+};
+
+
+//=================================================================================================
+// OccLists -- a class for maintaining occurence lists with lazy deletion:
+
+template<class K, class Vec, class Deleted, class MkIndex = MkIndexDefault<K> >
+class OccLists
+{
+    IntMap<K, Vec,  MkIndex> occs;
+    IntMap<K, char, MkIndex> dirty;
+    vec<K>                   dirties;
+    Deleted                  deleted;
+
+ public:
+    OccLists(const Deleted& d, MkIndex _index = MkIndex()) :
+        occs(_index), 
+        dirty(_index), 
+        deleted(d){}
+    
+    void  init      (const K& idx){ occs.reserve(idx); occs[idx].clear(); dirty.reserve(idx, 0); }
+    Vec&  operator[](const K& idx){ return occs[idx]; }
+    Vec&  lookup    (const K& idx){ if (dirty[idx]) clean(idx); return occs[idx]; }
+
+    void  cleanAll  ();
+    void  clean     (const K& idx);
+    void  smudge    (const K& idx){
+        if (dirty[idx] == 0){
+            dirty[idx] = 1;
+            dirties.push(idx);
+        }
+    }
+
+    void  clear(bool free = true){
+        occs   .clear(free);
+        dirty  .clear(free);
+        dirties.clear(free);
+    }
+};
+
+
+template<class K, class Vec, class Deleted, class MkIndex>
+void OccLists<K,Vec,Deleted,MkIndex>::cleanAll()
+{
+    for (int i = 0; i < dirties.size(); i++)
+        // Dirties may contain duplicates so check here if a variable is already cleaned:
+        if (dirty[dirties[i]])
+            clean(dirties[i]);
+    dirties.clear();
+}
+
+
+template<class K, class Vec, class Deleted, class MkIndex>
+void OccLists<K,Vec,Deleted,MkIndex>::clean(const K& idx)
+{
+    Vec& vec = occs[idx];
+    int  i, j;
+    for (i = j = 0; i < vec.size(); i++)
+        if (!deleted(vec[i]))
+            vec[j++] = vec[i];
+    vec.shrink(i - j);
+    dirty[idx] = 0;
+}
+
+
+//=================================================================================================
+// CMap -- a class for mapping clauses to values:
+
+
+template<class T>
+class CMap
+{
+    struct CRefHash {
+        uint32_t operator()(CRef cr) const { return (uint32_t)cr; } };
+
+    typedef Map<CRef, T, CRefHash> HashTable;
+    HashTable map;
+        
+ public:
+    // Size-operations:
+    void     clear       ()                           { map.clear(); }
+    int      size        ()                const      { return map.elems(); }
+
+    
+    // Insert/Remove/Test mapping:
+    void     insert      (CRef cr, const T& t){ map.insert(cr, t); }
+    void     growTo      (CRef cr, const T& t){ map.insert(cr, t); } // NOTE: for compatibility
+    void     remove      (CRef cr)            { map.remove(cr); }
+    bool     has         (CRef cr, T& t)      { return map.peek(cr, t); }
+
+    // Vector interface (the clause 'c' must already exist):
+    const T& operator [] (CRef cr) const      { return map[cr]; }
+    T&       operator [] (CRef cr)            { return map[cr]; }
+
+    // Iteration (not transparent at all at the moment):
+    int  bucket_count() const { return map.bucket_count(); }
+    const vec<typename HashTable::Pair>& bucket(int i) const { return map.bucket(i); }
+
+    // Move contents to other map:
+    void moveTo(CMap& other){ map.moveTo(other.map); }
+
+    // TMP debug:
+    void debug(){
+        printf(" --- size = %d, bucket_count = %d\n", size(), map.bucket_count()); }
+};
+
+
+/*_________________________________________________________________________________________________
+|
+|  subsumes : (other : const Clause&)  ->  Lit
+|  
+|  Description:
+|       Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other'
+|       by subsumption resolution.
+|  
+|    Result:
+|       lit_Error  - No subsumption or simplification
+|       lit_Undef  - Clause subsumes 'other'
+|       p          - The literal p can be deleted from 'other'
+|________________________________________________________________________________________________@*/
+inline Lit Clause::subsumes(const Clause& other) const
+{
+    //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
+    //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
+    assert(!header.learnt);   assert(!other.header.learnt);
+    assert(header.has_extra); assert(other.header.has_extra);
+    if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
+        return lit_Error;
+
+    Lit        ret = lit_Undef;
+    const Lit* c   = (const Lit*)(*this);
+    const Lit* d   = (const Lit*)other;
+
+    for (unsigned i = 0; i < header.size; i++) {
+        // search for c[i] or ~c[i]
+        for (unsigned j = 0; j < other.header.size; j++)
+            if (c[i] == d[j])
+                goto ok;
+            else if (ret == lit_Undef && c[i] == ~d[j]){
+                ret = c[i];
+                goto ok;
+            }
+
+        // did not find it
+        return lit_Error;
+    ok:;
+    }
+
+    return ret;
+}
+
+inline void Clause::strengthen(Lit p)
+{
+    remove(*this, p);
+    calcAbstraction();
+}
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/Sort.h b/libs/minisat/Sort.h
new file mode 100644
index 000000000..4a25a9b49
--- /dev/null
+++ b/libs/minisat/Sort.h
@@ -0,0 +1,98 @@
+/******************************************************************************************[Sort.h]
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Sort_h
+#define Minisat_Sort_h
+
+#include "libs/minisat/Vec.h"
+
+//=================================================================================================
+// Some sorting algorithms for vec's
+
+
+namespace Minisat {
+
+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)
+{
+    if (size <= 15)
+        selectionSort(array, size, lt);
+
+    else{
+        T           pivot = array[size / 2];
+        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);
+        sort(&array[i], size-i, lt);
+    }
+}
+template <class T> static inline void sort(T* array, int size) {
+    sort(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>()); }
+
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/System.cc b/libs/minisat/System.cc
new file mode 100644
index 000000000..01d0dfe11
--- /dev/null
+++ b/libs/minisat/System.cc
@@ -0,0 +1,171 @@
+#define __STDC_FORMAT_MACROS
+#define __STDC_LIMIT_MACROS
+/***************************************************************************************[System.cc]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 <signal.h>
+#include <stdio.h>
+
+#include "libs/minisat/System.h"
+
+#if defined(__linux__)
+
+#include <stdlib.h>
+
+using namespace Minisat;
+
+static inline int memReadStat(int field)
+{
+    char  name[256];
+    pid_t pid = getpid();
+    int   value;
+
+    sprintf(name, "/proc/%d/statm", pid);
+    FILE* in = fopen(name, "rb");
+    if (in == NULL) return 0;
+
+    for (; field >= 0; field--)
+        if (fscanf(in, "%d", &value) != 1)
+            printf("ERROR! Failed to parse memory statistics from \"/proc\".\n"), exit(1);
+    fclose(in);
+    return value;
+}
+
+
+static inline int memReadPeak(void)
+{
+    char  name[256];
+    pid_t pid = getpid();
+
+    sprintf(name, "/proc/%d/status", pid);
+    FILE* in = fopen(name, "rb");
+    if (in == NULL) return 0;
+
+    // Find the correct line, beginning with "VmPeak:":
+    int peak_kb = 0;
+    while (!feof(in) && fscanf(in, "VmPeak: %d kB", &peak_kb) != 1)
+        while (!feof(in) && fgetc(in) != '\n')
+            ;
+    fclose(in);
+
+    return peak_kb;
+}
+
+double Minisat::memUsed() { return (double)memReadStat(0) * (double)getpagesize() / (1024*1024); }
+double Minisat::memUsedPeak(bool strictlyPeak) { 
+    double peak = memReadPeak() / (double)1024;
+    return peak == 0 && !strictlyPeak ? memUsed() : peak; }
+
+#elif defined(__FreeBSD__) || defined(__FreeBSD_kernel__) || defined(__gnu_hurd__)
+
+double Minisat::memUsed() {
+    struct rusage ru;
+    getrusage(RUSAGE_SELF, &ru);
+    return (double)ru.ru_maxrss / 1024; }
+double Minisat::memUsedPeak() { return memUsed(); }
+
+
+#elif defined(__APPLE__)
+#include <malloc/malloc.h>
+
+double Minisat::memUsed() {
+    malloc_statistics_t t;
+    malloc_zone_statistics(NULL, &t);
+    return (double)t.max_size_in_use / (1024*1024); }
+double Minisat::memUsedPeak() { return memUsed(); }
+
+#else
+double Minisat::memUsed()     { return 0; }
+double Minisat::memUsedPeak() { return 0; }
+#endif
+
+
+void Minisat::setX86FPUPrecision()
+{
+#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
+    // Only correct FPU precision on Linux architectures that needs and supports it:
+    fpu_control_t oldcw, newcw;
+    _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
+    printf("WARNING: for repeatability, setting FPU to use double precision\n");
+#endif
+}
+
+
+#if !defined(_MSC_VER) && !defined(__MINGW32__)
+void Minisat::limitMemory(uint64_t max_mem_mb)
+{
+// FIXME: OpenBSD does not support RLIMIT_AS. Not sure how well RLIMIT_DATA works instead.
+#if defined(__OpenBSD__)
+#define RLIMIT_AS RLIMIT_DATA
+#endif
+
+    // Set limit on virtual memory:
+    if (max_mem_mb != 0){
+        rlim_t new_mem_lim = (rlim_t)max_mem_mb * 1024*1024;
+        rlimit rl;
+        getrlimit(RLIMIT_AS, &rl);
+        if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
+            rl.rlim_cur = new_mem_lim;
+            if (setrlimit(RLIMIT_AS, &rl) == -1)
+                printf("WARNING! Could not set resource limit: Virtual memory.\n");
+        }
+    }
+
+#if defined(__OpenBSD__)
+#undef RLIMIT_AS
+#endif
+}
+#else
+void Minisat::limitMemory(uint64_t /*max_mem_mb*/)
+{
+    printf("WARNING! Memory limit not supported on this architecture.\n");
+}
+#endif
+
+
+#if !defined(_MSC_VER) && !defined(__MINGW32__)
+void Minisat::limitTime(uint32_t max_cpu_time)
+{
+    if (max_cpu_time != 0){
+        rlimit rl;
+        getrlimit(RLIMIT_CPU, &rl);
+        if (rl.rlim_max == RLIM_INFINITY || (rlim_t)max_cpu_time < rl.rlim_max){
+            rl.rlim_cur = max_cpu_time;
+            if (setrlimit(RLIMIT_CPU, &rl) == -1)
+                printf("WARNING! Could not set resource limit: CPU-time.\n");
+        }
+    }
+}
+#else
+void Minisat::limitTime(uint32_t /*max_cpu_time*/)
+{
+    printf("WARNING! CPU-time limit not supported on this architecture.\n");
+}
+#endif
+
+
+void Minisat::sigTerm(void handler(int))
+{
+    signal(SIGINT, handler);
+    signal(SIGTERM,handler);
+#ifdef SIGXCPU
+    signal(SIGXCPU,handler);
+#endif
+}
diff --git a/libs/minisat/System.h b/libs/minisat/System.h
new file mode 100644
index 000000000..eb8a7e4d3
--- /dev/null
+++ b/libs/minisat/System.h
@@ -0,0 +1,72 @@
+/****************************************************************************************[System.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_System_h
+#define Minisat_System_h
+
+#if defined(__linux__)
+#include <fpu_control.h>
+#endif
+
+#include "libs/minisat/IntTypes.h"
+
+//-------------------------------------------------------------------------------------------------
+
+namespace Minisat {
+
+static inline double cpuTime(void); // CPU-time in seconds.
+
+extern double memUsed();            // Memory in mega bytes (returns 0 for unsupported architectures).
+extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures).
+
+extern void   setX86FPUPrecision(); // Make sure double's are represented with the same precision
+                                    // in memory and registers.
+
+extern void   limitMemory(uint64_t max_mem_mb); // Set a limit on total memory usage. The exact
+                                                // semantics varies depending on architecture.
+
+extern void   limitTime(uint32_t max_cpu_time); // Set a limit on maximum CPU time. The exact
+                                                // semantics varies depending on architecture.
+
+extern void   sigTerm(void handler(int));      // Set up handling of available termination signals.
+
+}
+
+//-------------------------------------------------------------------------------------------------
+// Implementation of inline functions:
+
+#if defined(_MSC_VER) || defined(__MINGW32__)
+#include <time.h>
+
+static inline double Minisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
+
+#else
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <unistd.h>
+
+static inline double Minisat::cpuTime(void) {
+    struct rusage ru;
+    getrusage(RUSAGE_SELF, &ru);
+    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
+
+#endif
+
+#endif
diff --git a/libs/minisat/UPDATE.sh b/libs/minisat/UPDATE.sh
new file mode 100644
index 000000000..88fcf759a
--- /dev/null
+++ b/libs/minisat/UPDATE.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+rm -fv LICENSE *.cc *.h
+git clone --depth 1 https://github.com/niklasso/minisat minisat_upstream
+rm minisat_upstream/minisat/*/Main.cc
+mv minisat_upstream/LICENSE minisat_upstream/minisat/*/*.{h,cc} .
+rm -rf minisat_upstream
+
+sed -i -e 's,^#include *"minisat/[^/]\+,#include "libs/minisat,' *.cc *.h
+sed -i -e 's/PRIi64/ & /' Options.h
+sed -i -e '1 i #define __STDC_LIMIT_MACROS' *.cc
+sed -i -e '1 i #define __STDC_FORMAT_MACROS' *.cc
diff --git a/libs/minisat/Vec.h b/libs/minisat/Vec.h
new file mode 100644
index 000000000..2086e0bb2
--- /dev/null
+++ b/libs/minisat/Vec.h
@@ -0,0 +1,134 @@
+/*******************************************************************************************[Vec.h]
+Copyright (c) 2003-2007, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, 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 Minisat_Vec_h
+#define Minisat_Vec_h
+
+#include <assert.h>
+#include <limits>
+#include <new>
+
+#include "libs/minisat/IntTypes.h"
+#include "libs/minisat/XAlloc.h"
+
+namespace Minisat {
+
+//=================================================================================================
+// Automatically resizable arrays
+//
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T, class _Size = int>
+class vec {
+public:
+    typedef _Size Size;
+private:
+    T*   data;
+    Size sz;
+    Size cap;
+
+    // Don't allow copying (error prone):
+    vec<T>&  operator=(vec<T>& other);
+             vec      (vec<T>& other);
+
+    static inline Size max(Size x, Size y){ return (x > y) ? x : y; }
+
+public:
+    // Constructors:
+    vec()                        : data(NULL), sz(0), cap(0)    { }
+    explicit vec(Size size)      : data(NULL), sz(0), cap(0)    { growTo(size); }
+    vec(Size size, const T& pad) : data(NULL), sz(0), cap(0)    { growTo(size, pad); }
+   ~vec()                                                       { clear(true); }
+
+    // Pointer to first element:
+    operator T*       (void)           { return data; }
+
+    // Size operations:
+    Size     size     (void) const   { return sz; }
+    void     shrink   (Size nelems)  { assert(nelems <= sz); for (Size i = 0; i < nelems; i++) sz--, data[sz].~T(); }
+    void     shrink_  (Size nelems)  { assert(nelems <= sz); sz -= nelems; }
+    int      capacity (void) const   { return cap; }
+    void     capacity (Size min_cap);
+    void     growTo   (Size size);
+    void     growTo   (Size size, const T& pad);
+    void     clear    (bool dealloc = false);
+
+    // Stack interface:
+    void     push  (void)              { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; }
+    //void     push  (const T& elem)     { if (sz == cap) capacity(sz+1); data[sz++] = elem; }
+    void     push  (const T& elem)     { if (sz == cap) capacity(sz+1); new (&data[sz++]) T(elem); }
+    void     push_ (const T& elem)     { assert(sz < cap); data[sz++] = elem; }
+    void     pop   (void)              { assert(sz > 0); sz--, data[sz].~T(); }
+    // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but
+    // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not
+    // happen given the way capacities are calculated (below). Essentially, all capacities are
+    // even, but INT_MAX is odd.
+
+    const T& last  (void) const        { return data[sz-1]; }
+    T&       last  (void)              { return data[sz-1]; }
+
+    // Vector interface:
+    const T& operator [] (Size index) const { return data[index]; }
+    T&       operator [] (Size index)       { return data[index]; }
+
+    // Duplicatation (preferred instead):
+    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (Size i = 0; i < sz; i++) copy[i] = 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, class _Size>
+void vec<T,_Size>::capacity(Size min_cap) {
+    if (cap >= min_cap) return;
+    Size add = max((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1);   // NOTE: grow by approximately 3/2
+    const Size size_max = std::numeric_limits<Size>::max();
+    if ( ((size_max <= std::numeric_limits<int>::max()) && (add > size_max - cap))
+    ||   (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) )
+        throw OutOfMemoryException();
+ }
+
+
+template<class T, class _Size>
+void vec<T,_Size>::growTo(Size size, const T& pad) {
+    if (sz >= size) return;
+    capacity(size);
+    for (Size i = sz; i < size; i++) data[i] = pad;
+    sz = size; }
+
+
+template<class T, class _Size>
+void vec<T,_Size>::growTo(Size size) {
+    if (sz >= size) return;
+    capacity(size);
+    for (Size i = sz; i < size; i++) new (&data[i]) T();
+    sz = size; }
+
+
+template<class T, class _Size>
+void vec<T,_Size>::clear(bool dealloc) {
+    if (data != NULL){
+        for (Size i = 0; i < sz; i++) data[i].~T();
+        sz = 0;
+        if (dealloc) free(data), data = NULL, cap = 0; } }
+
+//=================================================================================================
+}
+
+#endif
diff --git a/libs/minisat/XAlloc.h b/libs/minisat/XAlloc.h
new file mode 100644
index 000000000..1da176028
--- /dev/null
+++ b/libs/minisat/XAlloc.h
@@ -0,0 +1,45 @@
+/****************************************************************************************[XAlloc.h]
+Copyright (c) 2009-2010, 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 Minisat_XAlloc_h
+#define Minisat_XAlloc_h
+
+#include <errno.h>
+#include <stdlib.h>
+
+namespace Minisat {
+
+//=================================================================================================
+// Simple layer on top of malloc/realloc to catch out-of-memory situtaions and provide some typing:
+
+class OutOfMemoryException{};
+static inline void* xrealloc(void *ptr, size_t size)
+{
+    void* mem = realloc(ptr, size);
+    if (mem == NULL && errno == ENOMEM){
+        throw OutOfMemoryException();
+    }else
+        return mem;
+}
+
+//=================================================================================================
+}
+
+#endif