Improvement to the SAT solver (skipping binary clauses).

3 files changed, 57 insertions, 5 deletions

diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index d4726b81..3904f8b0 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -306,6 +306,15 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
     assert(end - begin > 1);
     assert(learnt >= 0 && learnt < 2);
     size           = end - begin;
+
+    // do not allocate memory for the two-literal problem clause
+    if ( size == 2 && !learnt )
+    {
+        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(clause_from_lit(begin[1])));
+        vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(clause_from_lit(begin[0])));
+        return NULL;
+    }
+
 //    c              = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
 #ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
     c = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
@@ -336,6 +345,8 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
     vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
     vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
 
+//    if ( learnt )
+//    printf( "%d ", size );
     return c;
 }
 
@@ -1212,6 +1223,7 @@ void sat_solver_delete(sat_solver* s)
 
 int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 {
+    clause * c;
     lit *i,*j;
     int maxvar;
     lbool* values;
@@ -1271,7 +1283,9 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
         return enqueue(s,*begin,(clause*)0);
 
     // create new clause
-    vecp_push(&s->clauses,clause_new(s,begin,j,0));
+    c = clause_new(s,begin,j,0);
+    if ( c )
+        vecp_push(&s->clauses,c);
 
 
     s->stats.clauses++;
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index a67e829a..f500b46b 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -36,7 +36,7 @@ ABC_NAMESPACE_HEADER_START
 
 //=================================================================================================
 // Simple types:
-
+/*
 #ifndef __cplusplus
 #ifndef false
 #  define false 0
@@ -64,7 +64,7 @@ static inline int  lit_sign (lit l)        { return l & 1; }
 static inline int  lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
 static inline lit  lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
 static inline int  lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }
-
+*/
 
 //=================================================================================================
 // Public interface:
@@ -84,14 +84,14 @@ extern int         sat_solver_nclauses(sat_solver* s);
 extern int         sat_solver_nconflicts(sat_solver* s);
 
 extern void        sat_solver_setnvars(sat_solver* s,int n);
-
+/*
 struct stats_t
 {
     ABC_INT64_T   starts, decisions, propagations, inspects, conflicts;
     ABC_INT64_T   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
 };
 typedef struct stats_t stats_t;
-
+*/
 extern void        Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
 extern void        Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
 extern int *       Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars );
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h
index 6e604d36..4eedbdd0 100644
--- a/src/sat/bsat/satVec.h
+++ b/src/sat/bsat/satVec.h
@@ -86,6 +86,44 @@ static inline void   vecp_push   (vecp* v, void* e)
 
 
 
+//=================================================================================================
+// Simple types:
+
+#ifndef __cplusplus
+#ifndef false
+#  define false 0
+#endif
+#ifndef true
+#  define true 1
+#endif
+#endif
+
+typedef int                lit;
+typedef char               lbool;
+
+static const int   var_Undef = -1;
+static const lit   lit_Undef = -2;
+
+static const lbool l_Undef   =  0;
+static const lbool l_True    =  1;
+static const lbool l_False   = -1;
+
+static inline lit  toLit    (int v)        { return v + v; }
+static inline lit  toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit  lit_neg  (lit l)        { return l ^ 1; }
+static inline int  lit_var  (lit l)        { return l >> 1; }
+static inline int  lit_sign (lit l)        { return l & 1; }
+static inline int  lit_print(lit l)        { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }
+static inline lit  lit_read (int s)        { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }
+static inline int  lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n;                  }
+
+struct stats_t
+{
+    ABC_INT64_T   starts, decisions, propagations, inspects, conflicts;
+    ABC_INT64_T   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+};
+typedef struct stats_t stats_t;
+
 
 ABC_NAMESPACE_HEADER_END