summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat/satSolver.c')
-rw-r--r--src/sat/bsat/satSolver.c202
1 files changed, 25 insertions, 177 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 19ff6f8b..512c5751 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -27,7 +27,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "satSolver.h"
//#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT
-#define WATCHFLAG 1
//=================================================================================================
// Debug:
@@ -91,11 +90,9 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[
//=================================================================================================
// Encode literals in clause pointers:
-static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); }
+static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); }
static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); }
-static clause* clause_from_lit2(lit l) { return (clause*)(unsigned long)l; }
-static lit clause_read_lit2(clause* c) { return (lit)(unsigned long)c; }
//=================================================================================================
// Simple helpers:
@@ -111,15 +108,6 @@ static inline void vecp_remove(vecp* v, void* e)
for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
vecp_resize(v,vecp_size(v)-1);
}
-static inline void vecp_remove2(vecp* v, void* e)
-{
- void** ws = vecp_begin(v);
- int j = 0;
- for (; ws[j] != e ; j++);
- assert(j < vecp_size(v));
- for (; j < vecp_size(v)-2; j++) ws[j] = ws[j+2];
- vecp_resize(v,vecp_size(v)-2);
-}
//=================================================================================================
// Variable order functions:
@@ -316,26 +304,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*)c);
//vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
- if ( WATCHFLAG )
- {
- if ( size == 2 )
- {
- 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]));
- }
- else
- {
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit2(begin[1]));
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
- vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit2(begin[0]));
- }
- }
- else
- {
- 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])));
- }
+ 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])));
return c;
}
@@ -351,24 +321,8 @@ static void clause_remove(sat_solver* s, clause* c)
//vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
assert(lits[0] < s->size*2);
- if ( WATCHFLAG )
- {
- if ( clause_size(c) == 2 )
- {
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)clause_from_lit(lits[1]));
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)clause_from_lit(lits[0]));
- }
- else
- {
- vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
- vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
- }
- }
- else
- {
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
- vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
- }
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+ vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
if (clause_learnt(c)){
s->stats.learnts--;
@@ -749,31 +703,6 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
}
-void sat_solver_check(sat_solver* s)
-{
- int j, k;
- lit Lit, First, *lits;
- vecp* ws;
- clause **begin, **end, **i;
- for ( j = 0; j < s->size; j++ )
- for ( k = 0; k < 2; k++ )
- {
- Lit = toLitCond( j, k );
- ws = sat_solver_read_wlist(s,Lit);
- begin = (clause**)vecp_begin(ws);
- end = begin + vecp_size(ws);
- for (i = begin; i < end; i++)
- {
- if (clause_is_lit(*i))
- continue;
- lits = clause_begin(*i);
- First = clause_read_lit2(*(i+1));
- assert( First == lits[0] || First == lits[1] );
- i++;
- }
- }
-}
-
clause* sat_solver_propagate(sat_solver* s)
{
lbool* values = s->assigns;
@@ -787,19 +716,15 @@ clause* sat_solver_propagate(sat_solver* s)
clause **begin = (clause**)vecp_begin(ws);
clause **end = begin + vecp_size(ws);
clause **i, **j;
-// sat_solver_check(s);
s->stats.propagations++;
s->simpdb_props--;
-
+
//printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
- for (i = j = begin; i < end; i++)
- {
- if (clause_is_lit(*i))
- {
+ for (i = j = begin; i < end; ){
+ if (clause_is_lit(*i)){
*j++ = *i;
- if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p)))
- {
+ if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
confl = s->binary;
(clause_begin(confl))[1] = lit_neg(p);
(clause_begin(confl))[0] = clause_read_lit(*i++);
@@ -808,27 +733,13 @@ clause* sat_solver_propagate(sat_solver* s)
while (i < end)
*j++ = *i++;
}
- }
- else
- {
- lit false_lit, first;
+ }else{
+ lit false_lit;
lbool sig;
- if ( WATCHFLAG )
- {
- first = clause_read_lit2(*(i+1));
- sig = !lit_sign(first); sig += sig - 1;
- if (values[lit_var(first)] == sig)
- {
- *j++ = *i++;
- *j++ = *i;
- continue;
- }
- }
-
lits = clause_begin(*i);
- // Make sure the false literal is in data[1]:
+ // Make sure the false literal is data[1]:
false_lit = lit_neg(p);
if (lits[0] == false_lit){
lits[0] = lits[1];
@@ -837,95 +748,35 @@ clause* sat_solver_propagate(sat_solver* s)
assert(lits[1] == false_lit);
//printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
- if ( WATCHFLAG )
- {
-/*
- // If 0th watch is true, then clause is already satisfied.
- sig = !lit_sign(lits[0]); sig += sig - 1;
- if (values[lit_var(lits[0])] == sig)
- {
- *j++ = *i++;
- *j++ = *i;
- continue;
- }
- else
-*/
- {
+ // If 0th watch is true, then clause is already satisfied.
+ sig = !lit_sign(lits[0]); sig += sig - 1;
+ if (values[lit_var(lits[0])] == sig){
+ *j++ = *i;
+ }else{
// Look for new watch:
lit* stop = lits + clause_size(*i);
lit* k;
-// assert( lits[0] == first );
- for (k = lits + 2; k < stop; k++)
- {
+ for (k = lits + 2; k < stop; k++){
lbool sig = lit_sign(*k); sig += sig - 1;
- if (values[lit_var(*k)] != sig)
- {
+ if (values[lit_var(*k)] != sig){
lits[1] = *k;
*k = false_lit;
-// vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
- vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i++);
- vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),clause_from_lit2(lits[0]));
- break;
- }
+ vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+ goto next; }
}
- if ( k < stop )
- continue;
*j++ = *i;
// Clause is unit under assignment:
- if (!enqueue(s,lits[0], *i))
- {
+ if (!enqueue(s,lits[0], *i)){
confl = *i++;
- *j++ = clause_from_lit2(lits[0]); i++; //
// Copy the remaining watches:
while (i < end)
*j++ = *i++;
}
- else
- {
- *j++ = clause_from_lit2(lits[0]); i++; //
- }
- }
- }
- else
- {
- // If 0th watch is true, then clause is already satisfied.
- sig = !lit_sign(lits[0]); sig += sig - 1;
- if (values[lit_var(lits[0])] == sig)
- {
- *j++ = *i;
- }
- else
- {
- // Look for new watch:
- lit* stop = lits + clause_size(*i);
- lit* k;
- for (k = lits + 2; k < stop; k++)
- {
- lbool sig = lit_sign(*k); sig += sig - 1;
- if (values[lit_var(*k)] != sig)
- {
- lits[1] = *k;
- *k = false_lit;
- vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
- break;
- }
- }
- if ( k < stop )
- continue;
-
- *j++ = *i;
- // Clause is unit under assignment:
- if (!enqueue(s,lits[0], *i))
- {
- confl = *i++;
- // Copy the remaining watches:
- while (i < end)
- *j++ = *i++;
- }
- }
}
}
+ next:
+ i++;
}
s->stats.inspects += j - (clause**)vecp_begin(ws);
@@ -944,7 +795,7 @@ void sat_solver_reducedb(sat_solver* s)
double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
clause** learnts = (clause**)vecp_begin(&s->learnts);
clause** reasons = s->reasons;
-//printf( "Trying to reduce DB\n" );
+
sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
@@ -1037,10 +888,8 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
}
if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
- {
// Simplify the set of problem clauses:
sat_solver_simplify(s);
- }
if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
// Reduce the set of learnt clauses:
@@ -1271,7 +1120,6 @@ bool sat_solver_simplify(sat_solver* s)
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
return true;
-//printf( "Trying to simplify\n" );
reasons = s->reasons;
for (type = 0; type < 2; type++){
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 14:10:42 +0000