rename charm related files into par_* to distiguish the sequential code in satisfiabi...
authorYanhua YanhuaSunLaptop <yanhuasun@yanhua-suns-macbook-pro.local>
Sun, 28 Mar 2010 19:17:50 +0000 (14:17 -0500)
committerYanhua YanhuaSunLaptop <yanhuasun@yanhua-suns-macbook-pro.local>
Sun, 28 Mar 2010 19:17:50 +0000 (14:17 -0500)
12 files changed:
examples/charm++/satisfiability/mtl/Alg.h [new file with mode: 0644]
examples/charm++/satisfiability/mtl/BasicHeap.h [new file with mode: 0644]
examples/charm++/satisfiability/mtl/BoxedVec.h [new file with mode: 0644]
examples/charm++/satisfiability/mtl/Map.h [new file with mode: 0644]
examples/charm++/satisfiability/mtl/Queue.h [new file with mode: 0644]
examples/charm++/satisfiability/mtl/Sort.h [new file with mode: 0644]
examples/charm++/satisfiability/mtl/Vec.h [new file with mode: 0644]
examples/charm++/satisfiability/mtl/minisatHeap.h [new file with mode: 0644]
examples/charm++/satisfiability/mtl/template.mk [new file with mode: 0644]
examples/charm++/satisfiability/par_Solver.C [new file with mode: 0644]
examples/charm++/satisfiability/par_Solver.h [new file with mode: 0644]
examples/charm++/satisfiability/par_SolverTypes.h [new file with mode: 0644]

