Adding a new SAT solver to ABC. (Satoko)

The command is ‘satoko’

24 files changed, 3533 insertions, 2 deletions

diff --git a/Makefile b/Makefile
index d45978a9..4142e1b2 100644
--- a/Makefile
+++ b/Makefile
@@ -23,7 +23,7 @@ MODULES := \
 	src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \
 	src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
 	src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \
-	src/sat/bsat src/sat/xsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
+	src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
 	src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \
 	src/bool/rsb src/bool/rpo \
 	src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 008adbae..efb82fcc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -43,6 +43,7 @@
 #include "map/amap/amap.h"
 #include "opt/ret/retInt.h"
 #include "sat/xsat/xsat.h"
+#include "sat/satoko/satoko.h"
 #include "sat/cnf/cnf.h"
 #include "proof/cec/cec.h"
 #include "proof/acec/acec.h"
@@ -308,6 +309,7 @@ static int Abc_CommandDSec                   ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandSat                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDSat                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandXSat                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSatoko                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPSat                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandProve                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIProve                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -956,6 +958,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsat",          Abc_CommandDSat,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "xsat",          Abc_CommandXSat,             0 );
+    Cmd_CommandAdd( pAbc, "Verification", "satoko",        Abc_CommandSatoko,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "psat",          Abc_CommandPSat,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
     Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
@@ -23313,6 +23316,83 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    abctime clk;
+    int c;
+    satoko_opts_t opts;
+
+    satoko_default_opts(&opts);
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Chv" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            opts.conf_limit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( opts.conf_limit < 0 )
+                goto usage;
+            break;
+        case 'h':
+            goto usage;
+        case 'v':
+            opts.verbose ^= 1;
+            break;
+
+        default:
+            goto usage;
+        }
+    }
+
+    if ( argc == globalUtilOptind + 1 )
+    {
+        char * pFileName = argv[globalUtilOptind];
+        satoko_t * p;
+        int status;
+
+        satoko_parse_dimacs( pFileName, &p );
+    satoko_configure(p, &opts);
+
+        clk = Abc_Clock();
+        status = satoko_solve( p );
+
+        if ( status == SATOKO_UNDEC )
+            Abc_Print( 1, "UNDECIDED      " );
+        else if ( status == SATOKO_SAT )
+            Abc_Print( 1, "SATISFIABLE    " );
+        else
+            Abc_Print( 1, "UNSATISFIABLE  " );
+
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+        satoko_destroy( p );
+        return 0;
+    }
+
+usage:
+    Abc_Print( -2, "usage: satoko [-CILDE num] [-hv]<file>.cnf\n" );
+    Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
+    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
@@ -26238,7 +26318,7 @@ usage:
     Abc_Print( -2, "\t  Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, \"Better Generalization in IC3\", FMCAD 2013.\n");
     Abc_Print( -2, "\t  (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/85-Better-Generalization-IC3.pdf)\n");
 
-    
+
 
     return 1;
 }
