diff --git a/Constraints.C b/Constraints.C new file mode 100644 index 0000000..0633ba5 --- /dev/null +++ b/Constraints.C @@ -0,0 +1,266 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include "Constraints.h" +#include "Solver.h" +#include "Sort.h" + + +//================================================================================================= +// Helpers: + + +void removeWatch(vec& ws, Constr* elem) +{ + int j = 0; + for (; ws[j] != elem ; j++) assert(j < ws.size()); + for (; j < ws.size()-1; j++) ws[j] = ws[j+1]; + ws.pop(); +} + + +//================================================================================================= +// Clause constraint: + + +// Returns FALSE if top-level conflict detected (must be handled); TRUE otherwise. +// 'out_clause' may be set to NULL if clause is already satisfied by the top-level assignment. +// +bool Clause_new(Solver& S, const vec& ps_, bool learnt, Clause*& out_clause) +{ + vec qs; + if (&out_clause != NULL) out_clause = NULL; + + if (!learnt){ + assert(S.decisionLevel() == 0); + ps_.copyTo(qs); // Make a copy of the input vector. + + // Remove false literals: + for (int i = 0; i < qs.size();){ + if (S.value(qs[i]) != l_Undef){ + if (S.value(qs[i]) == l_True) + return true; // Clause always true -- don't add anything. + else + qs[i] = qs.last(), + qs.pop(); + }else + i++; + } + + // Remove duplicates: + sortUnique(qs); + for (int i = 0; i < qs.size()-1; i++){ + if (qs[i] == ~qs[i+1]) + return true; // Clause always true -- don't add anything. + } + } + const vec& ps = learnt ? ps_ : qs; // 'ps' is now the (possibly) reduced vector of literals. + + if (ps.size() == 0) + return false; + else if (ps.size() == 1) + return S.enqueue(ps[0]); + else{ + // Allocate clause: + assert(sizeof(Lit) == sizeof(unsigned)); + assert(sizeof(float) == sizeof(unsigned)); + void* mem = xmalloc(sizeof(Clause) + sizeof(unsigned)*(ps.size() + (int)learnt)); + Clause* c = new (mem) Clause; + + c->size_learnt = (int)learnt | (ps.size() << 1); + for (int i = 0; i < ps.size(); i++) c->data[i] = ps[i]; + if (learnt) c->activity() = 0.0; + + // For learnt clauses only: + if (learnt){ + // Put the second watch on the literal with highest decision level: + int max_i = 1; + int max = S.level[var(ps[1])]; + for (int i = 2; i < ps.size(); i++) + if (S.level[var(ps[i])] > max) + max = S.level[var(ps[i])], + max_i = i; + c->data[1] = ps[max_i]; + c->data[max_i] = ps[1]; + + // Bumping: + S.claBumpActivity(c); // (newly learnt clauses should be considered active) + + S.stats.learnts++; + S.stats.learnts_literals += c->size(); + }else{ + S.stats.clauses++; + S.stats.clauses_literals += c->size(); + } + + // Store clause: + S.watches[index(~c->data[0])].push(c); + S.watches[index(~c->data[1])].push(c); + if (&out_clause != NULL) out_clause = c; + + return true; + } +} + + +bool Clause::locked(const Solver& S) const { + return (const Clause *)S.reason[var(data[0])] == this; } + + +void Clause::remove(Solver& S, bool just_dealloc) +{ + if (!just_dealloc){ + removeWatch(S.watches[index(~data[0])], this); + removeWatch(S.watches[index(~data[1])], this); } + + if (learnt()){ + S.stats.learnts--; + S.stats.learnts_literals -= size(); + }else{ + S.stats.clauses--; + S.stats.clauses_literals -= size(); + } + + xfree(this); +} + + +// Can assume everything has been propagated! (esp. the first two literals are != l_False, unless +// the clause is binary and satisfied, in which case the first literal is true) +// Returns True if clause is satisfied (will be removed), False otherwise. +// +bool Clause::simplify(Solver& S) +{ + assert(S.decisionLevel() == 0); + for (int i = 0; i < size(); i++){ + if (S.value(data[i]) == l_True) + return true; + } + return false; +} + + +// 'p' is the literal that became TRUE +bool Clause::propagate(Solver& S, Lit p, bool& keep_watch) +{ + // Make sure the false literal is data[1]: + Lit false_lit = ~p; + if (data[0] == false_lit) + data[0] = data[1], data[1] = false_lit; + assert(data[1] == false_lit); + + // If 0th watch is true, then clause is already satisfied. + if (S.value(data[0]) == l_True){ + keep_watch = true; + return true; } + + // Look for new watch: + for (int i = 2; i < size(); i++){ + if (S.value(data[i]) != l_False){ + data[1] = data[i], data[i] = false_lit; + S.watches[index(~data[1])].push(this); + return true; } } + + // Clause is unit under assignment: + keep_watch = true; + return S.enqueue(data[0], this); +} + + +// Can assume 'out_reason' to be empty. +// Calculate reason for 'p'. If 'p == lit_Undef', calculate reason for conflict. +// +void Clause::calcReason(Solver& S, Lit p, vec& out_reason) +{ + assert(p == lit_Undef || p == data[0]); + for (int i = ((p == lit_Undef) ? 0 : 1); i < size(); i++) + assert(S.value(data[i]) == l_False), + out_reason.push(~data[i]); + if (learnt()) S.claBumpActivity(this); +} + + +//================================================================================================= +// AtMost constraint -- An example of extending MiniSat: + + +// Pre-condition: All variables must be distinct and unbound. (To lift this pre-condition, +// any fact immediately derivable from the new constraint should be enqueued by 'enqueue()'. +// If the constraint is already satisfied under the current top-level assignment, it should +// not be constructed at all.) +// +bool AtMost_new(Solver& S, const vec& ps, int n, AtMost*& out) +{ + assert(S.decisionLevel() == 0); + + void* mem = (void*)xmalloc(sizeof(AtMost) + sizeof(Lit) * ps.size()); + out = new (mem) AtMost; + out->size = ps.size(); + out->n = n; + out->counter = 0; + for (int i = 0; i < ps.size(); i++) out->lits[i] = ps[i]; + for (int i = 0; i < ps.size(); i++) S.watches[index(ps[i])].push(out); + + return true; +} + + +void AtMost::remove(Solver& S, bool just_dealloc) { + if (!just_dealloc) + for (int i = 0; i < size; i++) + removeWatch(S.watches[index(lits[i])], this); + xfree(this); +} + + +bool AtMost::simplify(Solver& S) { + return false; } + + +bool AtMost::propagate(Solver& S, Lit p, bool& keep_watch) +{ + keep_watch = true; + if (counter == n) return false; + + counter++; + S.undos[var(p)].push(this); + + // If no more can be true, enqueue the negation of the rest: + if (counter == n) + for (int i = 0; i < size; i++) + if (!S.enqueue(~lits[i], this)) + return false; + return true; +} + + +void AtMost::undo(Solver& S, Lit p) { + counter--; } + + +void AtMost::calcReason(Solver& S, Lit p, vec& out_reason) +{ + int c = (p == lit_Undef) ? -1 : 0; + for (int i = 0; i < size; i++){ + if (S.value(lits[i]) == l_True){ + out_reason.push(lits[i]); + if (++c == n) return; + } + } +} diff --git a/Constraints.h b/Constraints.h new file mode 100644 index 0000000..8c6e742 --- /dev/null +++ b/Constraints.h @@ -0,0 +1,95 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Constraints_h +#define Constraints_h + +#include "SolverTypes.h" + + +//================================================================================================= +// Constraint abstraction: + + +class Solver; + +struct Constr { + virtual void remove (Solver& S, bool just_dealloc = false) = 0; + virtual bool propagate (Solver& S, Lit p, bool& keep_watch) = 0; // ('keep_watch' is set to FALSE beftore call to this method) + virtual bool simplify (Solver& S) { return false; }; + virtual void undo (Solver& S, Lit p) { }; + virtual void calcReason(Solver& S, Lit p, vec& out_reason) = 0; + + virtual ~Constr(void) { }; // (not used, just to keep the compiler happy) +}; + + +//================================================================================================= +// Clauses: + + +class Clause : public Constr { + unsigned size_learnt; + Lit data[0]; + +public: + int size (void) const { return size_learnt >> 1; } + bool learnt (void) const { return size_learnt & 1; } + Lit operator [] (int index) const { return data[index]; } + + // Constructor -- creates a new clause and add it to watcher lists. + friend bool Clause_new(Solver& S, const vec& ps, bool learnt, Clause*& out_clause); + + // Learnt clauses only: + bool locked (const Solver& S) const; + float& activity(void) const { return *((float*)&data[size()]); } + + // Constraint interface: + void remove (Solver& S, bool just_dealloc = false); + bool propagate (Solver& S, Lit p, bool& keep_watch); + bool simplify (Solver& S); + void calcReason(Solver& S, Lit p, vec& out_reason); +}; + + +//================================================================================================= +// AtMost: + + +class AtMost : public Constr { + int n; + int counter; + int size; + Lit lits[0]; + +public: + // Constructor -- creates a new AtMost-constraint and add it to watcher lists. + friend bool AtMost_new(Solver& S, const vec& ps, int n, AtMost*& out); + + // Constraint interface: + void remove (Solver& S, bool just_dealloc = false); + bool propagate (Solver& S, Lit p, bool& keep_watch); + bool simplify (Solver& S); + void undo (Solver& S, Lit p); + void calcReason(Solver& S, Lit p, vec& out_reason); +}; + + +//================================================================================================= +#endif diff --git a/Global.h b/Global.h new file mode 100644 index 0000000..54462ab --- /dev/null +++ b/Global.h @@ -0,0 +1,236 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Global_h +#define Global_h + +#include +#include +#include +#include +#include +#include +#include + + +//================================================================================================= +// Basic Types & Minor Things: + + +#ifdef _MSC_VER +typedef __int64 int64; +#define I64_fmt "I64d" +#else +typedef long long int64; +#define I64_fmt "lld" +#endif +typedef const char cchar; + + +template static inline T min(T x, T y) { return (x < y) ? x : y; } +template static inline T max(T x, T y) { return (x > y) ? x : y; } + +template struct STATIC_ASSERTION_FAILURE; +template <> struct STATIC_ASSERTION_FAILURE{}; +#define TEMPLATE_FAIL STATIC_ASSERTION_FAILURE() + + +//================================================================================================= +// 'malloc()'-style memory allocation -- never returns NULL; aborts instead: + + +template static inline T* xmalloc(size_t size) { + T* tmp = (T*)malloc(size * sizeof(T)); + assert(size == 0 || tmp != NULL); + return tmp; } + +template static inline T* xrealloc(T* ptr, size_t size) { + T* tmp = (T*)realloc((void*)ptr, size * sizeof(T)); + assert(size == 0 || tmp != NULL); + return tmp; } + +template static inline void xfree(T *ptr) { + if (ptr != NULL) free((void*)ptr); } + + +//================================================================================================= +// Random numbers: + + +// Returns a random float 0 <= x < 1. Seed must never be 0. +static inline double drand(double& seed) { + seed *= 1389796; + int q = (int)(seed / 2147483647); + seed -= (double)q * 2147483647; + return seed / 2147483647; } + +// Returns a random integer 0 <= x < size. Seed must never be 0. +static inline int irand(double& seed, int size) { + return (int)(drand(seed) * size); } + + +//================================================================================================= +// Time: + + +#ifdef _MSC_VER +#include +static inline double cpuTime(void) { + return (double)clock() / CLOCKS_PER_SEC; } +#else +#include +#include +static inline double cpuTime(void) { + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } +#endif + + +//================================================================================================= +// 'vec' -- automatically resizable arrays (via 'push()' method): + + +// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) + +template +class vec { + T* data; + int sz; + int cap; + + void init(int size, const T& pad); + void grow(int min_cap); + +public: + // Types: + typedef int Key; + typedef T Datum; + + // Constructors: + vec(void) : data(NULL) , sz(0) , cap(0) { } + vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } + vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } + vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'xfree()') + ~vec(void) { clear(true); } + + // Ownership of underlying array: + T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; } + operator T* (void) { return data; } // (unsafe but convenient) + operator const T* (void) const { return data; } + + // Size operations: + int size (void) const { return sz; } + void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); } + void pop (void) { sz--, data[sz].~T(); } + void growTo (int size); + void growTo (int size, const T& pad); + void clear (bool dealloc = false); + + // Stack interface: + void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; } + void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; } + const T& last (void) const { return data[sz-1]; } + T& last (void) { return data[sz-1]; } + + // Vector interface: + const T& operator [] (int index) const { return data[index]; } + T& operator [] (int index) { return data[index]; } + + // Don't allow copying (error prone): + vec& operator = (vec& other) { TEMPLATE_FAIL; } + vec (vec& other) { TEMPLATE_FAIL; } + + // Duplicatation (preferred instead): + void copyTo(vec& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); } + void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } +}; + +template +void vec::grow(int min_cap) { + if (min_cap <= cap) return; + if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2; + else do cap = (cap*3 + 1)>>1; while (cap < min_cap); + data = xrealloc(data, cap); } + +template +void vec::growTo(int size, const T& pad) { + if (sz >= size) return; + grow(size); + for (int i = sz; i < size; i++) new (&data[i]) T(pad); + sz = size; } + +template +void vec::growTo(int size) { + if (sz >= size) return; + grow(size); + for (int i = sz; i < size; i++) new (&data[i]) T(); + sz = size; } + +template +void vec::clear(bool dealloc) { + if (data != NULL){ + for (int i = 0; i < sz; i++) data[i].~T(); + sz = 0; + if (dealloc) xfree(data), data = NULL, cap = 0; } } + + +//================================================================================================= +// Lifted booleans: + + +class lbool { + int value; + explicit lbool(int v) : value(v) { } + +public: + lbool() : value(0) { } + lbool(bool x) : value((int)x*2-1) { } + int toInt(void) const { return value; } + + bool operator == (const lbool& other) const { return value == other.value; } + bool operator != (const lbool& other) const { return value != other.value; } + lbool operator ~ (void) const { return lbool(-value); } + + friend int toInt (lbool l); + friend lbool toLbool(int v); +}; +inline int toInt (lbool l) { return l.toInt(); } +inline lbool toLbool(int v) { return lbool(v); } + +const lbool l_True = toLbool( 1); +const lbool l_False = toLbool(-1); +const lbool l_Undef = toLbool( 0); + + +//================================================================================================= +// Relation operators -- extend definitions from '==' and '<' + + +#ifndef __SGI_STL_INTERNAL_RELOPS // (be aware of SGI's STL implementation...) +#define __SGI_STL_INTERNAL_RELOPS +template static inline bool operator != (const T& x, const T& y) { return !(x == y); } +template static inline bool operator > (const T& x, const T& y) { return y < x; } +template static inline bool operator <= (const T& x, const T& y) { return !(y < x); } +template static inline bool operator >= (const T& x, const T& y) { return !(x < y); } +#endif + + +//================================================================================================= +#endif diff --git a/Heap.h b/Heap.h new file mode 100644 index 0000000..8aa2bc5 --- /dev/null +++ b/Heap.h @@ -0,0 +1,96 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef __HEAP__ +#define __HEAP__ + +static inline int left (int i) { return i * 2; } +static inline int right(int i) { return i * 2 + 1; } +static inline int parent(int i) { return i / 2; } + +template +class Heap { + public: + C comp; + vec heap; // heap of ints + vec indices; // int -> index in heap + + inline void percolateUp(int i) + { + int x = heap[i]; + while (parent(i) != 0 && comp(x,heap[parent(i)])){ + heap[i] = heap[parent(i)]; + indices[heap[i]] = i; + i = parent(i); + } + heap[i] = x; + indices[x] = i; + } + + inline void percolateDown(int i) + { + int x = heap[i]; + while (left(i) < heap.size()){ + int child = right(i) < heap.size() && comp(heap[right(i)],heap[left(i)]) ? right(i) : left(i); + if (!comp(heap[child],x)) break; + heap[i] = heap[child]; + indices[heap[i]] = i; + i = child; + } + heap[i] = x; + indices[x] = i; + } + + bool ok(int n) { return n >= 0 && n < (int)indices.size(); } + + public: + Heap(C c) : comp(c) { heap.push(-1); } + + void setBounds (int size) { assert(size >= 0); indices.growTo(size,0); } + bool inHeap (int n) { assert(ok(n)); return indices[n] != 0; } + void increase (int n) { assert(ok(n)); assert(inHeap(n)); percolateUp(indices[n]); } + bool empty (void) { return heap.size() == 1; } + + void insert(int n) { + assert(ok(n)); + indices[n] = heap.size(); + heap.push(n); + percolateUp(indices[n]); + } + + int getmin(void) { + int r = heap[1]; + heap[1] = heap.last(); + indices[heap[1]] = 1; + indices[r] = 0; + heap.pop(); + if (heap.size() > 1) + percolateDown(1); + return r; + } + + bool heapProperty(void) { return heapProperty(1); } + bool heapProperty(int i) { + return (size_t)i >= heap.size() || + ((parent(i) == 0 || !comp(heap[i],heap[parent(i)])) && + heapProperty(left(i)) && heapProperty(right(i))); + } +}; + +#endif diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..590930b --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a +copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS +OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/Main.C b/Main.C new file mode 100644 index 0000000..5696a18 --- /dev/null +++ b/Main.C @@ -0,0 +1,168 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include "Solver.h" +#include +#include +#include +#include + +//================================================================================================= +// Helpers: + + +// Reads an input stream to end-of-file and returns the result as a 'char*' terminated by '\0' +// (dynamic allocation in case 'in' is standard input). +// +char* readFile(gzFile in) +{ + char* data = xmalloc(65536); + int cap = 65536; + int size = 0; + + while (!gzeof(in)){ + if (size == cap){ + cap *= 2; + data = xrealloc(data, cap); } + size += gzread(in, &data[size], 65536); + } + data = xrealloc(data, size+1); + data[size] = '\0'; + + return data; +} + + +//================================================================================================= +// DIMACS Parser: + + +static void skipWhitespace(char*& in) { + while ((*in >= 9 && *in <= 13) || *in == 32) + in++; } + +static void skipLine(char*& in) { + for (;;){ + if (*in == 0) return; + if (*in == '\n') { in++; return; } + in++; } } + +static int parseInt(char*& in) { + int val = 0; + bool neg = false; + skipWhitespace(in); + if (*in == '-') neg = true, in++; + else if (*in == '+') in++; + if (*in < '0' || *in > '9') fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(1); + while (*in >= '0' && *in <= '9') + val = val*10 + (*in - '0'), + in++; + return neg ? -val : val; } + +static void readClause(char*& in, Solver& S, vec& lits) { + int parsed_lit, var; + lits.clear(); + for (;;){ + parsed_lit = parseInt(in); + if (parsed_lit == 0) break; + var = abs(parsed_lit)-1; + while (var >= S.nVars()) S.newVar(); + lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) ); + } +} + +static bool parse_DIMACS_main(char* in, Solver& S) { + vec lits; + for (;;){ + skipWhitespace(in); + if (*in == 0) + break; + else if (*in == 'c' || *in == 'p') + skipLine(in); + else{ + readClause(in, S, lits); + S.addClause(lits); + if (!S.okay()) + return false; + } + } + S.simplifyDB(); + return S.okay(); +} + + +// Inserts problem into solver. Returns FALSE upon immediate conflict. +// +bool parse_DIMACS(gzFile in, Solver& S) { + char* text = readFile(in); + bool ret = parse_DIMACS_main(text, S); + free(text); + return ret; } + + +//================================================================================================= + + +void printStats(SolverStats& stats, double cpu_time) +{ + printf("restarts : %"I64_fmt"\n", stats.starts); + printf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", stats.conflicts , stats.conflicts /cpu_time); + printf("decisions : %-12"I64_fmt" (%.0f /sec)\n", stats.decisions , stats.decisions /cpu_time); + printf("propagations : %-12"I64_fmt" (%.0f /sec)\n", stats.propagations, stats.propagations/cpu_time); + printf("inspects : %-12"I64_fmt" (%.0f /sec)\n", stats.inspects , stats.inspects /cpu_time); + printf("CPU time : %g s\n", cpu_time); +} + +Solver* solver; +static void SIGINT_handler(int signum) { + printf("\n"); printf("*** INTERRUPTED ***\n"); + printStats(solver->stats, cpuTime()); + printf("\n"); printf("*** INTERRUPTED ***\n"); + exit(0); } + + +//================================================================================================= + + +int main(int argc, char** argv) +{ + Solver S; + bool st; + + gzFile in = argc == 1 ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); + if (in == NULL) + fprintf(stderr, "ERROR! Could not open file: %s\n", argc == 1 ? "" : argv[1]), + exit(1); + st = parse_DIMACS(in, S); + gzclose(in); + + if (!st) + printf("Trivial problem\nUNSATISFIABLE\n"), + exit(20); + + S.verbosity = 1; + solver = &S; + signal(SIGINT,SIGINT_handler); + st = S.solve(); + printStats(S.stats, cpuTime()); + printf("\n"); + printf(st ? "SATISFIABLE\n" : "UNSATISFIABLE\n"); + + return 0; +} diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..aa19b44 --- /dev/null +++ b/Makefile @@ -0,0 +1,85 @@ +## +## Makefile for Standard, Profile, Debug, and Release version of MiniSat +## + +CSRCS = $(wildcard *.C) +CHDRS = $(wildcard *.h) +COBJS = $(addsuffix .o, $(basename $(CSRCS))) + +PCOBJS = $(addsuffix p, $(COBJS)) +DCOBJS = $(addsuffix d, $(COBJS)) +RCOBJS = $(addsuffix r, $(COBJS)) + +EXEC = minisat + +CXX = g++ +CFLAGS = -Wall +COPTIMIZE = -O3 -fomit-frame-pointer + + +.PHONY : s p d r build clean depend + +s: WAY=standard +p: WAY=profile +d: WAY=debug +r: WAY=release +rs: WAY=release static + +s: CFLAGS+=$(COPTIMIZE) -ggdb -D DEBUG +p: CFLAGS+=$(COPTIMIZE) -pg -ggdb -D DEBUG +d: CFLAGS+=-O0 -ggdb -D DEBUG +r: CFLAGS+=$(COPTIMIZE) -D NDEBUG +rs: CFLAGS+=$(COPTIMIZE) -D NDEBUG + +s: build $(EXEC) +p: build $(EXEC)_profile +d: build $(EXEC)_debug +r: build $(EXEC)_release +rs: build $(EXEC)_static + +build: + @echo Building $(EXEC) "("$(WAY)")" + +clean: + @rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \ + $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) depend.mak + +## Build rule +%.o %.op %.od %.or: %.C + @echo Compiling: $< + @$(CXX) $(CFLAGS) -c -o $@ $< + +## Linking rules (standard/profile/debug/release) +$(EXEC): $(COBJS) + @echo Linking $(EXEC) + @$(CXX) $(COBJS) -lz -ggdb -Wall -o $@ + +$(EXEC)_profile: $(PCOBJS) + @echo Linking $@ + @$(CXX) $(PCOBJS) -lz -ggdb -Wall -pg -o $@ + +$(EXEC)_debug: $(DCOBJS) + @echo Linking $@ + @$(CXX) $(DCOBJS) -lz -ggdb -Wall -o $@ + +$(EXEC)_release: $(RCOBJS) + @echo Linking $@ + @$(CXX) $(RCOBJS) -lz -Wall -o $@ + +$(EXEC)_static: $(RCOBJS) + @echo Linking $@ + @$(CXX) --static $(RCOBJS) -lz -Wall -o $@ + + +## Make dependencies +depend: depend.mak +depend.mak: $(CSRCS) $(CHDRS) + @echo Making dependencies ... + @$(CXX) -MM $(CSRCS) > depend.mak + @cp depend.mak /tmp/depend.mak.tmp + @sed "s/o:/op:/" /tmp/depend.mak.tmp >> depend.mak + @sed "s/o:/od:/" /tmp/depend.mak.tmp >> depend.mak + @sed "s/o:/or:/" /tmp/depend.mak.tmp >> depend.mak + @rm /tmp/depend.mak.tmp + +include depend.mak diff --git a/Queue.h b/Queue.h new file mode 100644 index 0000000..9bb3112 --- /dev/null +++ b/Queue.h @@ -0,0 +1,45 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Queue_h +#define Queue_h + + +//================================================================================================= + + +template +class Queue { + vec elems; + int first; + +public: + Queue(void) : first(0) { } + + void insert(T x) { elems.push(x); } + T dequeue(void) { return elems[first++]; } + void clear(void) { elems.clear(); first = 0; } + int size(void) { return elems.size() - first; } + + bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; } +}; + + +//================================================================================================= +#endif diff --git a/README b/README new file mode 100644 index 0000000..d7665c2 --- /dev/null +++ b/README @@ -0,0 +1,10 @@ +MiniSat v1.12b +======================================== + +This is the last version where arbitrary boolean constraints are +supported. Later versions of MiniSat only supports clauses. However, +don't be discouraged; the improvements made in v1.13 and v1.14 are +quite easily back-ported to this version, so if you really need the +functionality provided by this release, go ahead and use it (and send +us the upgrades if you make them!) + diff --git a/README~ b/README~ new file mode 100644 index 0000000..3642630 --- /dev/null +++ b/README~ @@ -0,0 +1,10 @@ +MiniSat v1.12b +======================================== + +This is the last version where arbitrary boolean constraints are +supported. Later versions of MiniSat only supports clauses. However, +don't be discouraged; the improvements made in v1.13 and v1.14 are +quite easily back-ported to this version, so if you really need +the functionality provided by this release, go ahead and use it +(and send us the upgrades if you make them!) + diff --git a/Solver.C b/Solver.C new file mode 100644 index 0000000..3b6068b --- /dev/null +++ b/Solver.C @@ -0,0 +1,496 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#include "Solver.h" +#include "Sort.h" +#include + + +//================================================================================================= +// Debug: + + +// For derivation output (verbosity level 2) +#define L_IND "%-*d" +#define L_ind decisionLevel()*3+3,decisionLevel() +#define L_LIT "%sx%d" +#define L_lit(p) sign(p)?"~":"", var(p) + +// Just like 'assert()' but expression will be evaluated in the release version as well. +inline void check(bool expr) { assert(expr); } + + +//================================================================================================= +// Minor methods: + + +// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be +// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). +// +Var Solver::newVar(void) +{ + int index; + index = nVars(); + watches .push(); // (list for positive literal) + watches .push(); // (list for negative literal) + undos .push(); + reason .push(NULL); + assigns .push(toInt(l_Undef)); + level .push(-1); + activity.push(0); + order .newVar(); + return index; +} + + +// Returns FALSE if immediate conflict. +bool Solver::assume(Lit p) { + assert(propQ.size() == 0); + if (verbosity >= 2) printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(p)); + trail_lim.push(trail.size()); + return enqueue(p); } + + +// Revert one variable binding on the trail. +// +inline void Solver::undoOne(void) +{ + if (verbosity >= 2){ Lit p = trail.last(); printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(p)); } + Lit p = trail.last(); trail.pop(); + Var x = var(p); + assigns[x] = toInt(l_Undef); + reason [x] = NULL; + order.undo(x); + while (undos[x].size() > 0) + undos[x].last()->undo(*this, p), + undos[x].pop(); +} + + +// Reverts to the state before last 'assume()'. +// +void Solver::cancel(void) +{ + assert(propQ.size() == 0); + if (verbosity >= 2){ if (trail.size() != trail_lim.last()){ Lit p = trail[trail_lim.last()]; printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(p)); } } + for (int c = trail.size() - trail_lim.last(); c != 0; c--) + undoOne(); + trail_lim.pop(); +} + + +// Revert to the state at given level. +// +void Solver::cancelUntil(int level) { + while (decisionLevel() > level) cancel(); } + + +// Record a clause and drive backtracking. 'clause[0]' must contain the asserting literal. +// +void Solver::record(const vec& clause) +{ + assert(clause.size() != 0); + Clause* c; + check(Clause_new(*this, clause, true, c)); + check(ok); + check(enqueue(clause[0], c)); + if (c != NULL) learnts.push(c); +} + + +//================================================================================================= +// Major methods: + + +/*_________________________________________________________________________________________________ +| +| analyze : (confl : Constr*) (out_learnt : vec&) (out_btlevel : int&) -> [void] +| +| Description: +| Analyze conflict and produce a reason clause. +| +| Pre-conditions: +| * 'out_learnt' is assumed to be cleared. +| * Current decision level must be greater than root level. +| +| Post-conditions: +| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. +| +| Effect: +| Will undo part of the trail, upto but not beyond the assumption of the current decision level. +|________________________________________________________________________________________________@*/ +void Solver::analyze(Constr* confl, vec& out_learnt, int& out_btlevel) +{ + vec& seen = analyze_seen; + int pathC = 0; + Lit p = lit_Undef; + vec p_reason; + seen.growTo(nVars(), 0); + + // Generate conflict clause: + // + out_learnt.push(); // (leave room for the asserting literal) + out_btlevel = 0; + do{ + assert(confl != NULL); // (otherwise should be UIP) + + p_reason.clear(); + confl->calcReason(*this, p, p_reason); + + for (int j = 0; j < p_reason.size(); j++){ + Lit q = p_reason[j]; + if (!seen[var(q)] && level[var(q)] > 0){ + seen[var(q)] = 1; + varBumpActivity(q); + if (level[var(q)] == decisionLevel()) + pathC++; + else{ + out_learnt.push(~q), + out_btlevel = max(out_btlevel, level[var(q)]); + } + } + } + + // Select next clause to look at: + do{ + p = trail.last(); + confl = reason[var(p)]; + undoOne(); + }while (!seen[var(p)]); + pathC--; + seen[var(p)] = 0; + }while (pathC > 0); + out_learnt[0] = ~p; + + for (int j = 0; j < out_learnt.size(); j++) seen[var(out_learnt[j])] = 0; // ('seen[]' is now cleared) + + if (verbosity >= 2){ + printf(L_IND"Learnt {", L_ind); + for (int i = 0; i < out_learnt.size(); i++) printf(" "L_LIT, L_lit(out_learnt[i])); + printf(" } at level %d\n", out_btlevel); } +} + + +/*_________________________________________________________________________________________________ +| +| enqueue : (p : Lit) (from : Constr*) -> [bool] +| +| Description: +| Puts a new fact on the propagation queue as well as immediately updating the variable's value. +| Should a conflict arise, FALSE is returned. +| +| Input: +| p - The fact to enqueue +| from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'. +| Default value is NULL (no reason). +| +| Output: +| TRUE if fact was enqueued without conflict, FALSE otherwise. +|________________________________________________________________________________________________@*/ +bool Solver::enqueue(Lit p, Constr* from) +{ + if (value(p) != l_Undef){ + if (value(p) == l_False){ + // Conflicting enqueued assignment + if (decisionLevel() == 0) + ok = false; + return false; + }else{ + // Existing consistent assignment -- don't enqueue + return true; + } + }else{ + // New fact -- store it. + if (verbosity >= 2) printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(p)); + assigns[var(p)] = toInt(lbool(!sign(p))); + level [var(p)] = decisionLevel(); + reason [var(p)] = from; + trail.push(p); + propQ.insert(p); + return true; + } +} + + +/*_________________________________________________________________________________________________ +| +| propagate : [void] -> [Constr*] +| +| Description: +| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, +| otherwise NULL. +| +| Post-conditions: +| * the propagation queue is empty, even if there was a conflict. +|________________________________________________________________________________________________@*/ +Constr* Solver::propagate(void) +{ + Constr* confl = NULL; + while (propQ.size() > 0){ + stats.propagations++; + Lit p = propQ.dequeue(); // 'p' is enqueued fact to propagate. + vec& ws = watches[index(p)]; + bool keep_watch; + Constr **i, **j, **end = (Constr**)ws + ws.size(); + for (i = j = (Constr**)ws; confl == NULL && i < end; i++){ + stats.inspects++; + keep_watch = false; + if (!(*i)->propagate(*this, p, keep_watch)) + confl = *i, + propQ.clear(); + if (keep_watch) + *j++ = *i; + } + + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + + ws.shrink(i - j); + } + + return confl; +} + + +/*_________________________________________________________________________________________________ +| +| reduceDB : () -> [void] +| +| Description: +| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked +| clauses are clauses that are reason to a some assignment. +|________________________________________________________________________________________________@*/ +struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->activity() < y->activity(); } }; +void Solver::reduceDB(void) +{ + int i, j; + double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity + + sort(learnts, reduceDB_lt()); + for (i = j = 0; i < learnts.size() / 2; i++){ + if (!learnts[i]->locked(*this)) + learnts[i]->remove(*this); + else + learnts[j++] = learnts[i]; + } + for (; i < learnts.size(); i++){ + if (!learnts[i]->locked(*this) && learnts[i]->activity() < extra_lim) + learnts[i]->remove(*this); + else + learnts[j++] = learnts[i]; + } + learnts.shrink(i - j); +} + + +/*_________________________________________________________________________________________________ +| +| simplifyDB : [void] -> [bool] +| +| Description: +| Simplify all constraints according to the current top-level assigment (redundant constraints +| may be removed altogether). +|________________________________________________________________________________________________@*/ +void Solver::simplifyDB(void) +{ + if (!ok) return; // GUARD (public method) + assert(decisionLevel() == 0); + + if (propagate() != NULL){ + ok = false; + return; } + if (nAssigns() == last_simplify) + return; + + last_simplify = nAssigns(); + + for (int type = 0; type < 2; type++){ + vec& cs = type ? (vec&)learnts : constrs; + + int j = 0; + for (int i = 0; i < cs.size(); i++){ + if (cs[i]->simplify(*this)) + cs[i]->remove(*this); + else + cs[j++] = cs[i]; + } + cs.shrink(cs.size()-j); + } +} + + +/*_________________________________________________________________________________________________ +| +| search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool] +| +| Description: +| Search for a model the specified number of conflicts, keeping the number of learnt clauses +| below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to +| indicate infinity. +| +| Output: +| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If +| all variables are decision variables, this means that the clause set is satisfiable. 'l_False' +| if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. +|________________________________________________________________________________________________@*/ +lbool Solver::search(int nof_conflicts, int nof_learnts, const SearchParams& params) +{ + if (!ok) return l_False; // GUARD (public method) + assert(root_level == decisionLevel()); + + stats.starts++; + int conflictC = 0; + var_decay = 1 / params.var_decay; + cla_decay = 1 / params.clause_decay; + model.clear(); + + for (;;){ + Constr* confl = propagate(); + if (confl != NULL){ + // CONFLICT + + if (verbosity >= 2) printf(L_IND"**CONFLICT**\n", L_ind); + stats.conflicts++; conflictC++; + vec learnt_clause; + int backtrack_level; + if (decisionLevel() == root_level) + return l_False; + analyze(confl, learnt_clause, backtrack_level); + cancelUntil(max(backtrack_level, root_level)); + record(learnt_clause); + varDecayActivity(); claDecayActivity(); + + }else{ + // NO CONFLICT + + if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + propQ.clear(); + cancelUntil(root_level); + return l_Undef; } + + if (decisionLevel() == 0) + // Simplify the set of problem clauses: + simplifyDB(), assert(ok); + + if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts) + // Reduce the set of learnt clauses: + reduceDB(); + + // New variable decision: + stats.decisions++; + Var next = order.select(params.random_var_freq); + + if (next == var_Undef){ + // Model found: + model.growTo(nVars()); + for (int i = 0; i < nVars(); i++) model[i] = value(i); + cancelUntil(root_level); + return l_True; + } + + check(assume(~Lit(next))); + } + } +} + + +// Return search-space coverage. Not extremely reliable. +// +double Solver::progressEstimate(void) +{ + double progress = 0; + double F = 1.0 / nVars(); + for (int i = 0; i < nVars(); i++) + if (value(i) != l_Undef) + progress += pow(F, level[i]); + return progress / nVars(); +} + + +// Divide all variable activities by 1e100. +// +void Solver::varRescaleActivity(void) +{ + for (int i = 0; i < nVars(); i++) + activity[i] *= 1e-100; + var_inc *= 1e-100; +} + + +// Divide all constraint activities by 1e100. +// +void Solver::claRescaleActivity(void) +{ + for (int i = 0; i < learnts.size(); i++) + learnts[i]->activity() *= 1e-20; + cla_inc *= 1e-20; +} + + +/*_________________________________________________________________________________________________ +| +| solve : (assumps : const vec&) -> [bool] +| +| Description: +| Top-level solve. If using assumptions (non-empty 'assumps' vector), you must call +| 'simplifyDB()' first to see that no top-level conflict is present (which would put the solver +| in an undefined state). +|________________________________________________________________________________________________@*/ +bool Solver::solve(const vec& assumps) +{ + simplifyDB(); + if (!ok) return false; + + SearchParams params(0.95, 0.999, 0.02); + double nof_conflicts = 100; + double nof_learnts = nConstrs() / 3; + lbool status = l_Undef; + + for (int i = 0; i < assumps.size(); i++) + if (!assume(assumps[i]) || propagate() != NULL){ + propQ.clear(); + cancelUntil(0); + return false; } + root_level = decisionLevel(); + + if (verbosity >= 1){ + printf("==================================[MINISAT]===================================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n"); + printf("==============================================================================\n"); + } + + while (status == l_Undef){ + if (verbosity >= 1){ + printf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n", (int)stats.conflicts, nConstrs(), (int)stats.clauses_literals, (int)nof_learnts, nLearnts(), (int)stats.learnts_literals, (double)stats.learnts_literals/nLearnts(), progress_estimate*100); + fflush(stdout); + } + status = search((int)nof_conflicts, (int)nof_learnts, params); + nof_conflicts *= 1.5; + nof_learnts *= 1.1; + } + if (verbosity >= 1) + printf("==============================================================================\n"); + + cancelUntil(0); + return status == l_True; +} diff --git a/Solver.h b/Solver.h new file mode 100644 index 0000000..acdc664 --- /dev/null +++ b/Solver.h @@ -0,0 +1,164 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Solver_h +#define Solver_h + +#include "SolverTypes.h" +#include "Constraints.h" +#include "Queue.h" +#include "VarOrder.h" + + +//================================================================================================= +// Solver -- the main class: + + +struct SolverStats { + int64 starts, decisions, propagations, inspects, conflicts; + int64 clauses, clauses_literals, learnts, learnts_literals; + SolverStats(void) : starts(0), decisions(0), propagations(0), inspects(0), conflicts(0) + , clauses(0), clauses_literals(0), learnts(0), learnts_literals(0) { } +}; + + +struct SearchParams { + double var_decay, clause_decay, random_var_freq; // (reasonable values are: 0.95, 0.999, 0.02) + SearchParams(double v = 1, double c = 1, double r = 0) : var_decay(v), clause_decay(c), random_var_freq(r) { } +}; + + +class Solver { +protected: + bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! + vec constrs; // List of problem constraints. + vec learnts; // List of learnt clauses. + double cla_inc; // Amount to bump next clause with. + double cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + + vec activity; // A heuristic measurement of the activity of a variable. + double var_inc; // Amount to bump next variable with. + double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order. + VarOrder order; // Keeps track of the decision variable order. + + vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + vec > undos; // 'undos[var]' is a list of constraints that will be called when 'var' becomes unbound. + Queue propQ; // Propagation queue. + + vec assigns; // The current assignments (lbool:s stored as char:s). + vec trail; // List of assignments made. + vec trail_lim; // Separator indices for different decision levels in 'trail'. + vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + vec level; // 'level[var]' is the decision level at which assignment was made. + int root_level; // Level of first proper decision. + int last_simplify; // Number of top-level assignments at last 'simplifyDB()'. + + // Temporaries (to reduce allocation overhead): + // + vec analyze_seen; + + // Main internal methods: + // + bool assume (Lit p); + void undoOne (void); + void cancel (void); + void cancelUntil (int level); + void record (const vec& clause); + + void analyze (Constr* confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) + bool enqueue (Lit fact, Constr* from = NULL); + Constr* propagate (void); + void reduceDB (void); + Lit pickBranchLit(const SearchParams& params); + lbool search (int nof_conflicts, int nof_learnts, const SearchParams& params); + double progressEstimate(void); + + // Activity: + // + void varBumpActivity(Lit p) { + if (var_decay < 0) return; // (negative decay means static variable order -- don't bump) + if ( (activity[var(p)] += var_inc) > 1e100 ) varRescaleActivity(); + order.update(var(p)); } + void varDecayActivity(void) { if (var_decay >= 0) var_inc *= var_decay; } + void varRescaleActivity(void); + + void claBumpActivity(Clause* c) { if ( (c->activity() += cla_inc) > 1e20 ) claRescaleActivity(); } + void claDecayActivity(void) { cla_inc *= cla_decay; } + void claRescaleActivity(void); + + int decisionLevel(void) { return trail_lim.size(); } + +public: + Solver(void) : ok (true) + , cla_inc (1) + , cla_decay (1) + , var_inc (1) + , var_decay (1) + , order (assigns, activity) + , last_simplify (-1) + , progress_estimate(0) + , verbosity(0) + { } + ~Solver(void) { + for (int i = 0; i < learnts.size(); i++) learnts[i]->remove(*this, true); + for (int i = 0; i < constrs.size(); i++) constrs[i]->remove(*this, true); } + + // Helpers: (semi-internal) + // + lbool value(Var x) { return toLbool(assigns[x]); } + lbool value(Lit p) { return sign(p) ? ~toLbool(assigns[var(p)]) : toLbool(assigns[var(p)]); } + + int nAssigns(void) { return trail.size(); } + int nConstrs(void) { return constrs.size(); } + int nLearnts(void) { return learnts.size(); } + + // Statistics: (read-only member variable) + // + SolverStats stats; + + // Problem specification: + // + Var newVar (void); + int nVars (void) { return assigns.size(); } + void addUnit(Lit p) { if (ok) enqueue(p); } + + // -- constraints: + friend class Clause; + friend class AtMost; + friend bool Clause_new(Solver& S, const vec& ps, bool learnt, Clause*& out_clause); + friend bool AtMost_new(Solver& S, const vec& ps, int max , AtMost*& out_constr); + + void addClause(const vec& ps) { if (ok){ Clause* c; ok = Clause_new(*this, ps, false, c); if (c != NULL) constrs.push(c); } } + void addAtMost(const vec& ps, int n) { if (ok){ AtMost* c; ok = AtMost_new(*this, ps, n , c); if (c != NULL) constrs.push(c); } } + + // Solving: + // + bool okay(void) { return ok; } + void simplifyDB(void); + bool solve(const vec& assumps); + bool solve(void) { vec tmp; return solve(tmp); } + + double progress_estimate; // Set by 'search()'. + vec model; // If problem is solved, this vector contains the model (if any). + int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything +}; + + +//================================================================================================= +#endif diff --git a/SolverTypes.h b/SolverTypes.h new file mode 100644 index 0000000..26ab335 --- /dev/null +++ b/SolverTypes.h @@ -0,0 +1,61 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + + +#ifndef SolverTypes_h +#define SolverTypes_h + +#ifndef Global_h +#include "Global.h" +#endif + + +//================================================================================================= +// Variables, literals: + + +// NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, +// so that they can be used as array indices. + +typedef int Var; +#define var_Undef (-1) + + +class Lit { + int x; +public: + Lit(void) /* unspecifed value allowed for efficiency */ { } + explicit Lit(Var var, bool sign = false) : x((var+var) + sign) { } + friend Lit operator ~ (Lit p) { Lit q; q.x = p.x ^ 1; return q; } + + friend bool sign (Lit p) { return p.x & 1; } + friend int var (Lit p) { return p.x >> 1; } + friend int index(Lit p) { return p.x; } // A "toInt" method that guarantees small, positive integers suitable for array indexing. + friend Lit toLit(int i) { Lit p; p.x = i; return p; } + + friend bool operator == (Lit p, Lit q) { return index(p) == index(q); } + friend bool operator < (Lit p, Lit q) { return index(p) < index(q); } // '<' guarantees that p, ~p are adjacent in the ordering. +}; + +const Lit lit_Undef(var_Undef, false); // }- Useful special constants. +const Lit lit_Error(var_Undef, true ); // } + + +//================================================================================================= +#endif diff --git a/Sort.h b/Sort.h new file mode 100644 index 0000000..97a8220 --- /dev/null +++ b/Sort.h @@ -0,0 +1,134 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + + +#ifndef Sort_h +#define Sort_h + +//#include + + +//================================================================================================= + + +template +struct LessThan_default { + bool operator () (T x, T y) { return x < y; } +}; + + +//================================================================================================= + + +template +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 static inline void selectionSort(T* array, int size) { + selectionSort(array, size, LessThan_default()); } + + +template +void sort(T* array, int size, LessThan lt, double& seed) +{ + if (size <= 15) + selectionSort(array, size, lt); + + else{ + T pivot = array[irand(seed, size)]; + T tmp; + int i = -1; + int j = size; + + for(;;){ + do i++; while(lt(array[i], pivot)); + do j--; while(lt(pivot, array[j])); + + if (i >= j) break; + + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + + sort(array , i , lt, seed); + sort(&array[i], size-i, lt, seed); + } +} +template void sort(T* array, int size, LessThan lt) { + double seed = 91648253; sort(array, size, lt, seed); } +template static inline void sort(T* array, int size) { + sort(array, size, LessThan_default()); } + + +template +void sortUnique(T* array, int& size, LessThan lt) +{ + int i, j; + T last; + + if (size == 0) return; + + sort(array, size, lt); + + i = 1; + last = array[0]; + for (j = 1; j < size; j++){ + if (lt(last, array[j])){ + last = array[i] = array[j]; + i++; } + } + + size = i; +} +template static inline void sortUnique(T* array, int& size) { + sortUnique(array, size, LessThan_default()); } + + +//================================================================================================= +// For 'vec's: + + +template void sort(vec& v, LessThan lt) { + sort((T*)v, v.size(), lt); } +template void sort(vec& v) { + sort(v, LessThan_default()); } + + +template void sortUnique(vec& v, LessThan lt) { + int size = v.size(); + T* data = v.release(); + sortUnique(data, size, lt); + v.~vec(); + new (&v) vec(data, size); } +template void sortUnique(vec& v) { + sortUnique(v, LessThan_default()); } + + +//================================================================================================= +#endif diff --git a/VarOrder.h b/VarOrder.h new file mode 100644 index 0000000..5df89d2 --- /dev/null +++ b/VarOrder.h @@ -0,0 +1,94 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef VarOrder_h +#define VarOrder_h + +#include "SolverTypes.h" +#include "Heap.h" + +//================================================================================================= + + +struct VarOrder_lt { + const vec& activity; + bool operator () (Var x, Var y) { return activity[x] > activity[y]; } + VarOrder_lt(const vec& act) : activity(act) { } +}; + +class VarOrder { + const vec& assigns; // var->val. Pointer to external assignment table. + const vec& activity; // var->act. Pointer to external activity table. + Heap heap; + double random_seed; // For the internal random number generator + +public: + VarOrder(const vec& ass, const vec& act) : + assigns(ass), activity(act), heap(VarOrder_lt(act)), random_seed(91648253) + { } + + inline void newVar(void); + inline void update(Var x); // Called when variable increased in activity. + inline void undo(Var x); // Called when variable is unassigned and may be selected again. + inline Var select(double random_freq =.0); // Selects a new, unassigned variable (or 'var_Undef' if none exists). +}; + + +void VarOrder::newVar(void) +{ + heap.setBounds(assigns.size()); + heap.insert(assigns.size()-1); +} + + +void VarOrder::update(Var x) +{ + if (heap.inHeap(x)) + heap.increase(x); +} + + +void VarOrder::undo(Var x) +{ + if (!heap.inHeap(x)) + heap.insert(x); +} + + +Var VarOrder::select(double random_var_freq) +{ + // Random decision: + if (drand(random_seed) < random_var_freq){ + Var next = irand(random_seed,assigns.size()); + if (toLbool(assigns[next]) == l_Undef) + return next; + } + + // Activity based decision: + while (!heap.empty()){ + Var next = heap.getmin(); + if (toLbool(assigns[next]) == l_Undef) + return next; + } + + return var_Undef; +} + +//================================================================================================= +#endif diff --git a/compile.sh b/compile.sh new file mode 100755 index 0000000..526d51d --- /dev/null +++ b/compile.sh @@ -0,0 +1,3 @@ +# In case the Makefile doesn't work for you, try this script. + +g++ -ggdb -D DEBUG -O3 Main.C Solver.C Constraints.C VarOrder.C -o minisat