New fixed point data type.

Expose all options to command line.
Expose search statistics to users.

src/base/abci/abc.c

@@ -23326,7 +23326,11 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     satoko_default_opts(&opts);
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Chv" ) ) != EOF )
+#ifdef SATOKO_ACT_VAR_FIXED
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CPDEFGHIJKLMNOQRSTUhv" ) ) != EOF )
+#else
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CPDEFGHIJKLMNOQRShv" ) ) != EOF )
+#endif
     {
         switch ( c )
         {
@@ -23341,6 +23345,184 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( opts.conf_limit < 0 )
                 goto usage;
             break;
+         case 'P':
+                if ( globalUtilOptind >= argc )
+                {
+                    Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                opts.prop_limit = atoi(argv[globalUtilOptind]);
+                globalUtilOptind++;
+                if ( opts.prop_limit < 0 )
+                    goto usage;
+                break;
+         case 'D':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-D\" should be followed by an float.\n" );
+                   goto usage;
+               }
+               opts.f_rst = atof(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               if ( opts.f_rst < 0 )
+                   goto usage;
+               break;
+         case 'E':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-E\" should be followed by an float.\n" );
+                   goto usage;
+               }
+               opts.b_rst = atof(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               if ( opts.b_rst < 0 )
+                   goto usage;
+               break;
+         case 'F':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.fst_block_rst = (unsigned)atoi(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               break;
+         case 'G':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.sz_lbd_bqueue = (unsigned)atoi(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               break;
+         case 'H':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.sz_trail_bqueue = (unsigned)atoi(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               break;
+         case 'I':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.n_conf_fst_reduce = (unsigned)atoi(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               break;
+         case 'J':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.inc_reduce = (unsigned)atoi(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               break;
+         case 'K':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.inc_special_reduce = (unsigned)atoi(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               break;
+         case 'L':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.lbd_freeze_clause = (unsigned)atoi(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               break;
+         case 'M':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.learnt_ratio = atof(argv[globalUtilOptind]) / 100;
+               globalUtilOptind++;
+               if ( opts.learnt_ratio < 0 )
+                   goto usage;
+               break;
+         case 'N':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.garbage_max_ratio = atof(argv[globalUtilOptind]) / 100;
+               globalUtilOptind++;
+               if ( opts.garbage_max_ratio < 0 )
+                   goto usage;
+               break;
+         case 'O':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.clause_max_sz_bin_resol = (unsigned)atoi(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               break;
+         case 'Q':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+                   goto usage;
+               }
+               opts.clause_min_lbd_bin_resol = (unsigned)atoi(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               break;
+         case 'R':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-R\" should be followed by an float.\n" );
+                   goto usage;
+               }
+               opts.clause_decay = atof(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               if ( opts.clause_decay < 0 )
+                   goto usage;
+               break;
+         case 'S':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-S\" should be followed by an float.\n" );
+                   goto usage;
+               }
+               opts.var_decay = atof(argv[globalUtilOptind]);
+               globalUtilOptind++;
+               if ( opts.var_decay < 0 )
+                   goto usage;
+               break;
+#ifdef SATOKO_ACT_VAR_FIXED
+         case 'T':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-T\" should be followed by an float.\n" );
+                   goto usage;
+               }
+               opts.var_act_limit = (unsigned)strtol(argv[globalUtilOptind], NULL, 16);
+               globalUtilOptind++;
+               break;
+         case 'U':
+               if ( globalUtilOptind >= argc )
+               {
+                   Abc_Print( -1, "Command line switch \"-U\" should be followed by an float.\n" );
+                   goto usage;
+               }
+               opts.var_act_rescale = (unsigned)strtol(argv[globalUtilOptind], NULL, 16);
+               globalUtilOptind++;
+               break;
+#endif
         case 'h':
             goto usage;
         case 'v':
@@ -23379,9 +23561,37 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
 usage:
-    Abc_Print( -2, "usage: satoko [-CILDE num] [-hv]<file>.cnf\n" );
+#ifdef SATOKO_ACT_VAR_FIXED
+    Abc_Print( -2, "usage: satoko [-CPDEFGHIJKLMNOQRSTU num] [-hv]<file>.cnf\n" );
+#else
+    Abc_Print( -2, "usage: satoko [-CPDEFGHIJKLMNOQRS num] [-hv]<file>.cnf\n" );
+#endif
     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-P num : limit on the number of propagations [default = %d]\n", opts.conf_limit );
+    Abc_Print( -2, "\n\tConstants used for restart heuristic:\n");
+    Abc_Print( -2, "\t-D num : Constant value used by restart heuristics in forcing restarts [default = %f]\n", opts.f_rst );
+    Abc_Print( -2, "\t-E num : Constant value used by restart heuristics in  blocking restarts [default = %f]\n", opts.b_rst );
+    Abc_Print( -2, "\t-F num : Lower bound n.of conflicts for start blocking restarts [default = %d]\n", opts.fst_block_rst );
+    Abc_Print( -2, "\t-G num : Size of the moving avarege queue for LBD (force restart) [default = %d]\n", opts.sz_lbd_bqueue );
+    Abc_Print( -2, "\t-H num : Size of the moving avarege queue for Trail size (block restart) [default = %d]\n", opts.sz_trail_bqueue );
+    Abc_Print( -2, "\n\tConstants used for clause database reduction heuristic:\n");
+    Abc_Print( -2, "\t-I num : N.of conflicts before first clause databese reduction [default = %d]\n", opts.n_conf_fst_reduce );
+    Abc_Print( -2, "\t-J num : Increment to reduce [default = %d]\n", opts.inc_reduce );
+    Abc_Print( -2, "\t-K num : Special increment to reduce [default = %d]\n", opts.inc_special_reduce );
+    Abc_Print( -2, "\t-L num : Protecs clauses from deletion for one turn if its LBD is lower [default = %d]\n", opts.lbd_freeze_clause );
+    Abc_Print( -2, "\t-M num : Percentage of learned clauses to remove [default = %d]\n", ( int )( 100 * opts.learnt_ratio ) );
+    Abc_Print( -2, "\t-N num : Max percentage of garbage in clause database [default = %d]\n", ( int )( 100 * opts.garbage_max_ratio ) );
+    Abc_Print( -2, "\n\tConstants used for binary resolution (clause minimization):\n");
+    Abc_Print( -2, "\t-O num : Max clause size for binary resolution [default = %d]\n", opts.clause_max_sz_bin_resol );
+    Abc_Print( -2, "\t-Q num : Min clause LBD for binary resolution [default = %d]\n", opts.clause_min_lbd_bin_resol );
+    Abc_Print( -2, "\n\tConstants used for branching (VSIDS heuristic):\n");
+    Abc_Print( -2, "\t-R num : Clause activity decay factor (when using float clause activity) [default = %f]\n", opts.clause_decay );
+    Abc_Print( -2, "\t-S num : Varibale activity decay factor [default = %f]\n", opts.var_decay );
+#ifdef SATOKO_ACT_VAR_FIXED
+    Abc_Print( -2, "\t-T num : Variable activity limit valeu [default = 0x%08X]\n", opts.var_act_limit );
+    Abc_Print( -2, "\t-U num : Variable activity re-scale factor [default = 0x%08X]\n", opts.var_act_rescale );
+#endif
+    Abc_Print( -2, "\n\t-v     : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }

src/sat/satoko/act_var.h

@@ -16,7 +16,7 @@
 #include "misc/util/abc_global.h"
 ABC_NAMESPACE_HEADER_START
 
-#if defined SATOKO_ACT_VAR_DBLE || defined SATOKO_ACT_VAR_FLOAT
+#if defined SATOKO_ACT_VAR_DBLE
 /** Re-scale the activity value for all variables.
  */
 static inline void var_act_rescale(solver_t *s)
@@ -25,8 +25,8 @@ static inline void var_act_rescale(solver_t *s)
     act_t *activity = vec_act_data(s->activity);
 
     for (i = 0; i < vec_act_size(s->activity); i++)
-        activity[i] *= VAR_ACT_RESCALE;
-    s->var_act_inc *= VAR_ACT_RESCALE;
+        activity[i] *= s->opts.var_act_rescale;
+    s->var_act_inc *= s->opts.var_act_rescale;
 }
 
 /** Increment the activity value of one variable ('var')
@@ -36,7 +36,7 @@ static inline void var_act_bump(solver_t *s, unsigned var)
     act_t *activity = vec_act_data(s->activity);
 
     activity[var] += s->var_act_inc;
-    if (activity[var] > VAR_ACT_LIMIT)
+    if (activity[var] > s->opts.var_act_limit)
         var_act_rescale(s);
     if (heap_in_heap(s->var_order, var))
         heap_decrease(s->var_order, var);
@@ -49,6 +49,34 @@ static inline void var_act_decay(solver_t *s)
     s->var_act_inc *= (1 / s->opts.var_decay);
 }
 
+#elif defined(SATOKO_ACT_VAR_FIXED)
+
+static inline void var_act_rescale(solver_t *s)
+{
+    unsigned i;
+    act_t *activity = (act_t *)vec_act_data(s->activity);
+
+    for (i = 0; i < vec_act_size(s->activity); i++)
+        activity[i] = fixed_mult(activity[i], VAR_ACT_RESCALE);
+    s->var_act_inc = fixed_mult(s->var_act_inc, VAR_ACT_RESCALE);
+}
+
+static inline void var_act_bump(solver_t *s, unsigned var)
+{
+    act_t *activity = (act_t *)vec_act_data(s->activity);
+
+    activity[var] = fixed_add(activity[var], s->var_act_inc);
+    if (activity[var] > VAR_ACT_LIMIT)
+        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 = fixed_mult(s->var_act_inc, dble2fixed(1 / s->opts.var_decay));
+}
+
 #else
 
 static inline void var_act_rescale(solver_t *s)
@@ -77,7 +105,7 @@ static inline void var_act_decay(solver_t *s)
     s->var_act_inc += (s->var_act_inc >> 4);
 }
 
-#endif /* SATOKO_ACT_VAR_DBLE || SATOKO_ACT_VAR_FLOAT */
+#endif /* SATOKO_ACT_VAR_DBLE || SATOKO_ACT_VAR_FIXED */
 
 ABC_NAMESPACE_HEADER_END
 #endif /* satoko__act_var_h */

src/sat/satoko/satoko.h

@@ -32,7 +32,7 @@ typedef struct satoko_opts satoko_opts_t;
 struct satoko_opts {
     /* Limits */
     long conf_limit;  /* Limit on the n.of conflicts */
-    long prop_limit;  /* Limit on the n.of implications */
+    long prop_limit;  /* Limit on the n.of propagations */
 
     /* Constants used for restart heuristic */
     double f_rst;          /* Used to force a restart */
@@ -42,7 +42,7 @@ struct satoko_opts {
     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 n_conf_fst_reduce;  /* N.of conflicts before first clause databese reduction */
     unsigned inc_reduce;         /* Increment to reduce */
     unsigned inc_special_reduce; /* Special increment to reduce */
     unsigned lbd_freeze_clause;
@@ -50,7 +50,9 @@ struct satoko_opts {
 
     /* VSIDS heuristic */
     float clause_decay;
-    act_t var_decay;
+    double var_decay;
+    act_t var_act_limit;
+    act_t var_act_rescale;
 
     /* Binary resolution */
     unsigned clause_max_sz_bin_resol;
@@ -59,6 +61,21 @@ struct satoko_opts {
     char verbose;
 };
 
+typedef struct satoko_stats satoko_stats_t;
+struct satoko_stats {
+    unsigned n_starts;
+    unsigned n_reduce_db;
+
+    long n_decisions;
+    long n_propagations;
+    long n_inspects;
+    long n_conflicts;
+
+    long n_original_lits;
+    long n_learnt_lits;
+};
+
+
 //===------------------------------------------------------------------------===
 extern satoko_t *satoko_create(void);
 extern void satoko_destroy(satoko_t *);
@@ -83,5 +100,7 @@ extern int  satoko_solve(satoko_t *);
  */
 extern int satoko_final_conflict(satoko_t *, unsigned *);
 
+extern satoko_stats_t satoko_stats(satoko_t *);
+
 ABC_NAMESPACE_HEADER_END
 #endif /* satoko__satoko_h */

src/sat/satoko/solver.h

@@ -38,19 +38,6 @@ enum {
 
 #define UNDEF 0xFFFFFFFF
 
-struct satoko_stats {
-    unsigned n_starts;
-    unsigned n_reduce_db;
-
-    long n_decisions;
-    long n_propagations;
-    long n_inspects;
-    long n_conflicts;
-
-    long n_original_lits;
-    long n_learnt_lits;
-};
-
 typedef struct solver_t_ solver_t;
 struct solver_t_ {
     /* User data */

src/sat/satoko/solver_api.c

@@ -12,8 +12,8 @@
 #include <math.h>
 
 #include "act_var.h"
-#include "utils/misc.h"
 #include "solver.h"
+#include "utils/misc.h"
 
 #include "misc/util/abc_global.h"
 ABC_NAMESPACE_IMPL_START
@@ -167,7 +167,9 @@ void satoko_default_opts(satoko_opts_t *opts)
     opts->lbd_freeze_clause = 30;
     opts->learnt_ratio = 0.5;
     /* VSIDS heuristic */
-    opts->var_decay = (act_t) 0.95;
+    opts->var_act_limit = VAR_ACT_LIMIT;
+    opts->var_act_rescale = VAR_ACT_RESCALE;
+    opts->var_decay = VAR_ACT_DECAY;
     opts->clause_decay = (clause_act_t) 0.995;
     /* Binary resolution */
     opts->clause_max_sz_bin_resol = 30;
@@ -308,4 +310,9 @@ int satoko_final_conflict(solver_t *s, unsigned *out)
 
 }
 
+satoko_stats_t satoko_stats(satoko_t *s)
+{
+    return s->stats;
+}
+
 ABC_NAMESPACE_IMPL_END

src/sat/satoko/types.h

@@ -9,21 +9,22 @@
 #ifndef satoko__types_h
 #define satoko__types_h
 
+#include "utils/fixed.h"
 #include "utils/vec/vec_dble.h"
-#include "utils/vec/vec_flt.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_VAR_FLOAT
+#define SATOKO_ACT_VAR_DBLE
+// #define SATOKO_ACT_VAR_FIXED
 // #define SATOKO_ACT_CLAUSE_FLOAT
 
 #ifdef SATOKO_ACT_VAR_DBLE
     #define VAR_ACT_INIT_INC 1.0
     #define VAR_ACT_LIMIT (double)1e100
     #define VAR_ACT_RESCALE (double)1e-100
+    #define VAR_ACT_DECAY (double)0.95
     typedef double act_t;
     typedef vec_dble_t vec_act_t ;
     #define vec_act_alloc(size) vec_dble_alloc(size)
@@ -32,18 +33,19 @@ ABC_NAMESPACE_HEADER_START
     #define vec_act_data(vec) vec_dble_data(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)
-#elif defined(SATOKO_ACT_VAR_FLOAT)
-    #define VAR_ACT_INIT_INC 1.0
-    #define VAR_ACT_LIMIT (float)1e20
-    #define VAR_ACT_RESCALE (float)1e-20
-    typedef float act_t;
-    typedef vec_flt_t vec_act_t ;
-    #define vec_act_alloc(size) vec_flt_alloc(size)
-    #define vec_act_free(vec) vec_flt_free(vec)
-    #define vec_act_size(vec) vec_flt_size(vec)
-    #define vec_act_data(vec) vec_flt_data(vec)
-    #define vec_act_at(vec, idx) vec_flt_at(vec, idx)
-    #define vec_act_push_back(vec, value) vec_flt_push_back(vec, value)
+#elif defined(SATOKO_ACT_VAR_FIXED)
+    #define VAR_ACT_INIT_INC FIXED_ONE
+    #define VAR_ACT_LIMIT  (fixed_t)0xDFFFFFFF
+    #define VAR_ACT_RESCALE (fixed_t)0x00000012
+    #define VAR_ACT_DECAY (double)0.96
+    typedef fixed_t 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_data(vec) vec_uint_data(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)
 #else
     #define VAR_ACT_INIT_INC (1 << 5)
     typedef unsigned act_t;

src/sat/satoko/utils/fixed.h

+//===--- sort.h -------------------------------------------------------------===
+//
+//                     satoko: Satisfiability solver
+//
+// This file is distributed under the BSD 2-Clause License.
+// See LICENSE for details.
+//
+//===------------------------------------------------------------------------===
+#ifndef satoko__utils__fixed_h
+#define satoko__utils__fixed_h
+
+#include "misc.h"
+
+#include "misc/util/abc_global.h"
+ABC_NAMESPACE_HEADER_START
+
+typedef unsigned fixed_t;
+static const int FIXED_W_BITS = 16; /* */
+static const int FIXED_F_BITS = 32 - FIXED_W_BITS;
+static const int FIXED_F_MASK = (1 << FIXED_F_BITS) - 1;
+static const fixed_t FIXED_MAX = 0xFFFFFFFF;
+static const fixed_t FIXED_MIN = 0x00000000;
+static const fixed_t FIXED_ONE = (1 << FIXED_F_BITS);
+
+/* Conversion functions */
+static inline fixed_t uint2fixed(unsigned a) { return a * FIXED_ONE; }
+static inline unsigned fixed2uint(fixed_t a)
+{
+    return (a + (FIXED_ONE >> 1)) / FIXED_ONE;
+}
+
+static inline float fixed2float(fixed_t a) { return (float)a / FIXED_ONE; }
+static inline fixed_t float2fixed(float a)
+{
+    float temp = a * FIXED_ONE;
+    temp += (temp >= 0) ? 0.5f : -0.5f;
+    return (fixed_t)temp;
+}
+
+static inline double fixed2dble(fixed_t a) { return (double)a / FIXED_ONE; }
+static inline fixed_t dble2fixed(double a)
+{
+    double temp = a * FIXED_ONE;
+    temp += (temp >= 0) ? 0.5f : -0.5f;
+    return (fixed_t)temp;
+}
+
+static inline fixed_t fixed_add(fixed_t a, fixed_t b) { return (a + b); }
+static inline fixed_t fixed_mult(fixed_t a, fixed_t b)
+{
+    unsigned hi_a = (a >> FIXED_F_BITS), lo_a = (a & FIXED_F_MASK);
+    unsigned hi_b = (b >> FIXED_F_BITS), lo_b = (b & FIXED_F_MASK);
+    unsigned lo_ab = lo_a * lo_b;
+    unsigned ab_ab = (hi_a * lo_b) + (lo_a * hi_b);
+    unsigned hi_ret = (hi_a * hi_b) + (ab_ab >> FIXED_F_BITS);
+    unsigned lo_ret = lo_ab + (ab_ab << FIXED_W_BITS);
+
+    /* Carry */
+    if (lo_ret < lo_ab)
+        hi_ret++;
+
+    return (hi_ret << FIXED_F_BITS) | (lo_ret >> FIXED_W_BITS);
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif /* satoko__utils__fixed_h */