diff --git a/examples/charm++/satisfiability/mtl/Alg.h b/examples/charm++/satisfiability/mtl/Alg.h
new file mode 100644 (file)
index 0000000..240962d
--- /dev/null
@@ -0,0 +1,57 @@
+/*******************************************************************************************[Alg.h]
+MiniSat -- Copyright (c) 2003-2006, 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 Alg_h
+#define Alg_h
+
+//=================================================================================================
+// Useful functions on vectors
+
+
+#if 1
+template<class V, class T>
+static inline void remove(V& ts, const T& t)
+{
+    int j = 0;
+    for (; j < ts.size() && ts[j] != t; j++);
+    assert(j < ts.size());
+    for (; j < ts.size()-1; j++) ts[j] = ts[j+1];
+    ts.pop();
+}
+#else
+template<class V, class T>
+static inline void remove(V& ts, const T& t)
+{
+    int j = 0;
+    for (; j < ts.size() && ts[j] != t; j++);
+    assert(j < ts.size());
+    ts[j] = ts.last();
+    ts.pop();
+}
+#endif
+
+template<class V, class T>
+static inline bool find(V& ts, const T& t)
+{
+    int j = 0;
+    for (; j < ts.size() && ts[j] != t; j++);
+    return j < ts.size();
+}
+
+#endif
diff --git a/examples/charm++/satisfiability/mtl/BasicHeap.h b/examples/charm++/satisfiability/mtl/BasicHeap.h
new file mode 100644 (file)
index 0000000..556d98f
--- /dev/null
@@ -0,0 +1,98 @@
+/******************************************************************************************[Heap.h]
+MiniSat -- Copyright (c) 2003-2006, 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 BasicHeap_h
+#define BasicHeap_h
+
+#include "Vec.h"
+
+//=================================================================================================
+// A heap implementation with support for decrease/increase key.
+
+
+template<class Comp>
+class BasicHeap {
+    Comp     lt;
+    vec<int> heap;     // heap of ints
+
+    // 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; }
+
+    inline void percolateUp(int i)
+    {
+        int x = heap[i];
+        while (i != 0 && lt(x, heap[parent(i)])){
+            heap[i]          = heap[parent(i)];
+            i                = parent(i);
+        }
+        heap   [i] = x;
+    }
+
+
+    inline void percolateDown(int i)
+    {
+        int 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];
+            i                = child;
+        }
+        heap[i] = x;
+    }
+
+
+    bool heapProperty(int i) {
+        return i >= heap.size()
+            || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
+
+
+  public:
+    BasicHeap(const C& c) : comp(c) { }
+
+    int  size      ()                     const { return heap.size(); }
+    bool empty     ()                     const { return heap.size() == 0; }
+    int  operator[](int index)            const { return heap[index+1]; }
+    void clear     (bool dealloc = false)       { heap.clear(dealloc); }
+    void insert    (int n)                      { heap.push(n); percolateUp(heap.size()-1); }
+
+
+    int  removeMin() {
+        int r   = heap[0];
+        heap[0] = heap.last();
+        heap.pop();
+        if (heap.size() > 1) percolateDown(0);
+        return r; 
+    }
+
+
+    // DEBUG: consistency checking
+    bool heapProperty() {
+        return heapProperty(1); }
+
+
+    // COMPAT: should be removed
+    int  getmin    ()      { return removeMin(); }
+};
+
+
+//=================================================================================================
+#endif
diff --git a/examples/charm++/satisfiability/mtl/BoxedVec.h b/examples/charm++/satisfiability/mtl/BoxedVec.h
new file mode 100644 (file)
index 0000000..bddf410
--- /dev/null
@@ -0,0 +1,147 @@
+/*******************************************************************************************[Vec.h]
+MiniSat -- Copyright (c) 2003-2006, 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 BoxedVec_h
+#define BoxedVec_h
+
+#include <cstdlib>
+#include <cassert>
+#include <new>
+
+//=================================================================================================
+// Automatically resizable arrays
+//
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T>
+class bvec {
+
+    static inline int imin(int x, int y) {
+        int mask = (x-y) >> (sizeof(int)*8-1);
+        return (x&mask) + (y&(~mask)); }
+
+    static inline int imax(int x, int y) {
+        int mask = (y-x) >> (sizeof(int)*8-1);
+        return (x&mask) + (y&(~mask)); }
+
+    struct Vec_t {
+        int sz;
+        int cap;
+        T   data[0];
+
+        static Vec_t* alloc(Vec_t* x, int size){
+            x = (Vec_t*)realloc((void*)x, sizeof(Vec_t) + sizeof(T)*size);
+            x->cap = size;
+            return x;
+        }
+        
+    };
+
+    Vec_t* ref;
+
+    static const int init_size = 2;
+    static int   nextSize (int current) { return (current * 3 + 1) >> 1; }
+    static int   fitSize  (int needed)  { int x; for (x = init_size; needed > x; x = nextSize(x)); return x; }
+
+    void fill (int size) {
+        assert(ref != NULL);
+        for (T* i = ref->data; i < ref->data + size; i++)
+            new (i) T();
+    }
+
+    void fill (int size, const T& pad) {
+        assert(ref != NULL);
+        for (T* i = ref->data; i < ref->data + size; i++)
+            new (i) T(pad);
+    }
+
+    // Don't allow copying (error prone):
+    altvec<T>&  operator = (altvec<T>& other) { assert(0); }
+    altvec (altvec<T>& other)                  { assert(0); }
+
+public:
+    void     clear  (bool dealloc = false) { 
+        if (ref != NULL){
+            for (int i = 0; i < ref->sz; i++) 
+                (*ref).data[i].~T();
+
+            if (dealloc) { 
+                free(ref); ref = NULL; 
+            }else 
+                ref->sz = 0;
+        } 
+    }
+
+    // Constructors:
+    altvec(void)                   : ref (NULL) { }
+    altvec(int size)               : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size);      ref->sz = size; }
+    altvec(int size, const T& pad) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size, pad); ref->sz = size; }
+   ~altvec(void) { clear(true); }
+
+    // Ownership of underlying array:
+    operator T*       (void)           { return ref->data; }     // (unsafe but convenient)
+    operator const T* (void) const     { return ref->data; }
+
+    // Size operations:
+    int      size   (void) const       { return ref != NULL ? ref->sz : 0; }
+
+    void     pop    (void)             { assert(ref != NULL && ref->sz > 0); int last = --ref->sz; ref->data[last].~T(); }
+    void     push   (const T& elem) {
+        int size = ref != NULL ? ref->sz  : 0;
+        int cap  = ref != NULL ? ref->cap : 0;
+        if (size == cap){
+            cap = cap != 0 ? nextSize(cap) : init_size;
+            ref = Vec_t::alloc(ref, cap); 
+        }
+        //new (&ref->data[size]) T(elem); 
+        ref->data[size] = elem; 
+        ref->sz = size+1; 
+    }
+
+    void     push   () {
+        int size = ref != NULL ? ref->sz  : 0;
+        int cap  = ref != NULL ? ref->cap : 0;
+        if (size == cap){
+            cap = cap != 0 ? nextSize(cap) : init_size;
+            ref = Vec_t::alloc(ref, cap); 
+        }
+        new (&ref->data[size]) T(); 
+        ref->sz = size+1; 
+    }
+
+    void     shrink (int nelems)             { for (int i = 0; i < nelems; i++) pop(); }
+    void     shrink_(int nelems)             { for (int i = 0; i < nelems; i++) pop(); }
+    void     growTo (int size)               { while (this->size() < size) push(); }
+    void     growTo (int size, const T& pad) { while (this->size() < size) push(pad); }
+    void     capacity (int size)             { growTo(size); }
+
+    const T& last  (void) const              { return ref->data[ref->sz-1]; }
+    T&       last  (void)                    { return ref->data[ref->sz-1]; }
+
+    // Vector interface:
+    const T& operator [] (int index) const  { return ref->data[index]; }
+    T&       operator [] (int index)        { return ref->data[index]; }
+
+    void copyTo(altvec<T>& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); }
+    void moveTo(altvec<T>& dest) { dest.clear(true); dest.ref = ref; ref = NULL; }
+
+};
+
+
+#endif
diff --git a/examples/charm++/satisfiability/mtl/Map.h b/examples/charm++/satisfiability/mtl/Map.h
new file mode 100644 (file)
index 0000000..b6d76a3
--- /dev/null
@@ -0,0 +1,118 @@
+/*******************************************************************************************[Map.h]
+MiniSat -- Copyright (c) 2003-2006, 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 Map_h
+#define Map_h
+
+#include <stdint.h>
+
+#include "Vec.h"
+
+//=================================================================================================
+// 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; } };
+
+//=================================================================================================
+// 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 {
+    struct Pair { K key; D data; };
+
+    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) { assert(0); }
+                   Map        (Map<K,D,H,E>& other) { assert(0); }
+
+    int32_t index  (const K& k) const { return hash(k) % cap; }
+    void   _insert (const K& k, const D& d) { table[index(k)].push(); table[index(k)].last().key = k; table[index(k)].last().data = d; }
+    void    rehash () {
+        const vec<Pair>* old = table;
+
+        int newsize = primes[0];
+        for (int i = 1; newsize <= cap && i < nprimes; i++)
+           newsize = primes[i];
+
+        table = new vec<Pair>[newsize];
+
+        for (int i = 0; i < cap; i++){
+            for (int j = 0; j < old[i].size(); j++){
+                _insert(old[i][j].key, old[i][j].data); }}
+
+        delete [] old;
+
+        cap = newsize;
+    }
+
+    
+    public:
+
+     Map () : table(NULL), cap(0), size(0) {}
+     Map (const H& h, const E& e) : Map(), hash(h), equals(e) {}
+    ~Map () { delete [] table; }
+
+    void insert (const K& k, const D& d) { if (size+1 > cap / 2) rehash(); _insert(k, d); size++; }
+    bool peek   (const K& k, D& d) {
+        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;
+    }
+
+    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();
+    }
+
+    void clear  () {
+        cap = size = 0;
+        delete [] table;
+        table = NULL;
+    }
+};
+
+#endif
diff --git a/examples/charm++/satisfiability/mtl/Queue.h b/examples/charm++/satisfiability/mtl/Queue.h
new file mode 100644 (file)
index 0000000..2cc110c
--- /dev/null
@@ -0,0 +1,82 @@
+/*****************************************************************************************[Queue.h]
+MiniSat -- Copyright (c) 2003-2006, 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
+
+#include "Vec.h"
+
+//=================================================================================================
+
+
+template <class T>
+class Queue {
+    vec<T>  elems;
+    int     first;
+
+public:
+    Queue(void) : first(0) { }
+
+    void insert(T x)   { elems.push(x); }
+    T    peek  () const { return elems[first]; }
+    void pop   () { first++; }
+
+    void clear(bool dealloc = false)   { elems.clear(dealloc); 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; }
+
+    const T& operator [] (int index) const  { return elems[first + index]; }
+
+};
+
+//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 () { buf.shrinkTo(1); first = end = 0; }
+//    int  size  () { return (end >= first) ? end - first : end - first + buf.size(); }
+//
+//    T    peek  () { 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/examples/charm++/satisfiability/mtl/Sort.h b/examples/charm++/satisfiability/mtl/Sort.h
new file mode 100644 (file)
index 0000000..1f301f5
--- /dev/null
@@ -0,0 +1,93 @@
+/******************************************************************************************[Sort.h]
+MiniSat -- Copyright (c) 2003-2006, 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 "Vec.h"
+
+//=================================================================================================
+// Some sorting algorithms for vec's
+
+
+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/examples/charm++/satisfiability/mtl/Vec.h b/examples/charm++/satisfiability/mtl/Vec.h
new file mode 100644 (file)
index 0000000..e780aa1
--- /dev/null
@@ -0,0 +1,133 @@
+/*******************************************************************************************[Vec.h]
+MiniSat -- Copyright (c) 2003-2006, 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 Vec_h
+#define Vec_h
+
+#include <cstdlib>
+#include <cassert>
+#include <new>
+
+//=================================================================================================
+// Automatically resizable arrays
+//
+// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
+
+template<class T>
+class vec {
+    T*  data;
+    int sz;
+    int cap;
+
+    void     init(int size, const T& pad);
+    void     grow(int min_cap);
+
+    // Don't allow copying (error prone):
+    vec<T>&  operator = (vec<T>& other) { assert(0); return *this; }
+             vec        (vec<T>& other) { assert(0); }
+
+    static inline int imin(int x, int y) {
+        int mask = (x-y) >> (sizeof(int)*8-1);
+        return (x&mask) + (y&(~mask)); }
+
+    static inline int imax(int x, int y) {
+        int mask = (y-x) >> (sizeof(int)*8-1);
+        return (x&mask) + (y&(~mask)); }
+
+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 'free()')
+   ~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     shrink_(int nelems)       { assert(nelems <= sz); sz -= nelems; }
+    void     pop    (void)             { sz--, data[sz].~T(); }
+    void     growTo (int size);
+    void     growTo (int size, const T& pad);
+    void     clear  (bool dealloc = false);
+    void     capacity (int size) { grow(size); }
+
+    // Stack interface:
+#if 1
+    void     push  (void)              { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; }
+    //void     push  (const T& elem)     { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; }
+    void     push  (const T& elem)     { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; }
+    void     push_ (const T& elem)     { assert(sz < cap); data[sz++] = elem; }
+#else
+    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++; }
+#endif
+
+    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]; }
+
+
+    // Duplicatation (preferred instead):
+    void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (&copy[i]) T(data[i]); }
+    void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
+};
+
+template<class T>
+void vec<T>::grow(int min_cap) {
+    if (min_cap <= cap) return;
+    if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2;
+    else          do cap = (cap*3+1) >> 1; while (cap < min_cap);
+    data = (T*)realloc(data, cap * sizeof(T)); }
+
+template<class T>
+void vec<T>::growTo(int size, const T& pad) {
+    if (sz >= size) return;
+    grow(size);
+    for (int i = sz; i < size; i++) new (&data[i]) T(pad);
+    sz = size; }
+
+template<class T>
+void vec<T>::growTo(int size) {
+    if (sz >= size) return;
+    grow(size);
+    for (int i = sz; i < size; i++) new (&data[i]) T();
+    sz = size; }
+
+template<class T>
+void vec<T>::clear(bool dealloc) {
+    if (data != NULL){
+        for (int i = 0; i < sz; i++) data[i].~T();
+        sz = 0;
+        if (dealloc) free(data), data = NULL, cap = 0; } }
+
+
+#endif
diff --git a/examples/charm++/satisfiability/mtl/minisatHeap.h b/examples/charm++/satisfiability/mtl/minisatHeap.h
new file mode 100644 (file)
index 0000000..6cb66cc
--- /dev/null
@@ -0,0 +1,169 @@
+/******************************************************************************************[Heap.h]
+MiniSat -- Copyright (c) 2003-2006, 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 minisatHeap_h
+#define minisatHeap_h
+
+#include "Vec.h"
+
+//=================================================================================================
+// A heap implementation with support for decrease/increase key.
+
+
+template<class Comp>
+class Heap {
+    Comp     lt;
+    vec<int> heap;     // heap of ints
+    vec<int> indices;  // int -> index in heap
+
+    // 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; }
+
+
+    inline void percolateUp(int i)
+    {
+        int x = heap[i];
+        while (i != 0 && lt(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() && 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;
+    }
+
+
+    bool heapProperty (int i) const {
+        return i >= heap.size()
+            || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); }
+
+
+  public:
+    Heap(const Comp& c) : lt(c) { }
+
+    int  size      ()          const { return heap.size(); }
+    bool empty     ()          const { return heap.size() == 0; }
+    bool inHeap    (int n)     const { return n < indices.size() && indices[n] >= 0; }
+    int  operator[](int index) const { assert(index < heap.size()); return heap[index]; }
+
+    void decrease  (int n) { assert(inHeap(n)); percolateUp(indices[n]); }
+
+    // RENAME WHEN THE DEPRECATED INCREASE IS REMOVED.
+    void increase_ (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+
+
+    void insert(int n)
+    {
+        indices.growTo(n+1, -1);
+        assert(!inHeap(n));
+
+        indices[n] = heap.size();
+        heap.push(n);
+        percolateUp(indices[n]); 
+    }
+
+
+    int  removeMin()
+    {
+        int x            = heap[0];
+        heap[0]          = heap.last();
+        indices[heap[0]] = 0;
+        indices[x]       = -1;
+        heap.pop();
+        if (heap.size() > 1) percolateDown(0);
+        return x; 
+    }
+
+
+    void clear(bool dealloc = false) 
+    { 
+        for (int i = 0; i < heap.size(); i++)
+            indices[heap[i]] = -1;
+#ifdef NDEBUG
+        for (int i = 0; i < indices.size(); i++)
+            assert(indices[i] == -1);
+#endif
+        heap.clear(dealloc); 
+    }
+
+
+    // Fool proof variant of insert/decrease/increase
+    void update (int n)
+    {
+        if (!inHeap(n))
+            insert(n);
+        else {
+            percolateUp(indices[n]);
+            percolateDown(indices[n]);
+        }
+    }
+
+
+    // Delete elements from the heap using a given filter function (-object).
+    // *** this could probaly be replaced with a more general "buildHeap(vec<int>&)" method ***
+    template <class F>
+    void filter(const F& filt) {
+        int i,j;
+        for (i = j = 0; i < heap.size(); i++)
+            if (filt(heap[i])){
+                heap[j]          = heap[i];
+                indices[heap[i]] = j++;
+            }else
+                indices[heap[i]] = -1;
+
+        heap.shrink(i - j);
+        for (int i = heap.size() / 2 - 1; i >= 0; i--)
+            percolateDown(i);
+
+        assert(heapProperty());
+    }
+
+
+    // DEBUG: consistency checking
+    bool heapProperty() const {
+        return heapProperty(1); }
+
+
+    // COMPAT: should be removed
+    void setBounds (int n) { }
+    void increase  (int n) { decrease(n); }
+    int  getmin    ()      { return removeMin(); }
+
+};
+
+
+//=================================================================================================
+#endif
diff --git a/examples/charm++/satisfiability/mtl/template.mk b/examples/charm++/satisfiability/mtl/template.mk
new file mode 100644 (file)
index 0000000..15f023f
--- /dev/null
@@ -0,0 +1,90 @@
+##
+##  Template makefile for Standard, Profile, Debug, Release, and Release-static versions
+##
+##    eg: "make rs" for a statically linked release version.
+##        "make d"  for a debug version (no optimizations).
+##        "make"    for the standard version (optimized, but with debug information and assertions active)
+
+CSRCS     ?= $(wildcard *.C)
+CHDRS     ?= $(wildcard *.h)
+COBJS     ?= $(addsuffix .o, $(basename $(CSRCS)))
+
+PCOBJS     = $(addsuffix p,  $(COBJS))
+DCOBJS     = $(addsuffix d,  $(COBJS))
+RCOBJS     = $(addsuffix r,  $(COBJS))
+
+EXEC      ?= $(notdir $(shell pwd))
+LIB       ?= $(EXEC)
+
+CXX       ?= g++
+CFLAGS    ?= -Wall
+LFLAGS    ?= -Wall
+
+COPTIMIZE ?= -O3
+
+.PHONY : s p d r rs lib libd clean 
+
+s:     $(EXEC)
+p:     $(EXEC)_profile
+d:     $(EXEC)_debug
+r:     $(EXEC)_release
+rs:    $(EXEC)_static
+lib:   lib$(LIB).a
+libd:  lib$(LIB)d.a
+
+## Compile options
+%.o:                   CFLAGS +=$(COPTIMIZE) -ggdb -D DEBUG
+%.op:                  CFLAGS +=$(COPTIMIZE) -pg -ggdb -D NDEBUG
+%.od:                  CFLAGS +=-O0 -ggdb -D DEBUG # -D INVARIANTS
+%.or:                  CFLAGS +=$(COPTIMIZE) -D NDEBUG
+
+## Link options
+$(EXEC):               LFLAGS := -ggdb $(LFLAGS)
+$(EXEC)_profile:       LFLAGS := -ggdb -pg $(LFLAGS)
+$(EXEC)_debug:         LFLAGS := -ggdb $(LFLAGS)
+$(EXEC)_release:       LFLAGS := $(LFLAGS)
+$(EXEC)_static:                LFLAGS := --static $(LFLAGS)
+
+## Dependencies
+$(EXEC):               $(COBJS)
+$(EXEC)_profile:       $(PCOBJS)
+$(EXEC)_debug:         $(DCOBJS)
+$(EXEC)_release:       $(RCOBJS)
+$(EXEC)_static:                $(RCOBJS)
+
+lib$(LIB).a:   $(filter-out Main.or, $(RCOBJS))
+lib$(LIB)d.a:  $(filter-out Main.od, $(DCOBJS))
+
+
+## Build rule
+%.o %.op %.od %.or:    %.C
+       @echo Compiling: "$@ ( $< )"
+       @$(CXX) $(CFLAGS) -c -o $@ $<
+
+## Linking rules (standard/profile/debug/release)
+$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
+       @echo Linking: "$@ ( $^ )"
+       @$(CXX) $^ $(LFLAGS) -o $@
+
+## Library rule
+lib$(LIB).a lib$(LIB)d.a:
+       @echo Library: "$@ ( $^ )"
+       @rm -f $@
+       @ar cq $@ $^
+
+## Clean rule
+clean:
+       @rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
+         $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mak lib$(LIB).a lib$(LIB)d.a
+
+## Make dependencies
+depend.mk: $(CSRCS) $(CHDRS)
+       @echo Making dependencies ...
+       @$(CXX) $(CFLAGS) -MM $(CSRCS) > depend.mk
+       @cp depend.mk /tmp/depend.mk.tmp
+       @sed "s/o:/op:/" /tmp/depend.mk.tmp >> depend.mk
+       @sed "s/o:/od:/" /tmp/depend.mk.tmp >> depend.mk
+       @sed "s/o:/or:/" /tmp/depend.mk.tmp >> depend.mk
+       @rm /tmp/depend.mk.tmp
+
+-include depend.mk
diff --git a/examples/charm++/satisfiability/par_Solver.C b/examples/charm++/satisfiability/par_Solver.C
new file mode 100644 (file)
index 0000000..71d55ef
--- /dev/null
@@ -0,0 +1,552 @@
+#include "main.decl.h"
+#include "par_SolverTypes.h"
+#include "par_Solver.h"
+#include "Solver.h"
+#include <map>
+#include <vector>
+
+using namespace std;
+
+extern CProxy_Main mainProxy;
+extern int grainsize;
+
+par_SolverState::par_SolverState()
+{
+    unsolved_clauses = 0; 
+    var_frequency = 0;
+}
+
+inline int par_SolverState::nVars()
+{
+    return var_frequency; 
+}
+
+int par_SolverState::clausesSize()
+{
+    return clauses.size();
+}
+int par_SolverState::newVar(bool sign, bool dvar)
+{
+    int v = nVars();
+    var_frequency++;
+    return v;
+}
+
+void par_SolverState::attachClause(par_Clause& c)
+{
+
+}
+
+int par_SolverState::unsolvedClauses()
+{
+    int unsolved = 0;
+    for(int i=0; i< clauses.size(); i++)
+    {
+        if(clauses[i].size() > 0)
+            unsolved++;
+    }
+
+    return unsolved;
+}
+
+void par_SolverState::printSolution()
+{
+    for(int _i=0; _i<var_size; _i++)
+    {
+        CkPrintf("%d\n", occurrence[_i]);
+    }
+}
+
+/* add clause, before adding, check unit conflict */
+bool par_SolverState::addClause(CkVec<par_Lit>& ps)
+{
+    /*TODO precheck is needed here */
+    if(ps.size() == 1)//unit clause
+    {
+        for(int _i=0; _i<unit_clause_index.size(); _i++)
+        {
+            int index = unit_clause_index[_i];
+
+            par_Clause unit = clauses[index];
+            par_Lit     unit_lit = unit[0];
+
+            if(unit_lit == ~ps[0])
+            {
+   
+                CkPrintf("clause conflict between %d and %d\n", index, clauses.size());
+                return false;
+            }
+            /*else if(unit_lit == ps[0])
+            {
+                return true;
+            }*/
+        }
+       /* all unit clauses are checked, no repeat, no conflict */
+        unit_clause_index.push_back(clauses.size());
+    }else{
+    //check whether the clause is already satisfiable in any case
+    /* if x and ~x exist in the same clause, this clause is already satisfiable, we do not have to deal with it */
+   
+    for(int i=0; i< ps.size(); i++)
+    {
+        par_Lit lit = ps[i];
+
+        for(int j=0; j<i; j++)
+        {
+            if(lit == ~ps[j])
+            {
+                CkPrintf("This clause is already satisfiable\n");
+                for(int _i=0; _i<ps.size(); _i++)
+                {
+                   occurrence[abs(toInt(ps[_i])-1)]--; 
+                   if(toInt(ps[_i]) > 0)
+                       positive_occurrence[abs(toInt(ps[_i])-1)]--; 
+                }
+                return true;
+            }
+        }
+    }
+    }
+    clauses.push_back(par_Clause());
+    clauses[clauses.size()-1].attachdata(ps, false);
+    unsolved_clauses++;
+    // build the linklist for each literal pointing to the clause, where the literal occurs
+    for(int i=0; i< ps.size(); i++)
+    {
+        par_Lit lit = ps[i];
+
+        if(toInt(lit) > 0)
+            whichClauses[2*toInt(lit)-2].push_back(clauses.size()-1);
+        else
+            whichClauses[-2*toInt(lit)-1].push_back(clauses.size()-1);
+
+    }
+
+    return true;
+}
+
+void par_SolverState::assignclause(CkVec<par_Clause>& cls )
+{
+    clauses.removeAll();
+    for(int i=0; i<cls.size(); i++)
+    {
+        clauses.push_back( cls[i]);
+    }
+}
+
+/* *********** Solver chare */
+
+mySolver::mySolver(par_SolverState* state_msg)
+{
+
+    /* Which variable get assigned  */
+    par_Lit lit = state_msg->assigned_lit;
+#ifdef DEBUG    
+    CkPrintf("\n\nNew chare: literal = %d, occurrence size=%d, level=%d \n", toInt(lit), state_msg->occurrence.size(), state_msg->level);
+#endif    
+    par_SolverState *next_state = copy_solverstate(state_msg);
+    
+    //Unit clauses
+    /* use this value to propagate the clauses */
+    // deal with the clauses where this literal is
+    int _unit_ = -1;
+    while(1){
+        int pp_ = 1;
+        int pp_i_ = 2;
+        int pp_j_ = 1;
+
+        if(toInt(lit) < 0)
+        {
+            pp_ = -1;
+            pp_i_ = 1;
+            pp_j_ = 2;
+        }
+
+        next_state->occurrence[pp_*toInt(lit)-1] = -pp_i_;
+    
+        //CkPrintf(" index=%d, total size=%d, original msg size=%d\n", pp_*2*toInt(lit)-pp_i_, next_state->whichClauses.size(), state_msg->whichClauses.size());
+
+        CkVec<int> &inClauses = next_state->whichClauses[pp_*2*toInt(lit)-pp_i_];
+        CkVec<int> &inClauses_opposite = next_state->whichClauses[pp_*2*toInt(lit)-pp_j_];
+
+    // literal with same sign, remove all these clauses
+       for(int j=0; j<inClauses.size(); j++)
+       {
+           int cl_index = inClauses[j];
+
+           par_Clause& cl_ = next_state->clauses[cl_index];
+           //for all the literals in this clauses, the occurrence decreases by 1
+           for(int k=0; k< cl_.size(); k++)
+           {
+               par_Lit lit_ = cl_[k];
+               if(toInt(lit_) == toInt(lit))
+                   continue;
+               next_state->occurrence[abs(toInt(lit_)) - 1]--;
+               if(toInt(lit_) > 0)
+               {
+                   next_state->positive_occurrence[toInt(lit_)-1]--;
+                   //remove the clause index for the literal
+                   for(int _i = 0; _i<next_state->whichClauses[2*toInt(lit_)-2].size(); _i++)
+                   {
+                       if(next_state->whichClauses[2*toInt(lit_)-2][_i] == cl_index)
+                       {
+                           next_state->whichClauses[2*toInt(lit_)-2].remove(_i);
+                           break;
+                       }
+                   }
+               }else
+               {
+                   for(int _i = 0; _i<next_state->whichClauses[-2*toInt(lit_)-1].size(); _i++)
+                   {
+                       if(next_state->whichClauses[-2*toInt(lit_)-1][_i] == cl_index)
+                       {
+                           next_state->whichClauses[-2*toInt(lit_)-1].remove(_i);
+                           break;
+                       }
+                   }
+               }
+           } //finish dealing with all literal in the clause
+           next_state->clauses[cl_index].resize(0);
+       } //finish dealing with clauses where the literal occur the same
+       /* opposite to the literal */
+       for(int j=0; j<inClauses_opposite.size(); j++)
+       {
+           int cl_index_ = inClauses_opposite[j];
+           par_Clause& cl_neg = next_state->clauses[cl_index_];
+           cl_neg.remove(-toInt(lit));
+
+           /*becomes a unit clause */
+           if(cl_neg.size() == 1)
+           {
+               next_state->unit_clause_index.push_back(cl_index_);
+           }else if (cl_neg.size() == 0)
+           {
+               return;
+           }
+       }
+
+       _unit_++;
+       if(_unit_ == next_state->unit_clause_index.size())
+           break;
+       par_Clause cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
+
+       while(cl.size() == 0){
+           _unit_++;
+           if(_unit_ == next_state->unit_clause_index.size())
+               break;
+           cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
+       };
+
+       if(_unit_ == next_state->unit_clause_index.size())
+           break;
+       lit = cl[0];
+    }
+    /***************/
+
+    int unsolved = next_state->unsolvedClauses();
+    if(unsolved == 0)
+    {
+        CkPrintf("One solution found in parallel processing \n");
+        //next_state->printSolution();
+        mainProxy.done(next_state->occurrence);
+        return;
+    }
+    int max_index = get_max_element(next_state->occurrence);
+#ifdef DEBUG
+    CkPrintf("max index = %d\n", max_index);
+#endif
+    //if() left literal unassigned is larger than a grain size, parallel 
+    ///* When we start sequential 3SAT Grainsize problem*/
+   
+    /* the other branch */
+    par_SolverState *new_msg2 = copy_solverstate(next_state);;
+
+    next_state->level = state_msg->level+1;
+
+    int lower = state_msg->lower;
+    int higher = state_msg->higher;
+    int middle = (lower+higher)/2;
+    int positive_max = next_state->positive_occurrence[max_index];
+    if(positive_max >= next_state->occurrence[max_index] - positive_max)
+    {
+        next_state->assigned_lit = par_Lit(max_index+1);
+        next_state->occurrence[max_index] = -2;
+    }
+    else
+    {
+        next_state->assigned_lit = par_Lit(-max_index-1);
+        next_state->occurrence[max_index] = -1;
+    }
+    bool satisfiable_1 = true;
+
+    if(unsolved > grainsize)
+    {
+        next_state->lower = lower + 1;
+        next_state->higher = middle;
+        *((int *)CkPriorityPtr(next_state)) = lower+1;
+        CkSetQueueing(next_state, CK_QUEUEING_IFIFO);
+        CProxy_mySolver::ckNew(next_state);
+    }
+    else //sequential
+    {
+        Solver      S;
+        S.verbosity = 1;
+        /* This code is urgly. Need to revise it later. Convert par data structure to sequential 
+         */
+        vector< vector<int> > seq_clauses;
+        //seq_clauses.resize(next_state->clauses.size());
+        for(int _i_=0; _i_<next_state->clauses.size(); _i_++)
+        {
+            if(next_state->clauses[_i_].size() > 0)
+            {
+                vector<int> unsolvedclaus;
+                par_Clause& cl = next_state->clauses[_i_];
+                unsolvedclaus.resize(cl.size());
+                for(int _j_=0; _j_<cl.size(); _j_++)
+                {
+                    unsolvedclaus[_j_] = toInt(cl[_j_]);
+                }
+                seq_clauses.push_back(unsolvedclaus);
+            }
+        }
+        satisfiable_1 = S.seq_processing(seq_clauses);//seq_solve(next_state);
+        if(satisfiable_1)
+        {
+            CkPrintf("One solution found by sequential processing \n");
+            mainProxy.done(next_state->occurrence);
+            return;
+        }
+    }
+
+    new_msg2->level = state_msg->level+1;
+    if(positive_max >= new_msg2->occurrence[max_index] - positive_max)
+    {
+        new_msg2->assigned_lit = par_Lit(-max_index-1);
+        new_msg2->occurrence[max_index] = -1;
+    }
+    else
+    {
+        new_msg2->assigned_lit = par_Lit(max_index+1);
+        new_msg2->occurrence[max_index] = -2;
+    }
+    unsolved = new_msg2->unsolvedClauses();
+    if(unsolved > grainsize)
+    {
+        new_msg2->lower = middle + 1;
+        new_msg2->higher = higher-1;
+        *((int *)CkPriorityPtr(new_msg2)) = middle+1;
+        CkSetQueueing(new_msg2, CK_QUEUEING_IFIFO);
+        CProxy_mySolver::ckNew(new_msg2);
+    }
+    else
+    {
+        Solver      S;
+        S.verbosity = 1;
+       
+        vector< vector<int> > seq_clauses;
+        for(int _i_=0; _i_<new_msg2->clauses.size(); _i_++)
+        {
+            par_Clause& cl = new_msg2->clauses[_i_];
+            if(cl.size() > 0)
+            {
+                vector<int> unsolvedclaus;
+                unsolvedclaus.resize(cl.size());
+                for(int _j_=0; _j_<cl.size(); _j_++)
+                {
+                    unsolvedclaus[_j_] = toInt(cl[_j_]);
+                }
+                seq_clauses.push_back(unsolvedclaus);
+            }
+        }
+
+        bool ret = S.seq_processing(seq_clauses);//seq_solve(next_state);
+        //bool ret = Solver::seq_processing(new_msg2->clauses);//seq_solve(new_msg2);
+        if(ret)
+        {
+            CkPrintf("One solution found by sequential processing \n");
+            mainProxy.done(new_msg2->occurrence);
+        }
+        return;
+    }
+
+}
+
+/* Which literals are already assigned, which is assigned this interation, the unsolved clauses */
+/* should all these be passed as function parameters */
+/* solve the 3sat in sequence */
+
+long long int computes = 0;
+bool mySolver::seq_solve(par_SolverState* state_msg)
+{
+    /* Which variable get assigned  */
+    par_Lit lit = state_msg->assigned_lit;
+       
+#ifdef DEBUG
+    CkPrintf("\n\n Computes=%d Sequential SAT New chare: literal = %d,  level=%d, unsolved clauses=%d\n", computes++, toInt(assigned_var), state_msg->level, state_msg->clauses.size());
+    //CkPrintf("\n\n Computes=%d Sequential SAT New chare: literal = %d, occurrence size=%d, level=%d \n", computes++, toInt(assigned_var), state_msg->occurrence.size(), state_msg->level);
+#endif
+    par_SolverState *next_state = copy_solverstate(state_msg);
+    
+    //Unit clauses
+    /* use this value to propagate the clauses */
+#ifdef DEBUG
+    CkPrintf(" remainning clause size is %d\n", (state_msg->clauses).size());
+#endif
+
+    int _unit_ = -1;
+    while(1){
+    int pp_ = 1;
+    int pp_i_ = 2;
+    int pp_j_ = 1;
+
+    if(toInt(lit) < 0)
+    {
+        pp_ = -1;
+        pp_i_ = 1;
+        pp_j_ = 2;
+    }
+
+    next_state->occurrence[pp_*toInt(lit)-1] = -pp_i_;
+    
+    CkVec<int> &inClauses = next_state->whichClauses[pp_*2*toInt(lit)-pp_i_];
+    CkVec<int> &inClauses_opposite = next_state->whichClauses[pp_*2*toInt(lit)-pp_j_];
+
+    // literal with same sign, remove all these clauses
+    for(int j=0; j<inClauses.size(); j++)
+    {
+        int cl_index = inClauses[j];
+
+        par_Clause& cl_ = next_state->clauses[cl_index];
+        //for all the literals in this clauses, the occurrence decreases by 1
+        for(int k=0; k< cl_.size(); k++)
+        {
+            par_Lit lit_ = cl_[k];
+            if(toInt(lit_) == toInt(lit))
+                continue;
+            next_state->occurrence[abs(toInt(lit_)) - 1]--;
+            if(toInt(lit_) > 0)
+            {
+                next_state->positive_occurrence[toInt(lit_)-1]--;
+                //remove the clause index for the literal
+                for(int _i = 0; _i<next_state->whichClauses[2*toInt(lit_)-2].size(); _i++)
+                {
+                    if(next_state->whichClauses[2*toInt(lit_)-2][_i] == cl_index)
+                    {
+                        next_state->whichClauses[2*toInt(lit_)-2].remove(_i);
+                        break;
+                    }
+                }
+            }else
+            {
+                for(int _i = 0; _i<next_state->whichClauses[-2*toInt(lit_)-1].size(); _i++)
+                {
+                    if(next_state->whichClauses[-2*toInt(lit_)-1][_i] == cl_index)
+                    {
+                        next_state->whichClauses[-2*toInt(lit_)-1].remove(_i);
+                        break;
+                    }
+                }
+            }
+        }
+            next_state->clauses[cl_index].resize(0);
+    }
+   
+    for(int j=0; j<inClauses_opposite.size(); j++)
+    {
+        int cl_index_ = inClauses_opposite[j];
+        par_Clause& cl_neg = next_state->clauses[cl_index_];
+        cl_neg.remove(-toInt(lit));
+            //becomes a unit clause
+         if(cl_neg.size() == 1)
+         {
+             next_state->unit_clause_index.push_back(cl_index_);
+         }else if (cl_neg.size() == 0)
+         {
+                return false;
+         }
+    }
+   
+    _unit_++;
+    if(_unit_ == next_state->unit_clause_index.size())
+        break;
+    par_Clause cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
+    
+    while(cl.size() == 0){
+        _unit_++;
+        if(_unit_ == next_state->unit_clause_index.size())
+            break;
+        cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
+        
+    };
+
+    if(_unit_ == next_state->unit_clause_index.size())
+        break;
+    
+    lit = cl[0];
+    }
+   
+    int unsolved = next_state->unsolvedClauses();
+    if(unsolved == 0)
+    {
+        CkPrintf("One solution found in sequential processing, check the output file for assignment\n");
+        mainProxy.done(next_state->occurrence);
+        return true;
+    }
+    
+    /**********************/
+    
+        /* it would be better to insert the unit literal in order of their occurrence */
+        /* make a decision and then fire new tasks */
+        /* if there is unit clause, should choose these first??? TODO */
+        /* TODO which variable to pick up */
+        /*unit clause literal and also which occurrs most times */
+        int max_index =  get_max_element(next_state->occurrence);
+#ifdef DEBUG
+        CkPrintf("max index = %d\n", max_index);
+#endif
+        next_state->level = state_msg->level+1;
+
+        par_SolverState *new_msg2 = copy_solverstate(next_state);;
+        
+        int positive_max = next_state->positive_occurrence[max_index];
+        if(positive_max >= next_state->occurrence[max_index] - positive_max)
+        {
+            next_state->occurrence[max_index] = -2;
+            next_state->assigned_lit = par_Lit(max_index+1);
+        }
+        else
+        {
+            next_state->occurrence[max_index] = -1;
+            next_state->assigned_lit = par_Lit(-max_index-1);
+        } 
+
+        bool   satisfiable_1 = seq_solve(next_state);
+        if(satisfiable_1)
+        {
+            return true;
+        }
+        
+        new_msg2->level = state_msg->level+1;
+       
+        if(positive_max >= next_state->occurrence[max_index] - positive_max)
+        {
+            new_msg2->occurrence[max_index] = -1;
+            new_msg2->assigned_lit = par_Lit(-max_index-1);
+        }
+        else
+        {
+            new_msg2->occurrence[max_index] = -2;
+            new_msg2->assigned_lit = par_Lit(max_index+1);
+        } 
+            
+        bool satisfiable_0 = seq_solve(new_msg2);
+        if(satisfiable_0)
+        {
+            return true;
+        }
+
+        //CkPrintf("Unsatisfiable through sequential\n");
+        return false;
+
+}
diff --git a/examples/charm++/satisfiability/par_Solver.h b/examples/charm++/satisfiability/par_Solver.h
new file mode 100644 (file)
index 0000000..83b7b74
--- /dev/null
@@ -0,0 +1,103 @@
+#ifndef _PAR_SOLVER_H
+#define _PAR_SOLVER_H
+
+class par_SolverState : public CMessage_par_SolverState {
+
+private:
+
+public:
+
+    
+    par_SolverState();
+
+    int nVars();
+
+    int clausesSize();
+    
+    int newVar (bool polarity = true, bool dvar = true);
+    
+    bool addClause(CkVec<par_Lit>& lits);
+
+    void attachClause(par_Clause& c);
+
+    void assignclause(CkVec<par_Clause>& );
+
+    int  unsolvedClauses();
+    
+    void printSolution();
+
+    CkVec<par_Clause>   clauses;
+    par_Lit             assigned_lit;
+    int             var_size;
+    int             unsolved_clauses;
+
+    int             var_frequency; // 1, -1, 1 freq = 3
+    CkVec<int>      unit_clause_index;
+    // -2 means true, -1 means false, 0 means anything, > 0 means occurrence
+    CkVec<int>      occurrence; 
+    CkVec<int>      positive_occurrence; 
+    //2 * N (positive, negative)
+    CkVec< CkVec< int > >   whichClauses;
+    int             level;
+   
+    int             lower;
+    int             higher;
+
+    //CkVec<Lit>      lit_state;
+    //vector<Lit> assigns;
+
+    /*
+    void pup(PUP::er &p) {
+    
+        p|assigns;
+        p|clauses;
+        p|assigned_lit;
+    }*/
+
+    friend par_SolverState* copy_solverstate( const par_SolverState* org)
+    {
+       par_SolverState *new_state = new (8*sizeof(int))par_SolverState;
+        
+       new_state->clauses.resize(org->clauses.size());
+       for(int _i=0; _i<org->clauses.size(); _i++)
+       {
+           new_state->clauses[_i] = par_Clause(org->clauses[_i]); 
+       }
+
+       new_state->var_size = org->var_size;
+
+       new_state->occurrence.resize(org->occurrence.size());
+       new_state->positive_occurrence.resize(org->occurrence.size());
+       for(int _i=0; _i<org->occurrence.size(); _i++){
+           new_state->occurrence[_i] = org->occurrence[_i];
+           new_state->positive_occurrence[_i] = org->occurrence[_i];
+       }
+       new_state->level = org->level;
+       int _size = org->whichClauses.size();
+       new_state->whichClauses.resize(_size); 
+       for(int i=0; i<_size; i++)
+       {
+           int _sub_size = org->whichClauses[i].size();
+           new_state->whichClauses[i].resize(_sub_size);
+
+           for(int j=0; j<_sub_size; j++)
+           {
+               new_state->whichClauses[i][j] = org->whichClauses[i][j];
+           }
+       }
+       return new_state;
+    }
+
+};
+
+
+class mySolver : public CBase_mySolver {
+
+private:
+
+    bool seq_solve(par_SolverState*);
+public:
+    mySolver(par_SolverState*);
+
+};
+#endif
diff --git a/examples/charm++/satisfiability/par_SolverTypes.h b/examples/charm++/satisfiability/par_SolverTypes.h
new file mode 100644 (file)
index 0000000..0c41302
--- /dev/null
@@ -0,0 +1,218 @@
+/***********************************************************************************[SolverTypes.h]
+MiniSat -- Copyright (c) 2003-2006, 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 _PAR_SolverTypes_h
+#define _PAR_SolverTypes_h
+
+#include <cassert>
+#include <stdint.h>
+
+
+template<class V> 
+int get_max_element(const V& ps) {
+
+    int max_index = -1;
+    int max = -1;
+    for(int __i=0; __i<ps.size(); __i++)
+    {
+        if(ps[__i] > max)
+        {
+            max = ps[__i];
+            max_index = __i;
+        }
+    }
+    return max_index;
+}
+
+
+//=================================================================================================
+// intiables, literals, lifted booleans, clauses:
+
+
+// NOTE! intiables are just integers. No abstraction here. They should be chosen from 0..N,
+// so that they can be used as array indices.
+
+#define var_Undef (-1)
+
+
+class par_Lit {
+    int     x;
+public:
+    par_Lit() : x(var_Undef)                                              { }   // (lit_Undef)
+    par_Lit(int var) {x = var;};
+    //par_Lit(int var, bool sign)   {x=sign?var:-var; }
+
+    // Don't use these for constructing/deconstructing literals. Use the normal constructors instead.
+    friend int  toInt       (par_Lit p);  // Guarantees small, positive integers suitable for array indexing.
+    friend par_Lit  par_toLit       (int i);  // Inverse of 'toInt()'
+    friend par_Lit  operator   ~(par_Lit p);
+    //friend bool sign        (Lit p);
+    friend int  var         (par_Lit p);
+    //friend Lit  unsign      (Lit p);
+    //friend Lit  id          (Lit p, bool sgn);
+
+    bool operator == (par_Lit p) const { return x == p.x; }
+    bool operator != (par_Lit p) const { return x != p.x; }
+    bool operator <  (par_Lit p) const { return x < p.x;  } // '<' guarantees that p, ~p are adjacent in the ordering.
+
+    void pup(PUP::er &p) {
+        p|x;
+    }
+};
+
+inline  int  toInt       (par_Lit p)           { return p.x; }
+inline  par_Lit  par_toLit       (int i)           { par_Lit p; p.x = i; return p; }
+inline  par_Lit  operator   ~(par_Lit p)           { par_Lit q; q.x = -p.x; return q; }
+//inline  bool sign        (Lit p)           { return p.x >1?true:false; }
+inline  int  var         (par_Lit p)           { return p.x >> 1; }
+//inline  Lit  unsign      (Lit p)           { Lit q; q.x = p.x & ~1; return q; }
+//inline  Lit  id          (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; }
+
+//const Lit lit_Undef(var_Undef, false);  // }- Useful special constants.
+//const Lit lit_Error(var_Undef, true );  // }
+
+
+//=================================================================================================
+// Lifted booleans:
+
+/*
+class lbool {
+    char     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 == (lbool b) const { return value == b.value; }
+    bool  operator != (lbool b) const { return value != b.value; }
+    lbool operator ^ (bool b) const { return b ? lbool(-value) : 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);
+*/
+//=================================================================================================
+// Clause -- a simple class for representing a clause:
+
+
+class par_Clause {
+    CkVec<par_Lit>  data;
+
+public:
+   
+     par_Clause(){data.removeAll();}
+   
+     par_Clause(const par_Clause& corg)
+     {
+         data.resize(corg.size());
+        for(int _i=0; _i<data.size(); _i++)
+        {
+            data[_i] = corg[_i];
+        }
+     }
+
+    // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
+    template<class V>
+    par_Clause(const V& ps, bool learnt) {
+        data.resize(ps.size());
+        for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
+    }
+    
+    template<class V>
+    void attachdata(const V& ps, bool learnt)
+    {
+        data.resize(ps.size());
+        for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
+    }
+
+    void remove(int v){
+        for(int i=0; i<data.size(); i++)
+        {
+            if(toInt(data[i]) == v)
+            {
+                data.remove(i);
+                return;
+            }
+        }
+    }
+    // -- use this function instead:
+    int          size        ()      const   { return data.size(); }
+    //void         shrink      (int i)         { }
+    //void         pop         ()              { shrink(1); }
+    //bool         learnt      ()      const   {  }
+    //uint32_t     mark        ()      const   { return 1; }
+    //void         mark        (uint32_t m)    {  }
+    //const Lit&   last        ()      const   { return data[size()-1]; }
+
+    // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for
+    //       subsumption operations to behave correctly.
+    par_Lit&         operator [] (int i)         { return data[i]; }
+    par_Lit          operator [] (int i) const   { return data[i]; }
+    //operator const Lit* (void) const         { return data; }
+
+    //float       activity    ()              { return 1; }
+    //uint32_t     abstraction () const { return 1; }
+
+    //Lit          subsumes    (const Clause& other) const;
+    //void         strengthen  (Lit p);
+
+
+    void        resize  (int __size)  {data.resize(__size); }
+    void pup(PUP::er &p) {
+        for(int i=0; i<size(); i++)
+            p|data[i];
+    }
+};
+
+
+/*_________________________________________________________________________________________________
+|
+|  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
+{
+        return lit_Error;
+}
+*/
+/*
+inline void Clause::strengthen(Lit p)
+{
+    //remove(*this, p);
+    //calcAbstraction();
+}
+*/
+#endif