diff --git a/src/sat/satoko/LICENSE b/src/sat/satoko/LICENSE
new file mode 100644
index 00000000..51938137
--- /dev/null
+++ b/src/sat/satoko/LICENSE
@@ -0,0 +1,22 @@
+Copyright 2017, Bruno Schmitt - UC Berkeley / UFRGS (bruno@oschmitt.com)
+
+Redistribution and use in source and binary forms, with or without modification,
+are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/src/sat/satoko/act_clause.h b/src/sat/satoko/act_clause.h
new file mode 100644
index 00000000..5a2fda2b
--- /dev/null
+++ b/src/sat/satoko/act_clause.h
@@ -0,0 +1,80 @@
+//===--- act_var.h ----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__act_clause_h
+#define satoko__act_clause_h
+
+#include "solver.h"
+#include "types.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#ifdef SATOKO_ACT_CLAUSE_FLOAT
+
+/** Re-scale the activity value for all clauses.
+ */
+static inline void clause_act_rescale(solver_t *s)
+{
+    unsigned i, cref;
+    struct clause *clause;
+
+    vec_uint_foreach(s->learnts, cref, i) {
+        clause = clause_read(s, cref);
+        clause->data[clause->size].act *= 1e-20;
+    }
+    s->clause_act_inc  *= 1e-20;
+}
+
+/** Increment the activity value of one clause ('clause')
+ */
+static inline void clause_act_bump(solver_t *s, struct clause *clause)
+{
+    clause->data[clause->size].act += s->clause_act_inc;
+    if (clause->data[clause->size].act > 1e20)
+        clause_act_rescale(s);
+}
+
+/** Increment the value by which clauses activity values are incremented
+ */
+static inline void clause_act_decay(solver_t *s)
+{
+    s->clause_act_inc *= (1 / s->opts.clause_decay);
+}
+
+#else /* SATOKO_ACT_CLAUSE_FLOAT */
+
+static inline void clause_act_rescale(solver_t *s)
+{
+    unsigned i, cref;
+    struct clause *clause;
+
+    vec_uint_foreach(s->learnts, cref, i) {
+        clause = clause_read(s, cref);
+        clause->data[clause->size].act >>= 14;
+    }
+    s->clause_act_inc >>= 14;
+    s->clause_act_inc = mkt_uint_max(s->clause_act_inc, (1 << 10));
+}
+
+static inline void clause_act_bump(solver_t *s, struct clause *clause)
+{
+    clause->data[clause->size].act += s->clause_act_inc;
+    if (clause->data[clause->size].act & 0x80000000)
+        clause_act_rescale(s);
+}
+
+static inline void clause_act_decay(solver_t *s)
+{
+    s->clause_act_inc += (s->clause_act_inc >> 10);
+}
+
+#endif /* SATOKO_ACT_CLAUSE_FLOAT */
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__act_clause_h */
diff --git a/src/sat/satoko/act_var.h b/src/sat/satoko/act_var.h
new file mode 100644
index 00000000..161e9d9a
--- /dev/null
+++ b/src/sat/satoko/act_var.h
@@ -0,0 +1,84 @@
+//===--- act_var.h ----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__act_var_h
+#define satoko__act_var_h
+
+#include "solver.h"
+#include "types.h"
+#include "utils/heap.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#ifdef SATOKO_ACT_VAR_DBLE
+/** Re-scale the activity value for all variables.
+ */
+static inline void var_act_rescale(solver_t *s)
+{
+    unsigned i;
+    double *activity = vec_dble_data(s->activity);
+
+    for (i = 0; i < vec_dble_size(s->activity); i++)
+        activity[i] *= 1e-100;
+    s->var_act_inc *= 1e-100;
+}
+
+/** Increment the activity value of one variable ('var')
+ */
+static inline void var_act_bump(solver_t *s, unsigned var)
+{
+    double *activity = vec_dble_data(s->activity);
+
+    activity[var] += s->var_act_inc;
+    if (activity[var] > 1e100)
+        var_act_rescale(s);
+    if (heap_in_heap(s->var_order, var))
+        heap_decrease(s->var_order, var);
+}
+
+/** Increment the value by which variables activity values are incremented
+ */
+static inline void var_act_decay(solver_t *s)
+{
+    s->var_act_inc *= (1 / s->opts.var_decay);
+}
+
+#else /* SATOKO_ACT_VAR_DBLE */
+
+static inline void var_act_rescale(solver_t *s)
+{
+    unsigned i;
+    unsigned *activity = vec_uint_data(s->activity);
+
+    for (i = 0; i < vec_uint_size(s->activity); i++)
+        activity[i] >>= 19;
+    s->var_act_inc >>= 19;
+    s->var_act_inc = mkt_uint_max(s->var_act_inc, (1 << 5));
+}
+
+static inline void var_act_bump(solver_t *s, unsigned var)
+{
+    unsigned *activity = vec_uint_data(s->activity);
+
+    activity[var] += s->var_act_inc;
+    if (activity[var] & 0x80000000)
+        var_act_rescale(s);
+    if (heap_in_heap(s->var_order, var))
+        heap_decrease(s->var_order, var);
+}
+
+static inline void var_act_decay(solver_t *s)
+{
+    s->var_act_inc += (s->var_act_inc >> 4);
+}
+
+#endif /* SATOKO_ACT_VAR_DBLE */
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__act_var_h */
diff --git a/src/sat/satoko/cdb.h b/src/sat/satoko/cdb.h
new file mode 100644
index 00000000..28686ff2
--- /dev/null
+++ b/src/sat/satoko/cdb.h
@@ -0,0 +1,100 @@
+//===--- cdb.h --------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__cdb_h
+#define satoko__cdb_h
+
+#include "clause.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+/* Clauses DB data structure */
+struct cdb {
+    unsigned size;
+    unsigned cap;
+    unsigned wasted;
+    unsigned *data;
+};
+
+//===------------------------------------------------------------------------===
+// Clause DB API
+//===------------------------------------------------------------------------===
+static inline struct clause *cdb_handler(struct cdb *p, unsigned cref)
+{
+    return cref != 0xFFFFFFFF ? (struct clause *)(p->data + cref) : NULL;
+}
+
+static inline unsigned cdb_cref(struct cdb *p, unsigned *clause)
+{
+    return (unsigned)(clause - &(p->data[0]));
+}
+
+static inline void cdb_grow(struct cdb *p, unsigned cap)
+{
+    unsigned prev_cap = p->cap;
+
+    if (p->cap >= cap)
+        return;
+    while (p->cap < cap) {
+        unsigned delta = ((p->cap >> 1) + (p->cap >> 3) + 2) & (unsigned)(~1);
+        p->cap += delta;
+        assert(p->cap >= prev_cap);
+    }
+    assert(p->cap > 0);
+    p->data = satoko_realloc(unsigned, p->data, p->cap);
+}
+
+static inline struct cdb *cdb_alloc(unsigned cap)
+{
+    struct cdb *p = satoko_calloc(struct cdb, 1);
+    if (cap <= 0)
+        cap = 1024 * 1024;
+    cdb_grow(p, cap);
+    return p;
+}
+
+static inline void cdb_free(struct cdb *p)
+{
+    satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned cdb_append(struct cdb *p, unsigned size)
+{
+    unsigned prev_size;
+    assert(size > 0);
+    cdb_grow(p, p->size + size);
+    prev_size = p->size;
+    p->size += size;
+    assert(p->size > prev_size);
+    return prev_size;
+}
+
+static inline void cdb_remove(struct cdb *p, struct clause *clause)
+{
+    p->wasted += clause->size;
+}
+
+static inline unsigned cdb_capacity(struct cdb *p)
+{
+    return p->cap;
+}
+
+static inline unsigned cdb_size(struct cdb *p)
+{
+    return p->size;
+}
+
+static inline unsigned cdb_wasted(struct cdb *p)
+{
+    return p->wasted;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__cdb_h */
diff --git a/src/sat/satoko/clause.h b/src/sat/satoko/clause.h
new file mode 100644
index 00000000..2be18cd6
--- /dev/null
+++ b/src/sat/satoko/clause.h
@@ -0,0 +1,63 @@
+//===--- clause.h -----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__clause_h
+#define satoko__clause_h
+
+#include "types.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+struct clause {
+    unsigned f_learnt    : 1;
+    unsigned f_mark      : 1;
+    unsigned f_reallocd  : 1;
+    unsigned f_deletable : 1;
+    unsigned lbd : 28;
+    unsigned size;
+    union {
+        unsigned lit;
+        clause_act_t act;
+    } data[0];
+};
+
+//===------------------------------------------------------------------------===
+// Clause API
+//===------------------------------------------------------------------------===
+static inline int clause_compare(const void *p1, const void *p2)
+{
+    const struct clause *c1 = (const struct clause *)p1;
+    const struct clause *c2 = (const struct clause *)p2;
+
+    if (c1->size > 2 && c2->size == 2)
+        return 1;
+    if (c1->size == 2 && c2->size > 2)
+        return 0;
+    if (c1->size == 2 && c2->size == 2)
+        return 0;
+
+    if (c1->lbd > c2->lbd)
+        return 1;
+    if (c1->lbd < c2->lbd)
+        return 0;
+
+    return c1->data[c1->size].act < c2->data[c2->size].act;
+}
+
+static inline void clause_print(struct clause *clause)
+{
+    unsigned i;
+    printf("{ ");
+    for (i = 0; i < clause->size; i++)
+        printf("%u ", clause->data[i].lit);
+    printf("}\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__clause_h */
diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c
new file mode 100644
index 00000000..5e4b92f9
--- /dev/null
+++ b/src/sat/satoko/cnf_reader.c
@@ -0,0 +1,156 @@
+//===--- cnf_reader.h -------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#include <assert.h>
+#include <ctype.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "satoko.h"
+#include "solver.h"
+#include "utils/mem.h"
+#include "utils/vec/vec_uint.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_IMPL_START
+
+/** Read the file into an internal buffer.
+ *
+ * This function will receive a file name. The return data is a string ended
+ * with '\0'.
+ *
+ */
+static char * file_open(const char *fname)
+{
+    FILE *file = fopen(fname, "rb");
+    char *buffer;
+    int sz_file;
+    int ret;
+
+    if (file == NULL) {
+        printf("Couldn't open file: %s\n", fname);
+        return NULL;
+    }
+    fseek(file, 0, SEEK_END);
+    sz_file = ftell(file);
+    rewind(file);
+    buffer = satoko_alloc(char, sz_file + 3);
+    ret = fread(buffer, sz_file, 1, file);
+    buffer[sz_file + 0] = '\n';
+    buffer[sz_file + 1] = '\0';
+    return buffer;
+}
+
+static void skip_spaces(char **pos)
+{
+    assert(pos != NULL);
+    for (; isspace(**pos); (*pos)++);
+}
+
+static void skip_line(char **pos)
+{
+    assert(pos != NULL);
+    for(; **pos != '\n' && **pos != '\r' && **pos != EOF; (*pos)++);
+    if (**pos != EOF)
+        (*pos)++;
+    return;
+}
+
+static int read_int(char **token)
+{
+    int value = 0;
+    int neg = 0;
+
+    skip_spaces(token);
+    if (**token == '-') {
+        neg = 1;
+        (*token)++;
+    } else if (**token == '+')
+        (*token)++;
+
+    if (!isdigit(**token)) {
+        printf("Parsing error. Unexpected char: %c.\n", **token);
+        exit(EXIT_FAILURE);
+    }
+    while (isdigit(**token)) {
+        value = (value * 10) + (**token - '0');
+        (*token)++;
+    }
+    return neg ? -value : value;
+}
+
+static void read_clause(char **token, vec_uint_t *lits)
+{
+    int var;
+    unsigned sign;
+
+    vec_uint_clear(lits);
+    while (1) {
+        var = read_int(token);
+        if (var == 0)
+            break;
+        sign = (var > 0);
+        var = abs(var) - 1;
+        vec_uint_push_back(lits, var2lit((unsigned) var, !sign));
+    }
+}
+
+/** Start the solver and reads the DIMAC file.
+ *
+ * Returns false upon immediate conflict.
+ */
+int satoko_parse_dimacs(char *fname, satoko_t **solver)
+{
+    satoko_t *p = NULL;
+    vec_uint_t *lits = NULL;
+    int n_var;
+    int n_clause;
+    char *buffer = file_open(fname);
+    char *token;
+
+    if (buffer == NULL)
+        return -1;
+
+    token = buffer;
+    while (1) {
+        skip_spaces(&token);
+        if (*token == 0)
+            break;
+        else if (*token == 'c')
+            skip_line(&token);
+        else if (*token == 'p') {
+            token++;
+            skip_spaces(&token);
+            for(; !isspace(*token); token++); /* skip 'cnf' */
+
+            n_var = read_int(&token);
+            n_clause = read_int(&token);
+            skip_line(&token);
+            lits = vec_uint_alloc((unsigned) n_var);
+            p = satoko_create();
+        } else {
+            if (lits == NULL) {
+                printf("There is no parameter line.\n");
+                satoko_free(buffer);
+                return -1;
+            }
+            read_clause(&token, lits);
+            if (!satoko_add_clause(p, vec_uint_data(lits), vec_uint_size(lits))) {
+                vec_uint_print(lits);
+                return 0;
+            }
+            }
+    }
+    vec_uint_free(lits);
+    satoko_free(buffer);
+    *solver = p;
+    return satoko_simplify(p);
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/module.make b/src/sat/satoko/module.make
new file mode 100644
index 00000000..512094ee
--- /dev/null
+++ b/src/sat/satoko/module.make
@@ -0,0 +1,3 @@
+SRC +=  src/sat/satoko/solver.c \
+    src/sat/satoko/solver_api.c \
+    src/sat/satoko/cnf_reader.c
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
new file mode 100644
index 00000000..49c7837e
--- /dev/null
+++ b/src/sat/satoko/satoko.h
@@ -0,0 +1,85 @@
+//===--- satoko.h -----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__satoko_h
+#define satoko__satoko_h
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+/** Return valeus */
+enum {
+    SATOKO_ERR = 0,
+    SATOKO_OK  = 1
+};
+
+enum {
+    SATOKO_UNDEC = 0, /* Undecided */
+    SATOKO_SAT   = 1,
+    SATOKO_UNSAT = -1
+};
+
+struct solver_t_;
+typedef struct solver_t_ satoko_t;
+
+typedef struct satoko_opts satoko_opts_t;
+struct satoko_opts {
+    /* Limits */
+    long long conf_limit;  /* Limit on the n.of conflicts */
+    long long prop_limit;  /* Limit on the n.of implications */
+
+    /* Constants used for restart heuristic */
+    double f_rst;          /* Used to force a restart */
+    double b_rst;          /* Used to block a restart */
+    unsigned fst_block_rst;   /* Lower bound n.of conflicts for start blocking restarts */
+    unsigned sz_lbd_bqueue;   /* Size of the moving avarege queue for LBD (force restart) */
+    unsigned sz_trail_bqueue; /* Size of the moving avarege queue for Trail size (block restart) */
+
+    /* Constants used for clause database reduction heuristic */
+    unsigned n_conf_fst_reduce;  /* N.of conflicts before first reduction */
+    unsigned inc_reduce;         /* Increment to reduce */
+    unsigned inc_special_reduce; /* Special increment to reduce */
+    unsigned lbd_freeze_clause;
+
+    /* VSIDS heuristic */
+    float clause_decay;
+    double var_decay;
+
+    /* Binary resolution */
+    unsigned clause_max_sz_bin_resol;
+    unsigned clause_min_lbd_bin_resol;
+    float garbage_max_ratio;
+    char verbose;
+};
+
+//===------------------------------------------------------------------------===
+extern satoko_t *satoko_create(void);
+extern void satoko_destroy(satoko_t *);
+extern void satoko_default_opts(satoko_opts_t *);
+extern void satoko_configure(satoko_t *, satoko_opts_t *);
+extern int  satoko_parse_dimacs(char *, satoko_t **);
+extern void satoko_add_variable(satoko_t *, char);
+extern int  satoko_add_clause(satoko_t *, unsigned *, unsigned);
+extern void satoko_assump_push(satoko_t *s, unsigned);
+extern void satoko_assump_pop(satoko_t *s);
+extern int  satoko_simplify(satoko_t *);
+extern int  satoko_solve(satoko_t *);
+
+/* If problem is unsatisfiable under assumptions, this function is used to
+ * obtain the final conflict clause expressed in the assumptions.
+ *
+ *  - It receives as inputs the solver and a pointer to a array where clause
+ * will be copied. The memory is allocated by the solver, but must be freed by
+ * the caller.
+ *  - The return value is either the size of the array or -1 in case the final
+ * conflict cluase was not generated.
+ */
+extern int  satoko_final_conflict(satoko_t *, unsigned *);
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__satoko_h */
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
new file mode 100644
index 00000000..b2861bad
--- /dev/null
+++ b/src/sat/satoko/solver.c
@@ -0,0 +1,704 @@
+//===--- solver.c -----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "act_clause.h"
+#include "act_var.h"
+#include "solver.h"
+#include "utils/heap.h"
+#include "utils/mem.h"
+#include "utils/sort.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_IMPL_START
+
+//===------------------------------------------------------------------------===
+// Lit funtions
+//===------------------------------------------------------------------------===
+/**
+ *  A literal is said to be redundant in a given clause if and only if all
+ *  variables in its reason are either present in that clause or (recursevely)
+ *  redundant.
+ */
+static inline int lit_is_removable(solver_t* s, unsigned lit, unsigned min_level)
+{
+    unsigned top = vec_uint_size(s->tagged);
+
+    assert(lit_reason(s, lit) != UNDEF);
+    vec_uint_clear(s->stack);
+    vec_uint_push_back(s->stack, lit2var(lit));
+    while (vec_uint_size(s->stack)) {
+        unsigned i;
+        unsigned var = vec_uint_pop_back(s->stack);
+        struct clause *c = clause_read(s, var_reason(s, var));
+        unsigned *lits = &(c->data[0].lit);
+
+        assert(var_reason(s, var) != UNDEF);
+        if (c->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) {
+            assert(lit_value(s, lits[1]) == LIT_TRUE);
+            mkt_swap(unsigned, lits[0], lits[1]);
+        }
+
+        /* Check scan the literals of the reason clause.
+         * The first literal is skiped because is the literal itself. */
+        for (i = 1; i < c->size; i++) {
+            var = lit2var(lits[i]);
+
+            /* Check if the variable has already been seen or if it
+             * was assinged a value at the decision level 0. In a
+             * positive case, there is no need to look any further */
+            if (vec_char_at(s->seen, var) || var_dlevel(s, var) == 0)
+                continue;
+
+            /* If the variable has a reason clause and if it was
+             * assingned at a 'possible' level, then we need to
+             * check if it is recursively redundant, otherwise the
+             * literal being checked is not redundant */
+            if (var_reason(s, var) != UNDEF && ((1 << (var_dlevel(s, var) & 31)) & min_level)) {
+                vec_uint_push_back(s->stack, var);
+                vec_uint_push_back(s->tagged, var);
+                vec_char_assign(s->seen, var, 1);
+            } else {
+                vec_uint_foreach_start(s->tagged, var, i, top)
+                    vec_char_assign(s->seen, var, 0);
+                vec_uint_shrink(s->tagged, top);
+                return 0;
+            }
+        }
+    }
+    return 1;
+}
+
+//===------------------------------------------------------------------------===
+// Clause functions
+//===------------------------------------------------------------------------===
+/* Calculate clause LBD (Literal Block Distance):
+ * - It's the number of variables in the final conflict clause that come from
+ * different decision levels
+ */
+static inline unsigned clause_clac_lbd(solver_t *s, unsigned *lits, unsigned size)
+{
+    unsigned i;
+    unsigned lbd = 0;
+
+    s->cur_stamp++;
+    for (i = 0; i < size; i++) {
+        unsigned level = lit_dlevel(s, lits[i]);
+        if (vec_uint_at(s->stamps, level) != s->cur_stamp) {
+            vec_uint_assign(s->stamps, level, s->cur_stamp);
+            lbd++;
+        }
+    }
+    return lbd;
+}
+
+static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits)
+{
+    unsigned *lits = vec_uint_data(clause_lits);
+    unsigned counter, sz, i;
+    unsigned lit;
+    unsigned neg_lit = lit_neg(lits[0]);
+    struct watcher *w;
+
+    s->cur_stamp++;
+    vec_uint_foreach(clause_lits, lit, i)
+        vec_uint_assign(s->stamps, lit2var(lit), s->cur_stamp);
+
+    counter = 0;
+    watch_list_foreach(s->bin_watches, w, neg_lit) {
+        unsigned imp_lit = w->blocker;
+        if (vec_uint_at(s->stamps, lit2var(imp_lit)) == s->cur_stamp &&
+            lit_value(s, imp_lit) == LIT_TRUE) {
+            counter++;
+            vec_uint_assign(s->stamps, lit2var(imp_lit), (s->cur_stamp - 1));
+        }
+    }
+    if (counter > 0) {
+        sz = vec_uint_size(clause_lits) - 1;
+        for (i = 1; i < vec_uint_size(clause_lits) - counter; i++)
+            if (vec_uint_at(s->stamps, lit2var(lits[i])) != s->cur_stamp) {
+                mkt_swap(unsigned, lits[i], lits[sz]);
+                i--;
+                sz--;
+            }
+        vec_uint_shrink(clause_lits, vec_uint_size(clause_lits) - counter);
+    }
+}
+
+static inline void clause_minimize(solver_t *s, vec_uint_t *clause_lits)
+{
+    unsigned i, j;
+    unsigned *lits = vec_uint_data(clause_lits);
+    unsigned min_level = 0;
+    unsigned clause_size;
+
+    for (i = 1; i < vec_uint_size(clause_lits); i++) {
+        unsigned level = lit_dlevel(s, lits[i]);
+        min_level |= 1 << (level & 31);
+    }
+
+    /* Remove reduntant literals */
+    vec_uint_foreach(clause_lits, i, j)
+        vec_uint_push_back(s->tagged, lit2var(i));
+    for (i = j = 1; i < vec_uint_size(clause_lits); i++)
+        if (lit_reason(s, lits[i]) == UNDEF || !lit_is_removable(s, lits[i], min_level))
+            lits[j++] = lits[i];
+    vec_uint_shrink(clause_lits, j);
+
+    /* Binary Resolution */
+    clause_size = vec_uint_size(clause_lits);
+    if (clause_size <= s->opts.clause_max_sz_bin_resol &&
+        clause_clac_lbd(s, lits, clause_size) <= s->opts.clause_min_lbd_bin_resol)
+        clause_bin_resolution(s, clause_lits);
+}
+
+static inline void clause_realloc(struct cdb *dest, struct cdb *src, unsigned *cref)
+{
+    unsigned new_cref;
+    struct clause *new_clause;
+    struct clause *old_clause = cdb_handler(src, *cref);
+
+    if (old_clause->f_reallocd) {
+        *cref = (unsigned) old_clause->size;
+        return;
+    }
+    new_cref = cdb_append(dest, 3 + old_clause->f_learnt + old_clause->size);
+    new_clause = cdb_handler(dest, new_cref);
+    memcpy(new_clause, old_clause, (3 + old_clause->f_learnt + old_clause->size) * 4);
+    old_clause->f_reallocd = 1;
+    old_clause->size = (unsigned) new_cref;
+    *cref = new_cref;
+}
+
+//===------------------------------------------------------------------------===
+// Solver internal functions
+//===------------------------------------------------------------------------===
+static inline unsigned solver_decide(solver_t *s)
+{
+    unsigned next_var = UNDEF;
+
+    while (next_var == UNDEF || var_value(s, next_var) != VAR_UNASSING) {
+        if (heap_size(s->var_order) == 0) {
+            next_var = UNDEF;
+            return UNDEF;
+        } else
+            next_var = heap_remove_min(s->var_order);
+    }
+    return var2lit(next_var, vec_char_at(s->polarity, next_var));
+}
+
+static inline void solver_new_decision(solver_t *s, unsigned lit)
+{
+    assert(var_value(s, lit2var(lit)) == VAR_UNASSING);
+    vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
+    solver_enqueue(s, lit, UNDEF);
+}
+
+/* Calculate Backtrack Level from the learnt clause */
+static inline unsigned solver_calc_bt_level(solver_t *s, vec_uint_t *learnt)
+{
+    unsigned i, tmp;
+        unsigned i_max = 1;
+    unsigned *lits = vec_uint_data(learnt);
+        unsigned max = lit_dlevel(s, lits[1]);
+
+    if (vec_uint_size(learnt) == 1)
+        return 0;
+    for (i = 2; i < vec_uint_size(learnt); i++) {
+        if (lit_dlevel(s, lits[i]) > max) {
+            max   = lit_dlevel(s, lits[i]);
+            i_max = i;
+        }
+    }
+        tmp         = lits[1];
+        lits[1]     = lits[i_max];
+        lits[i_max] = tmp;
+        return lit_dlevel(s, lits[1]);
+}
+
+/**
+ *  Most books and papers explain conflict analysis and the calculation of the
+ *  1UIP (first Unique Implication Point) using an implication graph. This
+ *  function, however, do not explicity constructs the graph! It inspects the
+ *  trail in reverse and figure out which literals should be added to the
+ *  to-be-learnt clause using the reasons of each assignment.
+ *
+ *  cur_lit: current literal being analyzed.
+ *  n_paths: number of unprocessed paths from conlfict node to the current
+ *           literal being analyzed (cur_lit).
+ *
+ *  This functions performs a backward BFS (breadth-first search) for 1UIP node.
+ *  The trail works as the BFS queue. The counter of unprocessed but seen
+ *  variables (n_paths) allows us to identify when 'cur_lit' is the closest
+ *  cause of conflict.
+ *
+ *  When 'n_paths' reaches zero it means there are no unprocessed reverse paths
+ *  back from the conflict node to 'cur_lit' - meaning it is the 1UIP decision
+ *  variable.
+ *
+ */
+static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt,
+                      unsigned *bt_level, unsigned *lbd)
+{
+    unsigned i;
+    unsigned *trail = vec_uint_data(s->trail);
+    unsigned idx = vec_uint_size(s->trail) - 1;
+    unsigned n_paths = 0;
+    unsigned p = UNDEF;
+    unsigned var;
+
+    vec_uint_push_back(learnt, UNDEF);
+    do {
+        struct clause *clause;
+        unsigned *lits;
+        unsigned j;
+
+        assert(cref != UNDEF);
+        clause = clause_read(s, cref);
+        lits = &(clause->data[0].lit);
+
+        if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) {
+            assert(lit_value(s, lits[1]) == LIT_TRUE);
+            mkt_swap(unsigned, lits[0], lits[1] );
+        }
+
+        if (clause->f_learnt)
+            clause_act_bump(s, clause);
+
+        if (clause->f_learnt && clause->lbd > 2) {
+            unsigned n_levels = clause_clac_lbd(s, lits, clause->size);
+            if (n_levels + 1 < clause->lbd) {
+                if (clause->lbd <= s->opts.lbd_freeze_clause)
+                    clause->f_deletable = 0;
+                clause->lbd = n_levels;
+            }
+        }
+
+        for (j = (p == UNDEF ? 0 : 1); j < clause->size; j++) {
+            var = lit2var(lits[j]);
+            if (vec_char_at(s->seen, var) || var_dlevel(s, var) == 0)
+                continue;
+            vec_char_assign(s->seen, var, 1);
+            var_act_bump(s, var);
+            if (var_dlevel(s, var) == solver_dlevel(s)) {
+                n_paths++;
+                if (var_reason(s, var) != UNDEF && clause_read(s, var_reason(s, var))->f_learnt)
+                    vec_uint_push_back(s->last_dlevel, var);
+            } else
+                vec_uint_push_back(learnt, lits[j]);
+        }
+
+        while (!vec_char_at(s->seen, lit2var(trail[idx--])));
+
+        p = trail[idx + 1];
+        cref = lit_reason(s, p);
+        vec_char_assign(s->seen, lit2var(p), 0);
+        n_paths--;
+    } while (n_paths > 0);
+
+    vec_uint_data(learnt)[0] = lit_neg(p);
+    clause_minimize(s, learnt);
+    *bt_level = solver_calc_bt_level(s, learnt);
+    *lbd = clause_clac_lbd(s, vec_uint_data(learnt), vec_uint_size(learnt));
+
+    if (vec_uint_size( s->last_dlevel) > 0) {
+        vec_uint_foreach(s->last_dlevel, var, i) {
+            if (clause_read(s, var_reason(s, var))->lbd < *lbd)
+                var_act_bump(s, var);
+        }
+        vec_uint_clear(s->last_dlevel);
+    }
+    vec_uint_foreach(s->tagged, var, i)
+        vec_char_assign(s->seen, var, 0);
+    vec_uint_clear(s->tagged);
+}
+
+static inline int solver_rst(solver_t *s)
+{
+    return b_queue_is_valid(s->bq_lbd) &&
+           (((long long)b_queue_avg(s->bq_lbd) * s->opts.f_rst) > (s->sum_lbd / s->stats.n_conflicts));
+}
+
+static inline int solver_block_rst(solver_t *s)
+{
+    return s->stats.n_conflicts > s->opts.fst_block_rst &&
+           b_queue_is_valid(s->bq_lbd) &&
+           (vec_uint_size(s->trail) > (s->opts.b_rst * (long long)b_queue_avg(s->bq_trail)));
+}
+
+static inline void solver_handle_conflict(solver_t *s, unsigned confl_cref)
+{
+    unsigned bt_level;
+    unsigned lbd;
+    unsigned cref;
+
+    vec_uint_clear(s->temp_lits);
+    solver_analyze(s, confl_cref, s->temp_lits, &bt_level, &lbd);
+    s->sum_lbd += lbd;
+    b_queue_push(s->bq_lbd, lbd);
+    solver_cancel_until(s, bt_level);
+    cref = UNDEF;
+    if (vec_uint_size(s->temp_lits) > 1) {
+        cref = solver_clause_create(s, s->temp_lits, 1);
+        clause_watch(s, cref);
+    }
+    solver_enqueue(s, vec_uint_at(s->temp_lits, 0), cref);
+    var_act_decay(s);
+    clause_act_decay(s);
+}
+
+static inline void solver_analyze_final(solver_t *s, unsigned lit)
+{
+    unsigned i;
+
+    vec_uint_push_back(s->final_conflict, lit);
+    if (solver_dlevel(s) == 0)
+        return;
+    vec_char_assign(s->seen, lit2var(lit), 1);
+    for (i = vec_uint_size(s->trail) - 1; i <= vec_uint_at(s->trail_lim, 0); i--) {
+        unsigned var = lit2var(vec_uint_at(s->trail, i));
+
+        if (vec_char_at(s->seen, var)) {
+            unsigned reason = var_reason(s, var);
+            if (reason == UNDEF) {
+                assert(var_dlevel(s, var) > 0);
+                vec_uint_push_back(s->final_conflict, lit_neg(vec_uint_at(s->trail, i)));
+            } else {
+                unsigned j;
+                struct clause *clause = clause_read(s, reason);
+                for (j = (clause->size == 2 ? 0 : 1); j < clause->size; j++) {
+                    if (lit_dlevel(s, clause->data[j].lit) > 0)
+                        vec_char_assign(s->seen, lit2var(clause->data[j].lit), 1);
+                }
+            }
+        vec_char_assign(s->seen, var, 0);
+        }
+    }
+    vec_char_assign(s->seen, lit2var(lit), 0);
+}
+
+static inline void solver_garbage_collect(solver_t *s)
+{
+    unsigned i;
+    unsigned *array;
+    struct cdb *new_cdb = cdb_alloc(cdb_capacity(s->all_clauses) - cdb_wasted(s->all_clauses));
+
+    for (i = 0; i < 2 * vec_char_size(s->assigns); i++) {
+        struct watcher *w;
+        watch_list_foreach(s->watches, w, i)
+            clause_realloc(new_cdb, s->all_clauses, &(w->cref));
+        watch_list_foreach(s->bin_watches, w, i)
+            clause_realloc(new_cdb, s->all_clauses, &(w->cref));
+    }
+
+    for (i = 0; i < vec_uint_size(s->trail); i++)
+        if (lit_reason(s, vec_uint_at(s->trail, i)) != UNDEF)
+            clause_realloc(new_cdb, s->all_clauses, &(vec_uint_data(s->reasons)[lit2var(vec_uint_at(s->trail, i))]));
+
+    array = vec_uint_data(s->learnts);
+    for (i = 0; i < vec_uint_size(s->learnts); i++)
+        clause_realloc(new_cdb, s->all_clauses, &(array[i]));
+
+    array = vec_uint_data(s->originals);
+    for (i = 0; i < vec_uint_size(s->originals); i++)
+        clause_realloc(new_cdb, s->all_clauses, &(array[i]));
+
+    cdb_free(s->all_clauses);
+    s->all_clauses = new_cdb;
+}
+
+static inline void solver_reduce_cdb(solver_t *s)
+{
+    unsigned i, limit;
+    unsigned n_learnts = vec_uint_size(s->learnts);
+    unsigned cref;
+    struct clause *clause;
+    struct clause **learnts_cls;
+
+    learnts_cls = satoko_alloc(struct clause *, n_learnts);
+    vec_uint_foreach(s->learnts, cref, i)
+        learnts_cls[i] = clause_read(s, cref);
+
+    limit = n_learnts / 2;
+
+    satoko_sort((void *)learnts_cls, n_learnts,
+            (int (*)(const void *, const void *)) clause_compare);
+
+    if (learnts_cls[n_learnts / 2]->lbd <= 3)
+        s->RC2 += s->opts.inc_special_reduce;
+    if (learnts_cls[n_learnts - 1]->lbd <= 6)
+        s->RC2 += s->opts.inc_special_reduce;
+
+    vec_uint_clear(s->learnts);
+    for (i = 0; i < n_learnts; i++) {
+        clause = learnts_cls[i];
+        cref = cdb_cref(s->all_clauses, (unsigned *)clause);
+        assert(clause->f_mark == 0);
+        if (clause->f_deletable && clause->lbd > 2 && clause->size > 2 && lit_reason(s, clause->data[0].lit) != cref && (i < limit)) {
+            clause->f_mark = 1;
+            s->stats.n_learnt_lits -= clause->size;
+            clause_unwatch(s, cref);
+            cdb_remove(s->all_clauses, clause);
+        } else {
+            if (!clause->f_deletable)
+                limit++;
+            clause->f_deletable = 1;
+            vec_uint_push_back(s->learnts, cref);
+        }
+    }
+    satoko_free(learnts_cls);
+
+    if (s->opts.verbose) {
+        printf("reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) \n",
+               vec_uint_size(s->learnts), n_learnts,
+               100.0 * vec_uint_size(s->learnts) / n_learnts);
+        fflush(stdout);
+    }
+    if (cdb_wasted(s->all_clauses) > cdb_size(s->all_clauses) * s->opts.garbage_max_ratio)
+        solver_garbage_collect(s);
+}
+
+//===------------------------------------------------------------------------===
+// Solver external functions
+//===------------------------------------------------------------------------===
+unsigned solver_clause_create(solver_t *s, vec_uint_t *lits, unsigned f_learnt)
+{
+    struct clause *clause;
+    unsigned cref;
+    unsigned n_words;
+
+    assert(vec_uint_size(lits) > 1);
+    assert(f_learnt == 0 || f_learnt == 1);
+
+    n_words = 3 + f_learnt + vec_uint_size(lits);
+    cref = cdb_append(s->all_clauses, n_words);
+    clause = clause_read(s, cref);
+    clause->f_learnt = f_learnt;
+    clause->f_mark = 0;
+    clause->f_reallocd = 0;
+    clause->f_deletable = f_learnt;
+    clause->size = vec_uint_size(lits);
+    memcpy(&(clause->data[0].lit), vec_uint_data(lits), sizeof(unsigned) * vec_uint_size(lits));
+
+    if (f_learnt) {
+        vec_uint_push_back(s->learnts, cref);
+        clause->lbd = clause_clac_lbd(s, vec_uint_data(lits), vec_uint_size(lits));
+        clause->data[clause->size].act = 0;
+        s->stats.n_learnt_lits += vec_uint_size(lits);
+        clause_act_bump(s, clause);
+    } else {
+        vec_uint_push_back(s->originals, cref);
+        s->stats.n_original_lits += vec_uint_size(lits);
+    }
+    return cref;
+}
+
+void solver_cancel_until(solver_t * s, unsigned level)
+{
+    int i;
+
+    if (solver_dlevel(s) <= level)
+        return;
+    for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, level); i--) {
+        unsigned var = lit2var(vec_uint_at(s->trail, (unsigned) i));
+
+        vec_char_assign(s->assigns, var, VAR_UNASSING);
+        vec_uint_assign(s->reasons, var, UNDEF);
+        vec_char_assign(s->polarity, var, lit_polarity(vec_uint_at(s->trail, (unsigned) i)));
+        if (!heap_in_heap(s->var_order, var))
+            heap_insert(s->var_order, var);
+    }
+    s->i_qhead = vec_uint_at(s->trail_lim, level);
+    vec_uint_shrink(s->trail, vec_uint_at(s->trail_lim, level));
+    vec_uint_shrink(s->trail_lim, level);
+}
+
+unsigned solver_propagate(solver_t *s)
+{
+    unsigned conf_cref = UNDEF;
+    unsigned *lits;
+    unsigned neg_lit;
+    unsigned n_propagations = 0;
+
+    while (s->i_qhead < vec_uint_size(s->trail)) {
+        unsigned p = vec_uint_at(s->trail, s->i_qhead++);
+        struct watch_list *ws;
+        struct watcher *begin;
+        struct watcher *end;
+        struct watcher *i, *j;
+
+        n_propagations++;
+        watch_list_foreach(s->bin_watches, i, p) {
+            if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING)
+                solver_enqueue(s, i->blocker, i->cref);
+            else if (lit_value(s, i->blocker) == LIT_FALSE)
+                return i->cref;
+        }
+
+        ws = vec_wl_at(s->watches, p);
+        begin = watch_list_array(ws);
+        end = begin + watch_list_size(ws);
+        for (i = j = begin; i < end;) {
+            struct clause *clause;
+            struct watcher w;
+
+            if (lit_value(s, i->blocker) == LIT_TRUE) {
+                *j++ = *i++;
+                continue;
+            }
+
+            clause = clause_read(s, i->cref);
+            lits = &(clause->data[0].lit);
+
+            // Make sure the false literal is data[1]:
+            neg_lit = lit_neg(p);
+            if (lits[0] == neg_lit)
+                mkt_swap(unsigned, lits[0], lits[1]);
+            assert(lits[1] == neg_lit);
+
+            w.cref = i->cref;
+            w.blocker = lits[0];
+
+            /* If 0th watch is true, then clause is already satisfied. */
+            if (lits[0] != i->blocker && lit_value(s, lits[0]) == LIT_TRUE)
+                *j++ = w;
+            else {
+                /* Look for new watch */
+                unsigned k;
+                for (k = 2; k < clause->size; k++) {
+                    if (lit_value(s, lits[k]) != LIT_FALSE) {
+                        lits[1] = lits[k];
+                        lits[k] = neg_lit;
+                        watch_list_push(vec_wl_at(s->watches, lit_neg(lits[1])), w);
+                        goto next;
+                    }
+                }
+
+                *j++ = w;
+
+                /* Clause becomes unit under this assignment */
+                if (lit_value(s, lits[0]) == LIT_FALSE) {
+                    conf_cref = i->cref;
+                    s->i_qhead = vec_uint_size(s->trail);
+                    i++;
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                } else
+                    solver_enqueue(s, lits[0], i->cref);
+            }
+        next:
+            i++;
+        }
+
+        s->stats.n_inspects += j - watch_list_array(ws);
+        watch_list_shrink(ws, j - watch_list_array(ws));
+    }
+    s->stats.n_propagations += n_propagations;
+    s->n_props_simplify -= n_propagations;
+    return conf_cref;
+}
+
+char solver_search(solver_t *s)
+{
+    s->stats.n_starts++;
+    while (1) {
+        unsigned confl_cref = solver_propagate(s);
+        if (confl_cref != UNDEF) {
+            s->stats.n_conflicts++;
+            if (solver_dlevel(s) == 0)
+                return SATOKO_UNSAT;
+            /* Restart heuristic */
+            b_queue_push(s->bq_trail, vec_uint_size(s->trail));
+            if (solver_block_rst(s))
+                b_queue_clean(s->bq_lbd);
+            solver_handle_conflict(s, confl_cref);
+        } else {
+            /* No conflict */
+            unsigned next_lit;
+
+            if (solver_rst(s)) {
+                b_queue_clean(s->bq_lbd);
+                solver_cancel_until(s, 0);
+                return SATOKO_UNDEC;
+            }
+            if (solver_dlevel(s) == 0)
+                satoko_simplify(s);
+
+            /* Reduce the set of learnt clauses */
+            if (s->stats.n_conflicts >= s->n_confl_bfr_reduce) {
+                s->RC1 = (s->stats.n_conflicts / s->RC2) + 1;
+                solver_reduce_cdb(s);
+                s->RC2 += s->opts.inc_reduce;
+                s->n_confl_bfr_reduce = s->RC1 * s->RC2;
+            }
+
+            /* Make decisions based on user assumptions */
+            next_lit = UNDEF;
+            while (solver_dlevel(s) < vec_uint_size(s->assumptions)) {
+                unsigned lit = vec_uint_at(s->assumptions, solver_dlevel(s));
+                if (lit_value(s, lit) == LIT_TRUE) {
+                    vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail));
+                } else if (lit_value(s, lit) == LIT_FALSE) {
+                    solver_analyze_final(s, lit_neg(lit));
+                    return SATOKO_UNSAT;
+                } else {
+                    next_lit = lit;
+                    break;
+                }
+
+            }
+            if (next_lit == UNDEF) {
+                s->stats.n_decisions++;
+                next_lit = solver_decide(s);
+                if (next_lit == UNDEF)
+                    return SATOKO_SAT;
+            }
+            solver_new_decision(s, next_lit);
+        }
+    }
+}
+
+//===------------------------------------------------------------------------===
+// Debug procedure
+//===------------------------------------------------------------------------===
+void solver_debug_check(solver_t *s, int result)
+{
+    unsigned cref, i;
+    unsigned *array;
+
+    printf("Checking for trail(%u) inconsistencies...", vec_uint_size(s->trail));
+    array = vec_uint_data(s->trail);
+    for (i = 1; i < vec_uint_size(s->trail); i++)
+        if (array[i - 1] == lit_neg(array[i])) {
+            printf("Inconsistent trail: %u %u\n", array[i - 1], array[i]);
+            return;
+        }
+    printf(" TRAIL OK\n");
+
+    printf("Checking clauses... \n");
+    vec_uint_foreach(s->originals, cref, i) {
+        unsigned j;
+        struct clause *clause = clause_read(s, cref);
+        for (j = 0; j < clause->size; j++) {
+            if (vec_uint_find(s->trail, clause->data[j].lit)) {
+                break;
+            }
+        }
+        if (result == SATOKO_SAT && j == clause->size) {
+            printf("FOUND UNSAT CLAUSE!!!!\n");
+            clause_print(clause);
+        }
+    }
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h
new file mode 100644
index 00000000..65b86c68
--- /dev/null
+++ b/src/sat/satoko/solver.h
@@ -0,0 +1,242 @@
+//===--- solver.h -----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__solver_h
+#define satoko__solver_h
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "clause.h"
+#include "cdb.h"
+#include "satoko.h"
+#include "types.h"
+#include "watch_list.h"
+#include "utils/b_queue.h"
+#include "utils/heap.h"
+#include "utils/mem.h"
+#include "utils/misc.h"
+#include "utils/vec/vec_char.h"
+#include "utils/vec/vec_dble.h"
+#include "utils/vec/vec_uint.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+enum {
+    LIT_FALSE = 1,
+    LIT_TRUE = 0,
+    VAR_UNASSING = 3
+};
+
+#define UNDEF 0xFFFFFFFF
+
+struct satoko_stats {
+    unsigned n_starts;
+    unsigned n_reduce_db;
+
+    long long n_decisions;
+    long long n_propagations;
+    long long n_inspects;
+    long long n_conflicts;
+
+    long long n_original_lits;
+    long long n_learnt_lits;
+};
+
+typedef struct solver_t_ solver_t;
+struct solver_t_ {
+    /* User data */
+    vec_uint_t *assumptions;
+    vec_uint_t *final_conflict;
+
+    /* Clauses Database */
+    struct cdb *all_clauses;
+    vec_uint_t *learnts;
+    vec_uint_t *originals;
+    vec_wl_t *watches;
+    vec_wl_t *bin_watches;
+
+    /* Activity heuristic */
+    act_t var_act_inc; /* Amount to bump next variable with. */
+    clause_act_t clause_act_inc; /* Amount to bump next clause with. */
+
+    /* Variable Information */
+    vec_act_t *activity; /* A heuristic measurement of the activity of a variable. */
+    heap_t *var_order;
+    vec_uint_t *levels;  /* Decision level of the current assignment */
+    vec_uint_t *reasons; /* Reason (clause) of the current assignment */
+    vec_char_t *assigns;
+    vec_char_t *polarity;
+
+    /* Assignments */
+    vec_uint_t *trail;
+    vec_uint_t *trail_lim; /* Separator indices for different decision levels in 'trail'. */
+    unsigned i_qhead; /* Head of propagation queue (as index into the trail). */
+    unsigned n_assigns_simplify; /* Number of top-level assignments since
+                    last execution of 'simplify()'. */
+    long long n_props_simplify;  /* Remaining number of propagations that
+                    must be made before next execution of
+                    'simplify()'. */
+
+    /* Temporary data used by Search method */
+    b_queue_t *bq_trail;
+    b_queue_t *bq_lbd;
+    long RC1;
+    long RC2;
+    unsigned n_confl_bfr_reduce;
+    float sum_lbd;
+
+    /* Temporary data used by Analyze */
+    vec_uint_t *temp_lits;
+    vec_char_t *seen;
+    vec_uint_t *tagged; /* Stack */
+    vec_uint_t *stack;
+    vec_uint_t *last_dlevel;
+
+    /* Misc temporary */
+    vec_uint_t *stamps; /* Multipurpose stamp used to calculate LBD and
+                 * clauses minimization with binary resolution */
+    unsigned cur_stamp; /* Used for marking literals and levels of interest */
+
+    struct satoko_stats stats;
+    struct satoko_opts opts;
+};
+
+//===------------------------------------------------------------------------===
+extern unsigned solver_clause_create(solver_t *, vec_uint_t *, unsigned);
+extern char solver_search(solver_t *);
+extern void solver_cancel_until(solver_t *, unsigned);
+extern unsigned solver_propagate(solver_t *);
+extern void solver_debug_check(solver_t *, int);
+
+//===------------------------------------------------------------------------===
+// Inline var/lit functions
+//===------------------------------------------------------------------------===
+static inline unsigned var2lit(unsigned var, char polarity)
+{
+    return var + var + ((unsigned) polarity != 0);
+}
+
+static inline unsigned lit2var(unsigned lit)
+{
+    return lit >> 1;
+}
+//===------------------------------------------------------------------------===
+// Inline var functions
+//===------------------------------------------------------------------------===
+static inline char var_value(solver_t *s, unsigned var)
+{
+    return vec_char_at(s->assigns, var);
+}
+
+static inline unsigned var_dlevel(solver_t *s, unsigned var)
+{
+    return vec_uint_at(s->levels, var);
+}
+
+static inline unsigned var_reason(solver_t *s, unsigned var)
+{
+    return vec_uint_at(s->reasons, var);
+}
+//===------------------------------------------------------------------------===
+// Inline lit functions
+//===------------------------------------------------------------------------===
+static inline unsigned lit_neg(unsigned lit)
+{
+    return lit ^ 1;
+}
+
+static inline char lit_polarity(unsigned lit)
+{
+    return (char)(lit & 1);
+}
+
+static inline char lit_value(solver_t *s, unsigned lit)
+{
+    return lit_polarity(lit) ^ vec_char_at(s->assigns, lit2var(lit));
+}
+
+static inline unsigned lit_dlevel(solver_t *s, unsigned lit)
+{
+    return vec_uint_at(s->levels, lit2var(lit));
+}
+
+static inline unsigned lit_reason(solver_t *s, unsigned lit)
+{
+    return vec_uint_at(s->reasons, lit2var(lit));
+}
+//===------------------------------------------------------------------------===
+// Inline solver minor functions
+//===------------------------------------------------------------------------===
+static inline unsigned solver_check_limits(solver_t *s)
+{
+    return (s->opts.conf_limit == 0 || s->opts.conf_limit >= s->stats.n_conflicts) &&
+           (s->opts.prop_limit == 0 || s->opts.prop_limit >= s->stats.n_propagations);
+}
+
+/** Returns current decision level */
+static inline unsigned solver_dlevel(solver_t *s)
+{
+    return vec_uint_size(s->trail_lim);
+}
+
+static inline int solver_enqueue(solver_t *s, unsigned lit, unsigned reason)
+{
+    unsigned var = lit2var(lit);
+
+    vec_char_assign(s->assigns, var, lit_polarity(lit));
+    vec_uint_assign(s->levels, var, solver_dlevel(s));
+    vec_uint_assign(s->reasons, var, reason);
+    vec_uint_push_back(s->trail, lit);
+    return SATOKO_OK;
+}
+
+//===------------------------------------------------------------------------===
+// Inline clause functions
+//===------------------------------------------------------------------------===
+static inline struct clause *clause_read(solver_t *s, unsigned cref)
+{
+    return cdb_handler(s->all_clauses, cref);
+}
+
+static inline void clause_watch(solver_t *s, unsigned cref)
+{
+    struct clause *clause = cdb_handler(s->all_clauses, cref);
+    struct watcher w1;
+    struct watcher w2;
+
+    w1.cref = cref;
+    w2.cref = cref;
+    w1.blocker = clause->data[1].lit;
+    w2.blocker = clause->data[0].lit;
+    if (clause->size == 2) {
+        watch_list_push(vec_wl_at(s->bin_watches, lit_neg(clause->data[0].lit)), w1);
+        watch_list_push(vec_wl_at(s->bin_watches, lit_neg(clause->data[1].lit)), w2);
+    } else {
+        watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), w1);
+        watch_list_push(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), w2);
+    }
+}
+
+static inline void clause_unwatch(solver_t *s, unsigned cref)
+{
+    struct clause *clause = cdb_handler(s->all_clauses, cref);
+    if (clause->size == 2) {
+        watch_list_remove(vec_wl_at(s->bin_watches, lit_neg(clause->data[0].lit)), cref);
+        watch_list_remove(vec_wl_at(s->bin_watches, lit_neg(clause->data[1].lit)), cref);
+    } else {
+        watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[0].lit)), cref);
+        watch_list_remove(vec_wl_at(s->watches, lit_neg(clause->data[1].lit)), cref);
+    }
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__solver_h */
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
new file mode 100644
index 00000000..db9a267b
--- /dev/null
+++ b/src/sat/satoko/solver_api.c
@@ -0,0 +1,310 @@
+//===--- solver_api.h -------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "act_var.h"
+#include "utils/misc.h"
+#include "solver.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_IMPL_START
+
+//===------------------------------------------------------------------------===
+// Satoko internal functions
+//===------------------------------------------------------------------------===
+static inline void solver_rebuild_order(solver_t *s)
+{
+    unsigned var;
+    vec_uint_t *vars = vec_uint_alloc(vec_char_size(s->assigns));
+
+    for (var = 0; var < vec_char_size(s->assigns); var++)
+        if (var_value(s, var) == VAR_UNASSING)
+            vec_uint_push_back(vars, var);
+    heap_build(s->var_order, vars);
+    vec_uint_free(vars);
+}
+
+static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
+{
+    unsigned i;
+    unsigned *lits = &(clause->data[0].lit);
+    for (i = 0; i < clause->size; i++)
+        if (lit_value(s, lits[i]) == LIT_TRUE)
+            return SATOKO_OK;
+    return SATOKO_ERR;
+}
+
+static inline void print_opts(solver_t *s)
+{
+    printf( "+-[ BLACK MAGIC - PARAMETERS ]-+\n");
+    printf( "|                              |\n");
+    printf( "|--> Restarts heuristic        |\n");
+    printf( "|    * LBD Queue   = %6d    |\n", s->opts.sz_lbd_bqueue);
+    printf( "|    * Trail Queue = %6d    |\n", s->opts.sz_trail_bqueue);
+    printf( "|    * f_rst       = %6.2f    |\n", s->opts.f_rst);
+    printf( "|    * b_rst       = %6.2f    |\n", s->opts.b_rst);
+    printf( "|                              |\n");
+    printf( "|--> Clause DB reduction:      |\n");
+    printf( "|    * First       = %6d    |\n", s->opts.n_conf_fst_reduce);
+    printf( "|    * Inc         = %6d    |\n", s->opts.inc_reduce);
+    printf( "|    * Special Inc = %6d    |\n", s->opts.inc_special_reduce);
+    printf( "|    * Protected (LBD) < %2d    |\n", s->opts.lbd_freeze_clause);
+    printf( "|                              |\n");
+    printf( "|--> Binary resolution:        |\n");
+    printf( "|    * Clause size < %3d       |\n", s->opts.clause_max_sz_bin_resol);
+    printf( "|    * Clause lbd  < %3d       |\n", s->opts.clause_min_lbd_bin_resol);
+    printf( "+------------------------------+\n\n");
+}
+
+static inline void print_stats(solver_t *s)
+{
+    printf("starts        : %10d\n", s->stats.n_starts);
+    printf("conflicts     : %10lld\n", s->stats.n_conflicts);
+    printf("decisions     : %10lld\n", s->stats.n_decisions);
+    printf("propagations  : %10lld\n", s->stats.n_propagations);
+}
+
+//===------------------------------------------------------------------------===
+// Satoko external functions
+//===------------------------------------------------------------------------===
+solver_t * satoko_create()
+{
+    solver_t *s = satoko_calloc(solver_t, 1);
+
+    satoko_default_opts(&s->opts);
+    /* User data */
+    s->assumptions = vec_uint_alloc(0);
+    s->final_conflict = vec_uint_alloc(0);
+    /* Clauses Database */
+    s->all_clauses = cdb_alloc(0);
+    s->originals = vec_uint_alloc(0);
+    s->learnts = vec_uint_alloc(0);
+    s->watches = vec_wl_alloc(0);
+    s->bin_watches = vec_wl_alloc(0);
+    /* Activity heuristic */
+    s->var_act_inc = VAR_ACT_INIT_INC;
+    s->clause_act_inc = CLAUSE_ACT_INIT_INC;
+    /* Variable Information */
+    s->activity = vec_act_alloc(0);
+    s->var_order = heap_alloc(s->activity);
+    s->levels = vec_uint_alloc(0);
+    s->reasons = vec_uint_alloc(0);
+    s->assigns = vec_char_alloc(0);
+    s->polarity = vec_char_alloc(0);
+    /* Assignments */
+    s->trail = vec_uint_alloc(0);
+    s->trail_lim = vec_uint_alloc(0);
+    /* Temporary data used by Search method */
+    s->bq_trail = b_queue_alloc(s->opts.sz_trail_bqueue);
+    s->bq_lbd = b_queue_alloc(s->opts.sz_lbd_bqueue);
+    s->n_confl_bfr_reduce = s->opts.n_conf_fst_reduce;
+    s->RC1 = 1;
+    s->RC2 = s->opts.n_conf_fst_reduce;
+    /* Temporary data used by Analyze */
+    s->temp_lits = vec_uint_alloc(0);
+    s->seen = vec_char_alloc(0);
+    s->tagged = vec_uint_alloc(0);
+    s->stack = vec_uint_alloc(0);
+    s->last_dlevel = vec_uint_alloc(0);
+    /* Misc temporary */
+    s->stamps = vec_uint_alloc(0);
+    return s;
+}
+
+void satoko_destroy(solver_t *s)
+{
+    vec_uint_free(s->assumptions);
+    vec_uint_free(s->final_conflict);
+    cdb_free(s->all_clauses);
+    vec_uint_free(s->originals);
+    vec_uint_free(s->learnts);
+    vec_wl_free(s->watches);
+    vec_wl_free(s->bin_watches);
+    vec_act_free(s->activity);
+    heap_free(s->var_order);
+    vec_uint_free(s->levels);
+    vec_uint_free(s->reasons);
+    vec_char_free(s->assigns);
+    vec_char_free(s->polarity);
+    vec_uint_free(s->trail);
+    vec_uint_free(s->trail_lim);
+    b_queue_free(s->bq_lbd);
+    b_queue_free(s->bq_trail);
+    vec_uint_free(s->temp_lits);
+    vec_char_free(s->seen);
+    vec_uint_free(s->tagged);
+    vec_uint_free(s->stack);
+    vec_uint_free(s->last_dlevel);
+    vec_uint_free(s->stamps);
+    satoko_free(s);
+}
+
+void satoko_default_opts(satoko_opts_t *opts)
+{
+    opts->verbose = 0;
+    /* Limits */
+    opts->conf_limit = 0;
+    opts->prop_limit  = 0;
+    /* Constants used for restart heuristic */
+    opts->f_rst = 0.8;
+    opts->b_rst = 1.4;
+    opts->fst_block_rst   = 10000;
+    opts->sz_lbd_bqueue   = 50;
+    opts->sz_trail_bqueue = 5000;
+    /* Constants used for clause database reduction heuristic */
+    opts->n_conf_fst_reduce = 2000;
+    opts->inc_reduce = 300;
+    opts->inc_special_reduce = 1000;
+    opts->lbd_freeze_clause = 30;
+    /* VSIDS heuristic */
+    opts->var_decay = 0.95;
+    opts->clause_decay = 0.995;
+    /* Binary resolution */
+    opts->clause_max_sz_bin_resol = 30;
+    opts->clause_min_lbd_bin_resol = 6;
+
+    opts->garbage_max_ratio = 0.3;
+}
+
+/**
+ * TODO: sanity check on configuration options
+ */
+void satoko_configure(satoko_t *s, satoko_opts_t *user_opts)
+{
+    assert(user_opts);
+    memcpy(&s->opts, user_opts, sizeof(satoko_opts_t));
+}
+
+int satoko_simplify(solver_t * s)
+{
+    unsigned i, j = 0;
+        unsigned cref;
+
+    assert(solver_dlevel(s) == 0);
+    if (solver_propagate(s) != UNDEF)
+        return SATOKO_ERR;
+    if (s->n_assigns_simplify == vec_uint_size(s->trail) || s->n_props_simplify > 0)
+        return SATOKO_OK;
+
+    vec_uint_foreach(s->originals, cref, i) {
+        struct clause *clause = clause_read(s, cref);
+
+            if (clause_is_satisfied(s, clause)) {
+            clause->f_mark = 1;
+            s->stats.n_original_lits -= clause->size;
+            clause_unwatch(s, cref);
+        } else
+            vec_uint_assign(s->originals, j++, cref);
+    }
+    vec_uint_shrink(s->originals, j);
+    solver_rebuild_order(s);
+    s->n_assigns_simplify = vec_uint_size(s->trail);
+    s->n_props_simplify = s->stats.n_original_lits + s->stats.n_learnt_lits;
+    return SATOKO_OK;
+}
+
+void satoko_add_variable(solver_t *s, char sign)
+{
+    unsigned var = vec_act_size(s->activity);
+    vec_wl_push(s->bin_watches);
+    vec_wl_push(s->bin_watches);
+    vec_wl_push(s->watches);
+    vec_wl_push(s->watches);
+    vec_act_push_back(s->activity, 0);
+    vec_uint_push_back(s->levels, 0);
+    vec_char_push_back(s->assigns, VAR_UNASSING);
+    vec_char_push_back(s->polarity, sign);
+    vec_uint_push_back(s->reasons, UNDEF);
+    vec_uint_push_back(s->stamps, 0);
+    vec_char_push_back(s->seen, 0);
+    heap_insert(s->var_order, var);
+}
+
+int satoko_add_clause(solver_t *s, unsigned *lits, unsigned size)
+{
+    unsigned i, j;
+    unsigned prev_lit;
+    unsigned max_var;
+    unsigned cref;
+
+    qsort((void *) lits, size, sizeof(unsigned), mkt_uint_compare);
+    max_var = lit2var(lits[size - 1]);
+    while (max_var >= vec_act_size(s->activity))
+        satoko_add_variable(s, LIT_FALSE);
+
+    vec_uint_clear(s->temp_lits);
+    j = 0;
+    prev_lit = UNDEF;
+    for (i = 0; i < size; i++) {
+        if (lits[i] == lit_neg(prev_lit) || lit_value(s, lits[i]) == LIT_TRUE)
+            return SATOKO_OK;
+        else if (lits[i] != prev_lit && var_value(s, lit2var(lits[i])) == VAR_UNASSING) {
+            prev_lit = lits[i];
+            vec_uint_push_back(s->temp_lits, lits[i]);
+        }
+    }
+
+    if (vec_uint_size(s->temp_lits) == 0)
+        return SATOKO_ERR;
+    if (vec_uint_size(s->temp_lits) == 1) {
+        solver_enqueue(s, vec_uint_at(s->temp_lits, 0), UNDEF);
+        return (solver_propagate(s) == UNDEF);
+    }
+
+    cref = solver_clause_create(s, s->temp_lits, 0);
+    clause_watch(s, cref);
+    return SATOKO_OK;
+}
+
+void satoko_assump_push(solver_t *s, unsigned lit)
+{
+    vec_uint_push_back(s->assumptions, lit);
+}
+
+void satoko_assump_pop(solver_t *s)
+{
+    assert(vec_uint_size(s->assumptions) > 0);
+    vec_uint_pop_back(s->assumptions);
+    solver_cancel_until(s, vec_uint_size(s->assumptions));
+}
+
+int satoko_solve(solver_t *s)
+{
+    char status = SATOKO_UNDEC;
+
+    assert(s);
+    if (s->opts.verbose)
+        print_opts(s);
+
+    while (status == SATOKO_UNDEC) {
+        status = solver_search(s);
+        if (solver_check_limits(s) == 0)
+            break;
+    }
+    if (s->opts.verbose)
+        print_stats(s);
+    solver_cancel_until(s, vec_uint_size(s->assumptions));
+    return status;
+}
+
+int satoko_final_conflict(solver_t *s, unsigned *out)
+{
+    if (vec_uint_size(s->final_conflict) == 0)
+        return -1;
+    out = satoko_alloc(unsigned, vec_uint_size(s->final_conflict));
+    memcpy(out, vec_uint_data(s->final_conflict),
+           sizeof(unsigned) * vec_uint_size(s->final_conflict));
+    return vec_uint_size(s->final_conflict);
+
+}
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h
new file mode 100644
index 00000000..2811c2c6
--- /dev/null
+++ b/src/sat/satoko/types.h
@@ -0,0 +1,50 @@
+//===--- types.h ------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__types_h
+#define satoko__types_h
+
+#include "utils/vec/vec_dble.h"
+#include "utils/vec/vec_uint.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#define SATOKO_ACT_VAR_DBLE
+#define SATOKO_ACT_CLAUSE_FLOAT
+
+#ifdef SATOKO_ACT_VAR_DBLE
+    #define VAR_ACT_INIT_INC 1.0
+    typedef double act_t;
+    typedef vec_dble_t vec_act_t ;
+    #define vec_act_alloc(size) vec_dble_alloc(size)
+    #define vec_act_free(vec) vec_dble_free(vec)
+    #define vec_act_size(vec) vec_dble_size(vec)
+    #define vec_act_at(vec, idx) vec_dble_at(vec, idx)
+    #define vec_act_push_back(vec, value) vec_dble_push_back(vec, value)
+#else
+    #define VAR_ACT_INIT_INC (1 << 5)
+    typedef unsigned act_t;
+    typedef    vec_uint_t vec_act_t;
+    #define vec_act_alloc(size) vec_uint_alloc(size)
+    #define vec_act_free(vec) vec_uint_free(vec)
+    #define vec_act_size(vec) vec_uint_size(vec)
+    #define vec_act_at(vec, idx) vec_uint_at(vec, idx)
+    #define vec_act_push_back(vec, value) vec_uint_push_back(vec, value)
+#endif /* SATOKO_ACT_VAR_DBLE */
+
+#ifdef SATOKO_ACT_CLAUSE_FLOAT
+    #define CLAUSE_ACT_INIT_INC 1.0
+    typedef float clause_act_t;
+#else
+    #define CLAUSE_ACT_INIT_INC (1 << 11)
+    typedef unsigned clause_act_t;
+#endif /* SATOKO_ACT_CLAUSE_FLOAT */
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__types_h */
diff --git a/src/sat/satoko/utils/b_queue.h b/src/sat/satoko/utils/b_queue.h
new file mode 100644
index 00000000..926edf29
--- /dev/null
+++ b/src/sat/satoko/utils/b_queue.h
@@ -0,0 +1,81 @@
+//===--- b_queue.h ----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__b_queue_h
+#define satoko__utils__b_queue_h
+
+#include "mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+/* Bounded Queue */
+typedef struct b_queue_t_ b_queue_t;
+struct b_queue_t_ {
+    unsigned size;
+    unsigned cap;
+    unsigned i_first;
+    unsigned i_empty;
+    unsigned long long sum;
+    unsigned *data;
+};
+
+//===------------------------------------------------------------------------===
+// Bounded Queue API
+//===------------------------------------------------------------------------===
+static inline b_queue_t *b_queue_alloc(unsigned cap)
+{
+    b_queue_t *p = satoko_calloc(b_queue_t, 1);
+    p->cap = cap;
+    p->data = satoko_calloc(unsigned, cap);
+    return p;
+}
+
+static inline void b_queue_free(b_queue_t *p)
+{
+    satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline void b_queue_push(b_queue_t *p, unsigned Value)
+{
+    if (p->size == p->cap) {
+        assert(p->i_first == p->i_empty);
+        p->sum -= p->data[p->i_first];
+        p->i_first = (p->i_first + 1) % p->cap;
+    } else
+        p->size++;
+
+    p->sum += Value;
+    p->data[p->i_empty] = Value;
+    if ((++p->i_empty) == p->cap) {
+        p->i_empty = 0;
+        p->i_first = 0;
+    }
+}
+
+static inline unsigned b_queue_avg(b_queue_t *p)
+{
+    return (unsigned)(p->sum / ((unsigned long long) p->size));
+}
+
+static inline unsigned b_queue_is_valid(b_queue_t *p)
+{
+    return (p->cap == p->size);
+}
+
+static inline void b_queue_clean(b_queue_t *p)
+{
+    p->i_first = 0;
+    p->i_empty = 0;
+    p->size = 0;
+    p->sum = 0;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__b_queue_h */
diff --git a/src/sat/satoko/utils/heap.h b/src/sat/satoko/utils/heap.h
new file mode 100644
index 00000000..e1611e95
--- /dev/null
+++ b/src/sat/satoko/utils/heap.h
@@ -0,0 +1,181 @@
+//===--- heap.h ----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__heap_h
+#define satoko__utils__heap_h
+
+#include "mem.h"
+#include "../types.h"
+#include "vec/vec_dble.h"
+#include "vec/vec_int.h"
+#include "vec/vec_uint.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct heap_t_ heap_t;
+struct heap_t_ {
+    vec_int_t *indices;
+    vec_uint_t *data;
+    vec_act_t *weights;
+};
+//===------------------------------------------------------------------------===
+// Heap internal functions
+//===------------------------------------------------------------------------===
+static inline unsigned left(unsigned i) { return 2 * i + 1; }
+static inline unsigned right(unsigned i) { return (i + 1) * 2; }
+static inline unsigned parent(unsigned i) { return (i - 1) >> 1; }
+
+static inline int compare(heap_t *p, unsigned x, unsigned y)
+{
+    return vec_act_at(p->weights, x) > vec_act_at(p->weights, y);
+}
+
+static inline void heap_percolate_up(heap_t *h, unsigned i)
+{
+    unsigned x = vec_uint_at(h->data, i);
+    unsigned p = parent(i);
+
+    while (i != 0 && compare(h, x, vec_uint_at(h->data, p))) {
+        vec_uint_assign(h->data, i, vec_uint_at(h->data, p));
+        vec_int_assign(h->indices, vec_uint_at(h->data, p), (int) i);
+        i = p;
+        p = parent(p);
+    }
+    vec_uint_assign(h->data, i, x);
+    vec_int_assign(h->indices, x, (int) i);
+}
+
+static inline void heap_percolate_down(heap_t *h, unsigned i)
+{
+    unsigned x = vec_uint_at(h->data, i);
+
+    while (left(i) < vec_uint_size(h->data)) {
+        unsigned child = right(i) < vec_uint_size(h->data) &&
+                     compare(h, vec_uint_at(h->data, right(i)), vec_uint_at(h->data, left(i)))
+                   ? right(i)
+                   : left(i);
+
+        if (!compare(h, vec_uint_at(h->data, child), x))
+            break;
+
+        vec_uint_assign(h->data, i, vec_uint_at(h->data, child));
+        vec_int_assign(h->indices, vec_uint_at(h->data, i), (int) i);
+        i = child;
+    }
+    vec_uint_assign(h->data, i, x);
+    vec_int_assign(h->indices, x, (int) i);
+}
+
+//===------------------------------------------------------------------------===
+// Heap API
+//===------------------------------------------------------------------------===
+static inline heap_t *heap_alloc(vec_act_t *weights)
+{
+    heap_t *p = satoko_alloc(heap_t, 1);
+    p->weights = weights;
+    p->indices = vec_int_alloc(0);
+    p->data = vec_uint_alloc(0);
+    return p;
+}
+
+static inline void heap_free(heap_t *p)
+{
+    vec_int_free(p->indices);
+    vec_uint_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned heap_size(heap_t *p)
+{
+    return vec_uint_size(p->data);
+}
+
+static inline int heap_in_heap(heap_t *p, unsigned entry)
+{
+    return (entry < vec_int_size(p->indices)) &&
+           (vec_int_at(p->indices, entry) >= 0);
+}
+
+static inline void heap_increase(heap_t *p, unsigned entry)
+{
+    assert(heap_in_heap(p, entry));
+    heap_percolate_down(p, (unsigned) vec_int_at(p->indices, entry));
+}
+
+static inline void heap_decrease(heap_t *p, unsigned entry)
+{
+    assert(heap_in_heap(p, entry));
+    heap_percolate_up(p, (unsigned) vec_int_at(p->indices, entry));
+}
+
+static inline void heap_insert(heap_t *p, unsigned entry)
+{
+    if (vec_int_size(p->indices) < entry + 1) {
+        unsigned old_size = vec_int_size(p->indices);
+        unsigned i;
+        int e;
+        vec_int_resize(p->indices, entry + 1);
+        vec_int_foreach_start(p->indices, e, i, old_size)
+            vec_int_assign(p->indices, i, -1);
+    }
+    assert(!heap_in_heap(p, entry));
+    vec_int_assign(p->indices, entry, (int) vec_uint_size(p->data));
+    vec_uint_push_back(p->data, entry);
+    heap_percolate_up(p, (unsigned) vec_int_at(p->indices, entry));
+}
+
+static inline void heap_update(heap_t *p, unsigned i)
+{
+    if (!heap_in_heap(p, i))
+        heap_insert(p, i);
+    else {
+        heap_percolate_up(p, (unsigned) vec_int_at(p->indices, i));
+        heap_percolate_down(p, (unsigned) vec_int_at(p->indices, i));
+    }
+}
+
+static inline void heap_build(heap_t *p, vec_uint_t *entries)
+{
+    int i;
+    unsigned j, entry;
+
+    vec_uint_foreach(p->data, entry, j)
+        vec_int_assign(p->indices, entry, -1);
+    vec_uint_clear(p->data);
+    vec_uint_foreach(entries, entry, j) {
+        vec_int_assign(p->indices, entry, (int) j);
+        vec_uint_push_back(p->data, entry);
+    }
+    for ((i = vec_uint_size(p->data) / 2 - 1); i >= 0; i--)
+        heap_percolate_down(p, (unsigned) i);
+}
+
+static inline void heap_clear(heap_t *p)
+{
+    unsigned i;
+    int entry;
+    vec_int_foreach(p->indices, entry, i)
+        vec_int_assign(p->indices, i, -1);
+    vec_uint_clear(p->data);
+}
+
+static inline unsigned heap_remove_min(heap_t *p)
+{
+    unsigned x = vec_uint_at(p->data, 0);
+    vec_uint_assign(p->data, 0, vec_uint_at(p->data, vec_uint_size(p->data) - 1));
+    vec_int_assign(p->indices, vec_uint_at(p->data, 0), 0);
+    vec_int_assign(p->indices, x, -1);
+    vec_uint_pop_back(p->data);
+    if (vec_uint_size(p->data) > 1)
+        heap_percolate_down(p, 0);
+    return x;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__heap_h */
diff --git a/src/sat/satoko/utils/mem.h b/src/sat/satoko/utils/mem.h
new file mode 100755
index 00000000..5ff9873d
--- /dev/null
+++ b/src/sat/satoko/utils/mem.h
@@ -0,0 +1,23 @@
+//===--- mem.h --------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__mem_h
+#define satoko__utils__mem_h
+
+#include <stdlib.h>
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#define satoko_alloc(type, n_elements) ((type *) malloc((n_elements) * sizeof(type)))
+#define satoko_calloc(type, n_elements) ((type *) calloc((n_elements), sizeof(type)))
+#define satoko_realloc(type, ptr, n_elements) ((type *) realloc(ptr, (n_elements) * sizeof(type)))
+#define satoko_free(p) do { free(p); p = NULL; } while(0)
+
+ABC_NAMESPACE_HEADER_END
+#endif
diff --git a/src/sat/satoko/utils/misc.h b/src/sat/satoko/utils/misc.h
new file mode 100755
index 00000000..aa8bcb8c
--- /dev/null
+++ b/src/sat/satoko/utils/misc.h
@@ -0,0 +1,37 @@
+//===--- misc.h -------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__misc_h
+#define satoko__utils__misc_h
+
+#include <stdint.h>
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+#define mkt_swap(type, a, b)  { type t = a; a = b; b = t; }
+
+static inline unsigned mkt_uint_max(unsigned a, unsigned b)
+{
+    return a > b ?  a : b;
+}
+
+static inline int mkt_uint_compare(const void *p1, const void *p2)
+{
+    const unsigned pp1 = *(const unsigned *)p1;
+    const unsigned pp2 = *(const unsigned *)p2;
+
+    if (pp1 < pp2)
+        return -1;
+    if (pp1 > pp2)
+        return 1;
+    return 0;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__misc_h */
diff --git a/src/sat/satoko/utils/sort.h b/src/sat/satoko/utils/sort.h
new file mode 100644
index 00000000..285f4b91
--- /dev/null
+++ b/src/sat/satoko/utils/sort.h
@@ -0,0 +1,65 @@
+//===--- sort.h -------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__sort_h
+#define satoko__utils__sort_h
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+static inline void select_sort(void **data, unsigned size,
+                   int (*comp_fn)(const void *, const void *))
+{
+    unsigned i, j, i_best;
+    void *temp;
+
+    for (i = 0; i < (size - 1); i++) {
+        i_best = i;
+        for (j = i + 1; j < size; j++) {
+            if (comp_fn(data[j], data[i_best]))
+                i_best = j;
+        }
+        temp = data[i];
+        data[i] = data[i_best];
+        data[i_best] = temp;
+    }
+}
+
+static void satoko_sort(void **data, unsigned size,
+            int (*comp_fn)(const void *, const void *))
+{
+    if (size <= 15)
+        select_sort(data, size, comp_fn);
+    else {
+        void *pivot = data[size / 2];
+        void *temp;
+        unsigned j = size;
+        int i = -1;
+
+        for (;;) {
+            do {
+                i++;
+            } while (comp_fn(data[i], pivot));
+            do {
+                j--;
+            } while (comp_fn(pivot, data[j]));
+
+            if ((unsigned) i >= j)
+                break;
+
+            temp = data[i];
+            data[i] = data[j];
+            data[j] = temp;
+        }
+        satoko_sort(data, (unsigned) i, comp_fn);
+        satoko_sort(data + i, (size - (unsigned) i), comp_fn);
+    }
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__sort_h */
diff --git a/src/sat/satoko/utils/vec/vec_char.h b/src/sat/satoko/utils/vec/vec_char.h
new file mode 100644
index 00000000..fe88797a
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_char.h
@@ -0,0 +1,259 @@
+//===--- vec_char.h ---------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_char_h
+#define satoko__utils__vec__vec_char_h
+
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "../mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct vec_char_t_ vec_char_t;
+struct vec_char_t_ {
+    unsigned cap;
+    unsigned size;
+    char *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_char_foreach(vec, entry, i) \
+    for (i = 0; (i < vec_char_size(vec)) && (((entry) = vec_char_at(vec, i)), 1); i++)
+
+#define vec_char_foreach_start(vec, entry, i, start) \
+    for (i = start; (i < vec_char_size(vec)) && (((entry) = vec_char_at(vec, i)), 1); i++)
+
+#define vec_char_foreach_stop(vec, entry, i, stop) \
+    for (i = 0; (i < stop) && (((entry) = vec_char_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_char_t * vec_char_alloc(unsigned cap)
+{
+    vec_char_t *p = satoko_alloc(vec_char_t, 1);
+
+    if (cap > 0 && cap < 16)
+        cap = 16;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(char, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_char_t * vec_char_alloc_exact(unsigned cap)
+{
+    vec_char_t *p = satoko_alloc(vec_char_t, 1);
+
+    cap = 0;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(char, p->cap ) : NULL;
+    return p;
+}
+
+static inline vec_char_t * vec_char_init(unsigned size, char value)
+{
+    vec_char_t *p = satoko_alloc(vec_char_t, 1);
+
+    p->cap = size;
+    p->size = size;
+    p->data = p->cap ? satoko_alloc(char, p->cap) : NULL;
+    memset(p->data, value, sizeof(char) * p->size);
+    return p;
+}
+
+static inline void vec_char_free(vec_char_t *p)
+{
+    if (p->data != NULL)
+        satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned vec_char_size(vec_char_t *p)
+{
+    return p->size;
+}
+
+static inline void vec_char_resize(vec_char_t *p, unsigned new_size)
+{
+    p->size = new_size;
+    if (p->cap >= new_size)
+        return;
+    p->data = satoko_realloc(char, p->data, new_size);
+    assert(p->data != NULL);
+    p->cap = new_size;
+}
+
+static inline void vec_char_shrink(vec_char_t *p, unsigned new_size)
+{
+    assert(p->cap > new_size);
+    p->size = new_size;
+}
+
+static inline void vec_char_reserve(vec_char_t *p, unsigned new_cap)
+{
+    if (p->cap >= new_cap)
+        return;
+    p->data = satoko_realloc(char, p->data, new_cap);
+    assert(p->data != NULL);
+    p->cap = new_cap;
+}
+
+static inline unsigned vec_char_capacity(vec_char_t *p)
+{
+    return p->cap;
+}
+
+static inline int vec_char_empty(vec_char_t *p)
+{
+    return p->size ? 0 : 1;
+}
+
+static inline void vec_char_erase(vec_char_t *p)
+{
+    satoko_free(p->data);
+    p->size = 0;
+    p->cap = 0;
+}
+
+static inline char vec_char_at(vec_char_t *p, unsigned idx)
+{
+    assert(idx >= 0 && idx < p->size);
+    return p->data[idx];
+}
+
+static inline char * vec_char_at_ptr(vec_char_t *p, unsigned idx)
+{
+    assert(idx >= 0 && idx < p->size);
+    return p->data + idx;
+}
+
+static inline char * vec_char_data(vec_char_t *p)
+{
+    assert(p);
+    return p->data;
+}
+
+static inline void vec_char_duplicate(vec_char_t *dest, const vec_char_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_char_resize(dest, src->cap);
+    memcpy(dest->data, src->data, sizeof(char) * src->cap);
+    dest->size = src->size;
+}
+
+static inline void vec_char_copy(vec_char_t *dest, const vec_char_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_char_resize(dest, src->size);
+    memcpy(dest->data, src->data, sizeof(char) * src->size);
+    dest->size = src->size;
+}
+
+static inline void vec_char_push_back(vec_char_t *p, char value)
+{
+    if (p->size == p->cap) {
+        if (p->cap < 16)
+            vec_char_reserve(p, 16);
+        else
+            vec_char_reserve(p, 2 * p->cap);
+    }
+    p->data[p->size] = value;
+    p->size++;
+}
+
+static inline char vec_char_pop_back(vec_char_t *p)
+{
+    assert(p && p->size);
+    return p->data[--p->size];
+}
+
+static inline void vec_char_assign(vec_char_t *p, unsigned idx, char value)
+{
+    assert((idx >= 0) && (idx < vec_char_size(p)));
+    p->data[idx] = value;
+}
+
+static inline void vec_char_insert(vec_char_t *p, unsigned idx, char value)
+{
+    assert((idx >= 0) && (idx < vec_char_size(p)));
+    vec_char_push_back(p, 0);
+    memmove(p->data + idx + 1, p->data + idx, (p->size - idx - 2) * sizeof(char));
+    p->data[idx] = value;
+}
+
+static inline void vec_char_drop(vec_char_t *p, unsigned idx)
+{
+    assert((idx >= 0) && (idx < vec_char_size(p)));
+    memmove(p->data + idx, p->data + idx + 1, (p->size - idx - 1) * sizeof(char));
+    p->size -= 1;
+}
+
+static inline void vec_char_clear(vec_char_t *p)
+{
+    p->size = 0;
+}
+
+static inline int vec_char_asc_compare(const void *p1, const void *p2)
+{
+    const char *pp1 = (const char *)p1;
+    const char *pp2 = (const char *)p2;
+
+    if (*pp1 < *pp2)
+        return -1;
+    if (*pp1 > *pp2)
+        return 1;
+    return 0;
+}
+
+static inline int vec_char_desc_compare(const void *p1, const void *p2)
+{
+    const char *pp1 = (const char *)p1;
+    const char *pp2 = (const char *)p2;
+
+    if (*pp1 > *pp2)
+        return -1;
+    if (*pp1 < *pp2)
+        return 1;
+    return 0;
+}
+
+static inline void vec_char_sort(vec_char_t *p, int ascending)
+{
+    if (ascending)
+        qsort((void *) p->data, p->size, sizeof(char),
+              (int (*)(const void *, const void *)) vec_char_asc_compare);
+    else
+        qsort((void*) p->data, p->size, sizeof(char),
+              (int (*)(const void *, const void *)) vec_char_desc_compare);
+}
+
+
+static inline long vec_char_memory(vec_char_t *p)
+{
+    return p == NULL ? 0 : sizeof(char) * p->cap + sizeof(vec_char_t);
+}
+
+static inline void vec_char_print(vec_char_t* p)
+{
+    assert(p != NULL);
+    fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
+    for (unsigned i = 0; i < p->size; i++)
+        fprintf(stdout, " %d", p->data[i]);
+    fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_char_h */
diff --git a/src/sat/satoko/utils/vec/vec_dble.h b/src/sat/satoko/utils/vec/vec_dble.h
new file mode 100755
index 00000000..50281c2a
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_dble.h
@@ -0,0 +1,246 @@
+//===--- vec_int.h ----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_dble_h
+#define satoko__utils__vec__vec_dble_h
+
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "../mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct vec_dble_t_ vec_dble_t;
+struct vec_dble_t_ {
+    unsigned cap;
+    unsigned size;
+    double *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_dble_foreach(vec, entry, i) \
+    for (i = 0; (i < vec->size) && (((entry) = vec_dble_at(vec, i)), 1); i++)
+
+#define vec_dble_foreach_start(vec, entry, i, start) \
+    for (i = start; (i < vec_dble_size(vec)) && (((entry) = vec_dble_at(vec, i)), 1); i++)
+
+#define vec_dble_foreach_stop(vec, entry, i, stop) \
+    for (i = 0; (i < stop) && (((entry) = vec_dble_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_dble_t *vec_dble_alloc(unsigned cap)
+{
+    vec_dble_t* p = satoko_alloc(vec_dble_t, 1);
+
+    if (cap > 0 && cap < 16)
+        cap = 16;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(double, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_dble_t *vec_dble_alloc_exact(unsigned cap)
+{
+    vec_dble_t* p = satoko_alloc(vec_dble_t, 1);
+
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(double, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_dble_t *vec_dble_init(unsigned size, double value)
+{
+    vec_dble_t* p = satoko_alloc(vec_dble_t, 1);
+
+    p->cap = size;
+    p->size = size;
+    p->data = p->cap ? satoko_alloc(double, p->cap) : NULL;
+    memset(p->data, value, sizeof(double) * p->size);
+    return p;
+}
+
+static inline void vec_dble_free(vec_dble_t *p)
+{
+    if (p->data != NULL)
+        satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned vec_dble_size(vec_dble_t *p)
+{
+    return p->size;
+}
+
+static inline void vec_dble_resize(vec_dble_t *p, unsigned new_size)
+{
+    p->size = new_size;
+    if (p->cap >= new_size)
+        return;
+    p->data = satoko_realloc(double, p->data, new_size);
+    assert(p->data != NULL);
+    p->cap = new_size;
+}
+
+static inline void vec_dble_reserve(vec_dble_t *p, unsigned new_cap)
+{
+    if (p->cap >= new_cap)
+        return;
+    p->data = satoko_realloc(double, p->data, new_cap);
+    assert(p->data != NULL);
+    p->cap = new_cap;
+}
+
+static inline unsigned vec_dble_capacity(vec_dble_t *p)
+{
+    return p->cap;
+}
+
+static inline int vec_dble_empty(vec_dble_t *p)
+{
+    return p->size ? 0 : 1;
+}
+
+static inline void vec_dble_erase(vec_dble_t *p)
+{
+    satoko_free(p->data);
+    p->size = 0;
+    p->cap = 0;
+}
+
+static inline double vec_dble_at(vec_dble_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data[i];
+}
+
+static inline double *vec_dble_at_ptr(vec_dble_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data + i;
+}
+
+static inline double *vec_dble_data(vec_dble_t *p)
+{
+    assert(p);
+    return p->data;
+}
+
+static inline void vec_dble_duplicate(vec_dble_t *dest, const vec_dble_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_dble_resize(dest, src->cap);
+    memcpy(dest->data, src->data, sizeof(double) * src->cap);
+    dest->size = src->size;
+}
+
+static inline void vec_dble_copy(vec_dble_t *dest, const vec_dble_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_dble_resize(dest, src->size);
+    memcpy(dest->data, src->data, sizeof(double) * src->size);
+    dest->size = src->size;
+}
+
+static inline void vec_dble_push_back(vec_dble_t *p, double value)
+{
+    if (p->size == p->cap) {
+        if (p->cap < 16)
+            vec_dble_reserve(p, 16);
+        else
+            vec_dble_reserve(p, 2 * p->cap);
+    }
+    p->data[p->size] = value;
+    p->size++;
+}
+
+static inline void vec_dble_assign(vec_dble_t *p, unsigned i, double value)
+{
+    assert((i >= 0) && (i < vec_dble_size(p)));
+    p->data[i] = value;
+}
+
+static inline void vec_dble_insert(vec_dble_t *p, unsigned i, double value)
+{
+    assert((i >= 0) && (i < vec_dble_size(p)));
+    vec_dble_push_back(p, 0);
+    memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(double));
+    p->data[i] = value;
+}
+
+static inline void vec_dble_drop(vec_dble_t *p, unsigned i)
+{
+    assert((i >= 0) && (i < vec_dble_size(p)));
+    memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(double));
+    p->size -= 1;
+}
+
+static inline void vec_dble_clear(vec_dble_t *p)
+{
+    p->size = 0;
+}
+
+static inline int vec_dble_asc_compare(const void *p1, const void *p2)
+{
+    const double *pp1 = (const double *) p1;
+    const double *pp2 = (const double *) p2;
+
+    if (*pp1 < *pp2)
+        return -1;
+    if (*pp1 > *pp2)
+        return 1;
+    return 0;
+}
+
+static inline int vec_dble_desc_compare(const void* p1, const void* p2)
+{
+    const double *pp1 = (const double *) p1;
+    const double *pp2 = (const double *) p2;
+
+    if (*pp1 > *pp2)
+        return -1;
+    if (*pp1 < *pp2)
+        return 1;
+    return 0;
+}
+
+static inline void vec_dble_sort(vec_dble_t* p, int ascending)
+{
+    if (ascending)
+        qsort((void *) p->data, p->size, sizeof(double),
+              (int (*)(const void*, const void*)) vec_dble_asc_compare);
+    else
+        qsort((void *) p->data, p->size, sizeof(double),
+              (int (*)(const void*, const void*)) vec_dble_desc_compare);
+}
+
+static inline long vec_dble_memory(vec_dble_t *p)
+{
+    return p == NULL ? 0 : sizeof(double) * p->cap + sizeof(vec_dble_t);
+}
+
+static inline void vec_dble_print(vec_dble_t *p)
+{
+    unsigned i;
+    assert(p != NULL);
+    fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
+    for (i = 0; i < p->size; i++)
+        fprintf(stdout, " %f", p->data[i]);
+    fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_dble_h */
diff --git a/src/sat/satoko/utils/vec/vec_int.h b/src/sat/satoko/utils/vec/vec_int.h
new file mode 100755
index 00000000..75c5d134
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_int.h
@@ -0,0 +1,240 @@
+//===--- vec_int.h ----------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_int_h
+#define satoko__utils__vec__vec_int_h
+
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "../mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct vec_int_t_ vec_int_t;
+struct vec_int_t_ {
+    unsigned cap;
+    unsigned size;
+    int *data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_int_foreach(vec, entry, i) \
+    for (i = 0; (i < vec->size) && (((entry) = vec_int_at(vec, i)), 1); i++)
+
+#define vec_int_foreach_start(vec, entry, i, start) \
+    for (i = start; (i < vec_int_size(vec)) && (((entry) = vec_int_at(vec, i)), 1); i++)
+
+#define vec_int_foreach_stop(vec, entry, i, stop) \
+    for (i = 0; (i < stop) && (((entry) = vec_int_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_int_t *vec_int_alloc(unsigned cap)
+{
+    vec_int_t* p = satoko_alloc(vec_int_t, 1);
+
+    if (cap > 0 && cap < 16)
+        cap = 16;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(int, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_int_t *vec_int_alloc_exact(unsigned cap)
+{
+    vec_int_t* p = satoko_alloc(vec_int_t, 1);
+
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(int, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_int_t *vec_int_init(unsigned size, int value)
+{
+    vec_int_t* p = satoko_alloc(vec_int_t, 1);
+
+    p->cap = size;
+    p->size = size;
+    p->data = p->cap ? satoko_alloc(int, p->cap) : NULL;
+    memset(p->data, value, sizeof(int) * p->size);
+    return p;
+}
+
+static inline void vec_int_free(vec_int_t *p)
+{
+    if (p->data != NULL)
+        satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned vec_int_size(vec_int_t *p)
+{
+    return p->size;
+}
+
+static inline void vec_int_resize(vec_int_t *p, unsigned new_size)
+{
+    p->size = new_size;
+    if (p->cap >= new_size)
+        return;
+    p->data = satoko_realloc(int, p->data, new_size);
+    assert(p->data != NULL);
+    p->cap = new_size;
+}
+
+static inline void vec_int_reserve(vec_int_t *p, unsigned new_cap)
+{
+    if (p->cap >= new_cap)
+        return;
+    p->data = satoko_realloc(int, p->data, new_cap);
+    assert(p->data != NULL);
+    p->cap = new_cap;
+}
+
+static inline unsigned vec_int_capacity(vec_int_t *p)
+{
+    return p->cap;
+}
+
+static inline int vec_int_empty(vec_int_t *p)
+{
+    return p->size ? 0 : 1;
+}
+
+static inline void vec_int_erase(vec_int_t *p)
+{
+    satoko_free(p->data);
+    p->size = 0;
+    p->cap = 0;
+}
+
+static inline int vec_int_at(vec_int_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data[i];
+}
+
+static inline int *vec_int_at_ptr(vec_int_t *p, unsigned i)
+{
+    assert(i >= 0 && i < p->size);
+    return p->data + i;
+}
+
+static inline void vec_int_duplicate(vec_int_t *dest, const vec_int_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_int_resize(dest, src->cap);
+    memcpy(dest->data, src->data, sizeof(int) * src->cap);
+    dest->size = src->size;
+}
+
+static inline void vec_int_copy(vec_int_t *dest, const vec_int_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_int_resize(dest, src->size);
+    memcpy(dest->data, src->data, sizeof(int) * src->size);
+    dest->size = src->size;
+}
+
+static inline void vec_int_push_back(vec_int_t *p, int value)
+{
+    if (p->size == p->cap) {
+        if (p->cap < 16)
+            vec_int_reserve(p, 16);
+        else
+            vec_int_reserve(p, 2 * p->cap);
+    }
+    p->data[p->size] = value;
+    p->size++;
+}
+
+static inline void vec_int_assign(vec_int_t *p, unsigned i, int value)
+{
+    assert((i >= 0) && (i < vec_int_size(p)));
+    p->data[i] = value;
+}
+
+static inline void vec_int_insert(vec_int_t *p, unsigned i, int value)
+{
+    assert((i >= 0) && (i < vec_int_size(p)));
+    vec_int_push_back(p, 0);
+    memmove(p->data + i + 1, p->data + i, (p->size - i - 2) * sizeof(int));
+    p->data[i] = value;
+}
+
+static inline void vec_int_drop(vec_int_t *p, unsigned i)
+{
+    assert((i >= 0) && (i < vec_int_size(p)));
+    memmove(p->data + i, p->data + i + 1, (p->size - i - 1) * sizeof(int));
+    p->size -= 1;
+}
+
+static inline void vec_int_clear(vec_int_t *p)
+{
+    p->size = 0;
+}
+
+static inline int vec_int_asc_compare(const void *p1, const void *p2)
+{
+    const int *pp1 = (const int *) p1;
+    const int *pp2 = (const int *) p2;
+
+    if (*pp1 < *pp2)
+        return -1;
+    if (*pp1 > *pp2)
+        return 1;
+    return 0;
+}
+
+static inline int vec_int_desc_compare(const void* p1, const void* p2)
+{
+    const int *pp1 = (const int *) p1;
+    const int *pp2 = (const int *) p2;
+
+    if (*pp1 > *pp2)
+        return -1;
+    if (*pp1 < *pp2)
+        return 1;
+    return 0;
+}
+
+static inline void vec_int_sort(vec_int_t* p, int ascending)
+{
+    if (ascending)
+        qsort((void *) p->data, p->size, sizeof(int),
+              (int (*)(const void*, const void*)) vec_int_asc_compare);
+    else
+        qsort((void *) p->data, p->size, sizeof(int),
+              (int (*)(const void*, const void*)) vec_int_desc_compare);
+}
+
+static inline long vec_int_memory(vec_int_t *p)
+{
+    return p == NULL ? 0 : sizeof(int) * p->cap + sizeof(vec_int_t);
+}
+
+static inline void vec_int_print(vec_int_t *p)
+{
+    unsigned i;
+    assert(p != NULL);
+    fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
+    for (i = 0; i < p->size; i++)
+        fprintf(stdout, " %d", p->data[i]);
+    fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_int_h */
diff --git a/src/sat/satoko/utils/vec/vec_uint.h b/src/sat/satoko/utils/vec/vec_uint.h
new file mode 100755
index 00000000..e6719ca3
--- /dev/null
+++ b/src/sat/satoko/utils/vec/vec_uint.h
@@ -0,0 +1,268 @@
+//===--- vec_uint.h ---------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__vec__vec_uint_h
+#define satoko__utils__vec__vec_uint_h
+
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+#include "../mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef struct vec_uint_t_ vec_uint_t;
+struct vec_uint_t_ {
+    unsigned cap;
+    unsigned size;
+    unsigned* data;
+};
+
+//===------------------------------------------------------------------------===
+// Vector Macros
+//===------------------------------------------------------------------------===
+#define vec_uint_foreach(vec, entry, i) \
+    for (i = 0; (i < vec_uint_size(vec)) && (((entry) = vec_uint_at(vec, i)), 1); i++)
+
+#define vec_uint_foreach_start(vec, entry, i, start) \
+    for (i = start; (i < vec_uint_size(vec)) && (((entry) = vec_uint_at(vec, i)), 1); i++)
+
+#define vec_uint_foreach_stop(vec, entry, i, stop) \
+    for (i = 0; (i < stop) && (((entry) = vec_uint_at(vec, i)), 1); i++)
+
+//===------------------------------------------------------------------------===
+// Vector API
+//===------------------------------------------------------------------------===
+static inline vec_uint_t * vec_uint_alloc(unsigned cap)
+{
+    vec_uint_t *p = satoko_alloc(vec_uint_t, 1);
+
+    if (cap > 0 && cap < 16)
+        cap = 16;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(unsigned, p->cap) : NULL;
+    return p;
+}
+
+static inline vec_uint_t * vec_uint_alloc_exact(unsigned cap)
+{
+    vec_uint_t *p = satoko_alloc(vec_uint_t, 1);
+
+    cap = 0;
+    p->size = 0;
+    p->cap = cap;
+    p->data = p->cap ? satoko_alloc(unsigned, p->cap ) : NULL;
+    return p;
+}
+
+static inline vec_uint_t * vec_uint_init(unsigned size, unsigned value)
+{
+    vec_uint_t *p = satoko_alloc(vec_uint_t, 1);
+
+    p->cap = size;
+    p->size = size;
+    p->data = p->cap ? satoko_alloc(unsigned, p->cap ) : NULL;
+    memset(p->data, value, sizeof(unsigned) * p->size);
+    return p;
+}
+
+static inline void vec_uint_free(vec_uint_t *p)
+{
+    if (p->data != NULL)
+        satoko_free(p->data);
+    satoko_free(p);
+}
+
+static inline unsigned vec_uint_size(vec_uint_t *p)
+{
+    return p->size;
+}
+
+static inline void vec_uint_resize(vec_uint_t *p, unsigned new_size)
+{
+    p->size = new_size;
+    if (p->cap >= new_size)
+        return;
+    p->data = satoko_realloc(unsigned, p->data, new_size);
+    assert(p->data != NULL);
+    p->cap = new_size;
+}
+
+static inline void vec_uint_shrink(vec_uint_t *p, unsigned new_size)
+{
+    assert(p->cap >= new_size);
+    p->size = new_size;
+}
+
+static inline void vec_uint_reserve(vec_uint_t *p, unsigned new_cap)
+{
+    if (p->cap >= new_cap)
+        return;
+    p->data = satoko_realloc(unsigned, p->data, new_cap);
+    assert(p->data != NULL);
+    p->cap = new_cap;
+}
+
+static inline unsigned vec_uint_capacity(vec_uint_t *p)
+{
+    return p->cap;
+}
+
+static inline int vec_uint_empty(vec_uint_t *p)
+{
+    return p->size ? 0 : 1;
+}
+
+static inline void vec_uint_erase(vec_uint_t *p)
+{
+    satoko_free(p->data);
+    p->size = 0;
+    p->cap = 0;
+}
+
+static inline unsigned vec_uint_at(vec_uint_t *p, unsigned idx)
+{
+    assert(idx >= 0 && idx < p->size);
+    return p->data[idx];
+}
+
+static inline unsigned * vec_uint_at_ptr(vec_uint_t *p, unsigned idx)
+{
+    assert(idx >= 0 && idx < p->size);
+    return p->data + idx;
+}
+
+static inline unsigned vec_uint_find(vec_uint_t *p, unsigned entry)
+{
+    unsigned i;
+    for (i = 0; i < p->size; i++)
+        if (p->data[i] == entry)
+            return 1;
+    return 0;
+}
+
+static inline unsigned * vec_uint_data(vec_uint_t *p)
+{
+    assert(p);
+    return p->data;
+}
+
+static inline void vec_uint_duplicate(vec_uint_t *dest, const vec_uint_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_uint_resize(dest, src->cap);
+    memcpy(dest->data, src->data, sizeof(unsigned) * src->cap);
+    dest->size = src->size;
+}
+
+static inline void vec_uint_copy(vec_uint_t *dest, const vec_uint_t *src)
+{
+    assert(dest != NULL && src != NULL);
+    vec_uint_resize(dest, src->size);
+    memcpy(dest->data, src->data, sizeof(unsigned) * src->size);
+    dest->size = src->size;
+}
+
+static inline void vec_uint_push_back(vec_uint_t *p, unsigned value)
+{
+    if (p->size == p->cap) {
+        if (p->cap < 16)
+            vec_uint_reserve(p, 16);
+        else
+            vec_uint_reserve(p, 2 * p->cap);
+    }
+    p->data[p->size] = value;
+    p->size++;
+}
+
+static inline unsigned vec_uint_pop_back(vec_uint_t *p)
+{
+    assert(p && p->size);
+    return p->data[--p->size];
+}
+
+static inline void vec_uint_assign(vec_uint_t *p, unsigned idx, unsigned value)
+{
+    assert((idx >= 0) && (idx < vec_uint_size(p)));
+    p->data[idx] = value;
+}
+
+static inline void vec_uint_insert(vec_uint_t *p, unsigned idx, unsigned value)
+{
+    assert((idx >= 0) && (idx < vec_uint_size(p)));
+    vec_uint_push_back(p, 0);
+    memmove(p->data + idx + 1, p->data + idx, (p->size - idx - 2) * sizeof(unsigned));
+    p->data[idx] = value;
+}
+
+static inline void vec_uint_drop(vec_uint_t *p, unsigned idx)
+{
+    assert((idx >= 0) && (idx < vec_uint_size(p)));
+    memmove(p->data + idx, p->data + idx + 1, (p->size - idx - 1) * sizeof(unsigned));
+    p->size -= 1;
+}
+
+static inline void vec_uint_clear(vec_uint_t *p)
+{
+    p->size = 0;
+}
+
+static inline int vec_uint_asc_compare(const void *p1, const void *p2)
+{
+    const unsigned *pp1 = (const unsigned *) p1;
+    const unsigned *pp2 = (const unsigned *) p2;
+
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 )
+        return 1;
+    return 0;
+}
+
+static inline int vec_uint_desc_compare(const void *p1, const void *p2)
+{
+    const unsigned *pp1 = (const unsigned *) p1;
+    const unsigned *pp2 = (const unsigned *) p2;
+
+    if ( *pp1 > *pp2 )
+        return -1;
+    if ( *pp1 < *pp2 )
+        return 1;
+    return 0;
+}
+
+static inline void vec_uint_sort(vec_uint_t *p, int ascending)
+{
+    if (ascending)
+        qsort((void *) p->data, p->size, sizeof(unsigned),
+              (int (*)(const void *, const void *)) vec_uint_asc_compare);
+    else
+        qsort((void*) p->data, p->size, sizeof(unsigned),
+              (int (*)(const void *, const void *)) vec_uint_desc_compare);
+}
+
+static inline long vec_uint_memory(vec_uint_t *p)
+{
+    return p == NULL ? 0 : sizeof(unsigned) * p->cap + sizeof(vec_uint_t);
+}
+
+static inline void vec_uint_print(vec_uint_t* p)
+{
+    unsigned i;
+    assert(p != NULL);
+    fprintf(stdout, "Vector has %u(%u) entries: {", p->size, p->cap);
+    for (i = 0; i < p->size; i++)
+        fprintf(stdout, " %u", p->data[i]);
+    fprintf(stdout, " }\n");
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__utils__vec__vec_uint_h */
diff --git a/src/sat/satoko/watch_list.h b/src/sat/satoko/watch_list.h
new file mode 100644
index 00000000..f492904a
--- /dev/null
+++ b/src/sat/satoko/watch_list.h
@@ -0,0 +1,152 @@
+//===--- watch_list.h -------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__watch_list_h
+#define satoko__watch_list_h
+
+#include "utils/mem.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+struct watcher {
+    unsigned cref;
+    unsigned blocker;
+};
+
+struct watch_list {
+    unsigned cap;
+    unsigned size;
+    struct watcher *watchers;
+};
+
+typedef struct vec_wl_t_ vec_wl_t;
+struct vec_wl_t_ {
+    unsigned cap;
+    unsigned size;
+    struct watch_list *watch_lists;
+};
+
+//===------------------------------------------------------------------------===
+// Watch list Macros
+//===------------------------------------------------------------------------===
+#define watch_list_foreach(vec, watch, lit) \
+    for (watch = watch_list_array(vec_wl_at(vec, lit)); \
+         watch < watch_list_array(vec_wl_at(vec, lit)) + watch_list_size(vec_wl_at(vec, lit)); \
+     watch++)
+
+//===------------------------------------------------------------------------===
+// Watch list API
+//===------------------------------------------------------------------------===
+static inline void watch_list_free(struct watch_list *wl)
+{
+    if (wl->watchers)
+        satoko_free(wl->watchers);
+}
+
+static inline unsigned watch_list_size(struct watch_list *wl)
+{
+    return wl->size;
+}
+
+static inline void watch_list_shrink(struct watch_list *wl, unsigned size)
+{
+    assert(size <= wl->size);
+    wl->size = size;
+}
+
+static inline void watch_list_push(struct watch_list *wl, struct watcher w)
+{
+    assert(wl);
+    if (wl->size == wl->cap) {
+        unsigned new_size = (wl->cap < 4) ? 4 : (wl->cap / 2) * 3;
+        struct watcher *watchers =
+            satoko_realloc(struct watcher, wl->watchers, new_size);
+        if (watchers == NULL) {
+            printf("Failed to realloc memory from %.1f MB to %.1f "
+                   "MB.\n",
+                   1.0 * wl->cap / (1 << 20),
+                   1.0 * new_size / (1 << 20));
+            fflush(stdout);
+            return;
+        }
+        wl->watchers = watchers;
+        wl->cap = new_size;
+    }
+    wl->watchers[wl->size++] = w;
+}
+
+static inline struct watcher *watch_list_array(struct watch_list *wl)
+{
+    return wl->watchers;
+}
+
+static inline void watch_list_remove(struct watch_list *wl, unsigned cref)
+{
+    struct watcher *watchers = watch_list_array(wl);
+    unsigned i;
+    for (i = 0; watchers[i].cref != cref; i++);
+    assert(i < watch_list_size(wl));
+    memmove((wl->watchers + i), (wl->watchers + i + 1),
+            (wl->size - i - 1) * sizeof(struct watcher));
+    wl->size -= 1;
+}
+
+static inline vec_wl_t *vec_wl_alloc(unsigned cap)
+{
+    vec_wl_t *vec_wl = satoko_alloc(vec_wl_t, 1);
+
+    if (cap == 0)
+        vec_wl->cap = 4;
+    else
+        vec_wl->cap = cap;
+    vec_wl->size = 0;
+    vec_wl->watch_lists = satoko_calloc(
+        struct watch_list, sizeof(struct watch_list) * vec_wl->cap);
+    return vec_wl;
+}
+
+static inline void vec_wl_free(vec_wl_t *vec_wl)
+{
+    for (unsigned i = 0; i < vec_wl->size; i++)
+        watch_list_free(vec_wl->watch_lists + i);
+    satoko_free(vec_wl->watch_lists);
+    satoko_free(vec_wl);
+}
+
+static inline void vec_wl_push(vec_wl_t *vec_wl)
+{
+    if (vec_wl->size == vec_wl->cap) {
+        unsigned new_size =
+            (vec_wl->cap < 4) ? vec_wl->cap * 2 : (vec_wl->cap / 2) * 3;
+
+        vec_wl->watch_lists = satoko_realloc(
+            struct watch_list, vec_wl->watch_lists, new_size);
+        memset(vec_wl->watch_lists + vec_wl->cap, 0,
+               sizeof(struct watch_list) * (new_size - vec_wl->cap));
+        if (vec_wl->watch_lists == NULL) {
+            printf("failed to realloc memory from %.1f mb to %.1f "
+                   "mb.\n",
+                   1.0 * vec_wl->cap / (1 << 20),
+                   1.0 * new_size / (1 << 20));
+            fflush(stdout);
+        }
+        vec_wl->cap = new_size;
+    }
+    vec_wl->size++;
+}
+
+static inline struct watch_list *vec_wl_at(vec_wl_t *vec_wl, unsigned idx)
+{
+    assert(idx < vec_wl->cap);
+    assert(idx < vec_wl->size);
+    return vec_wl->watch_lists + idx;
+}
+
+ABC_NAMESPACE_HEADER_END
+#endif /* satoko__watch_list_h */