diff options
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver3.c | 2299 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver3.h | 622 |
2 files changed, 2921 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver3.c b/src/sat/bsat/satSolver3.c new file mode 100644 index 00000000..b61ce96c --- /dev/null +++ b/src/sat/bsat/satSolver3.c @@ -0,0 +1,2299 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2005, Niklas Sorensson +http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko + +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <math.h> + +#include "satSolver3.h" + +ABC_NAMESPACE_IMPL_START + +#define SAT_USE_ANALYZE_FINAL + +//================================================================================================= +// Debug: + +//#define VERBOSEDEBUG + +// For derivation output (verbosity level 2) +#define L_IND "%-*d" +#define L_ind sat_solver3_dl(s)*2+2,sat_solver3_dl(s) +#define L_LIT "%sx%d" +#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p)) + +// Just like 'assert()' but expression will be evaluated in the release version as well. +static inline void check(int expr) { assert(expr); } + +static void printlits(lit* begin, lit* end) +{ + int i; + for (i = 0; i < end - begin; i++) + printf(L_LIT" ",L_lit(begin[i])); +} + +//================================================================================================= +// Random numbers: + + +// Returns a random float 0 <= x < 1. Seed must never be 0. +static inline double drand(double* seed) { + int q; + *seed *= 1389796; + q = (int)(*seed / 2147483647); + *seed -= (double)q * 2147483647; + return *seed / 2147483647; } + + +// Returns a random integer 0 <= x < size. Seed must never be 0. +static inline int irand(double* seed, int size) { + return (int)(drand(seed) * size); } + + +//================================================================================================= +// Variable datatype + minor functions: + +static const int var0 = 1; +static const int var1 = 0; +static const int varX = 3; + +struct varinfo_t +{ + unsigned val : 2; // variable value + unsigned pol : 1; // last polarity + unsigned tag : 1; // conflict analysis tag + unsigned lev : 28; // variable level +}; + +static inline int var_level (sat_solver3* s, int v) { return s->levels[v]; } +static inline int var_value (sat_solver3* s, int v) { return s->assigns[v]; } +static inline int var_polar (sat_solver3* s, int v) { return s->polarity[v]; } + +static inline void var_set_level (sat_solver3* s, int v, int lev) { s->levels[v] = lev; } +static inline void var_set_value (sat_solver3* s, int v, int val) { s->assigns[v] = val; } +static inline void var_set_polar (sat_solver3* s, int v, int pol) { s->polarity[v] = pol; } + +// variable tags +static inline int var_tag (sat_solver3* s, int v) { return s->tags[v]; } +static inline void var_set_tag (sat_solver3* s, int v, int tag) { + assert( tag > 0 && tag < 16 ); + if ( s->tags[v] == 0 ) + veci_push( &s->tagged, v ); + s->tags[v] = tag; +} +static inline void var_add_tag (sat_solver3* s, int v, int tag) { + assert( tag > 0 && tag < 16 ); + if ( s->tags[v] == 0 ) + veci_push( &s->tagged, v ); + s->tags[v] |= tag; +} +static inline void solver2_clear_tags(sat_solver3* s, int start) { + int i, * tagged = veci_begin(&s->tagged); + for (i = start; i < veci_size(&s->tagged); i++) + s->tags[tagged[i]] = 0; + veci_resize(&s->tagged,start); +} + +int sat_solver3_get_var_value(sat_solver3* s, int v) +{ + if ( var_value(s, v) == var0 ) + return l_False; + if ( var_value(s, v) == var1 ) + return l_True; + if ( var_value(s, v) == varX ) + return l_Undef; + assert( 0 ); + return 0; +} + +//================================================================================================= +// Simple helpers: + +static inline int sat_solver3_dl(sat_solver3* s) { return veci_size(&s->trail_lim); } +static inline veci* sat_solver3_read_wlist(sat_solver3* s, lit l) { return &s->wlists[l]; } + +//================================================================================================= +// Variable order functions: + +static inline void order_update(sat_solver3* s, int v) // updateorder +{ + int* orderpos = s->orderpos; + int* heap = veci_begin(&s->order); + int i = orderpos[v]; + int x = heap[i]; + int parent = (i - 1) / 2; + + assert(s->orderpos[v] != -1); + + while (i != 0 && s->activity[x] > s->activity[heap[parent]]){ + heap[i] = heap[parent]; + orderpos[heap[i]] = i; + i = parent; + parent = (i - 1) / 2; + } + + heap[i] = x; + orderpos[x] = i; +} + +static inline void order_assigned(sat_solver3* s, int v) +{ +} + +static inline void order_unassigned(sat_solver3* s, int v) // undoorder +{ + int* orderpos = s->orderpos; + if (orderpos[v] == -1){ + orderpos[v] = veci_size(&s->order); + veci_push(&s->order,v); + order_update(s,v); +//printf( "+%d ", v ); + } +} + +static inline int order_select(sat_solver3* s, float random_var_freq) // selectvar +{ + int* heap = veci_begin(&s->order); + int* orderpos = s->orderpos; + // Random decision: + if (drand(&s->random_seed) < random_var_freq){ + int next = irand(&s->random_seed,s->size); + assert(next >= 0 && next < s->size); + if (var_value(s, next) == varX) + return next; + } + // Activity based decision: + while (veci_size(&s->order) > 0){ + int next = heap[0]; + int size = veci_size(&s->order)-1; + int x = heap[size]; + veci_resize(&s->order,size); + orderpos[next] = -1; + if (size > 0){ + int i = 0; + int child = 1; + while (child < size){ + + if (child+1 < size && s->activity[heap[child]] < s->activity[heap[child+1]]) + child++; + assert(child < size); + if (s->activity[x] >= s->activity[heap[child]]) + break; + + heap[i] = heap[child]; + orderpos[heap[i]] = i; + i = child; + child = 2 * child + 1; + } + heap[i] = x; + orderpos[heap[i]] = i; + } + if (var_value(s, next) == varX) + return next; + } + return var_Undef; +} + +void sat_solver3_set_var_activity(sat_solver3* s, int * pVars, int nVars) +{ + int i; + assert( s->VarActType == 1 ); + for (i = 0; i < s->size; i++) + s->activity[i] = 0; + s->var_inc = Abc_Dbl2Word(1); + for ( i = 0; i < nVars; i++ ) + { + int iVar = pVars ? pVars[i] : i; + s->activity[iVar] = Abc_Dbl2Word(nVars-i); + order_update( s, iVar ); + } +} + +//================================================================================================= +// variable activities + +static inline void solver_init_activities(sat_solver3* s) +{ + // variable activities + s->VarActType = 0; + if ( s->VarActType == 0 ) + { + s->var_inc = (1 << 5); + s->var_decay = -1; + } + else if ( s->VarActType == 1 ) + { + s->var_inc = Abc_Dbl2Word(1.0); + s->var_decay = Abc_Dbl2Word(1.0 / 0.95); + } + else if ( s->VarActType == 2 ) + { + s->var_inc = Xdbl_FromDouble(1.0); + s->var_decay = Xdbl_FromDouble(1.0 / 0.950); + } + else assert(0); + + // clause activities + s->ClaActType = 0; + if ( s->ClaActType == 0 ) + { + s->cla_inc = (1 << 11); + s->cla_decay = -1; + } + else + { + s->cla_inc = 1; + s->cla_decay = (float)(1 / 0.999); + } +} + +static inline void act_var_rescale(sat_solver3* s) +{ + if ( s->VarActType == 0 ) + { + word* activity = s->activity; + int i; + for (i = 0; i < s->size; i++) + activity[i] >>= 19; + s->var_inc >>= 19; + s->var_inc = Abc_MaxInt( (unsigned)s->var_inc, (1<<4) ); + } + else if ( s->VarActType == 1 ) + { + double* activity = (double*)s->activity; + int i; + for (i = 0; i < s->size; i++) + activity[i] *= 1e-100; + s->var_inc = Abc_Dbl2Word( Abc_Word2Dbl(s->var_inc) * 1e-100 ); + //printf( "Rescaling var activity...\n" ); + } + else if ( s->VarActType == 2 ) + { + xdbl * activity = s->activity; + int i; + for (i = 0; i < s->size; i++) + activity[i] = Xdbl_Div( activity[i], 200 ); // activity[i] / 2^200 + s->var_inc = Xdbl_Div( s->var_inc, 200 ); + } + else assert(0); +} +static inline void act_var_bump(sat_solver3* s, int v) +{ + if ( s->VarActType == 0 ) + { + s->activity[v] += s->var_inc; + if ((unsigned)s->activity[v] & 0x80000000) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); + } + else if ( s->VarActType == 1 ) + { + double act = Abc_Word2Dbl(s->activity[v]) + Abc_Word2Dbl(s->var_inc); + s->activity[v] = Abc_Dbl2Word(act); + if (act > 1e100) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); + } + else if ( s->VarActType == 2 ) + { + s->activity[v] = Xdbl_Add( s->activity[v], s->var_inc ); + if (s->activity[v] > ABC_CONST(0x014c924d692ca61b)) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); + } + else assert(0); +} +static inline void act_var_bump_global(sat_solver3* s, int v) +{ + if ( !s->pGlobalVars || !s->pGlobalVars[v] ) + return; + if ( s->VarActType == 0 ) + { + s->activity[v] += (int)((unsigned)s->var_inc * 3); + if (s->activity[v] & 0x80000000) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); + } + else if ( s->VarActType == 1 ) + { + double act = Abc_Word2Dbl(s->activity[v]) + Abc_Word2Dbl(s->var_inc) * 3.0; + s->activity[v] = Abc_Dbl2Word(act); + if ( act > 1e100) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); + } + else if ( s->VarActType == 2 ) + { + s->activity[v] = Xdbl_Add( s->activity[v], Xdbl_Mul(s->var_inc, Xdbl_FromDouble(3.0)) ); + if (s->activity[v] > ABC_CONST(0x014c924d692ca61b)) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); + } + else assert( 0 ); +} +static inline void act_var_bump_factor(sat_solver3* s, int v) +{ + if ( !s->factors ) + return; + if ( s->VarActType == 0 ) + { + s->activity[v] += (int)((unsigned)s->var_inc * (float)s->factors[v]); + if (s->activity[v] & 0x80000000) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); + } + else if ( s->VarActType == 1 ) + { + double act = Abc_Word2Dbl(s->activity[v]) + Abc_Word2Dbl(s->var_inc) * s->factors[v]; + s->activity[v] = Abc_Dbl2Word(act); + if ( act > 1e100) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); + } + else if ( s->VarActType == 2 ) + { + s->activity[v] = Xdbl_Add( s->activity[v], Xdbl_Mul(s->var_inc, Xdbl_FromDouble(s->factors[v])) ); + if (s->activity[v] > ABC_CONST(0x014c924d692ca61b)) + act_var_rescale(s); + if (s->orderpos[v] != -1) + order_update(s,v); + } + else assert( 0 ); +} + +static inline void act_var_decay(sat_solver3* s) +{ + if ( s->VarActType == 0 ) + s->var_inc += (s->var_inc >> 4); + else if ( s->VarActType == 1 ) + s->var_inc = Abc_Dbl2Word( Abc_Word2Dbl(s->var_inc) * Abc_Word2Dbl(s->var_decay) ); + else if ( s->VarActType == 2 ) + s->var_inc = Xdbl_Mul(s->var_inc, s->var_decay); + else assert(0); +} + +// clause activities +static inline void act_clause_rescale(sat_solver3* s) +{ + if ( s->ClaActType == 0 ) + { + unsigned* activity = (unsigned *)veci_begin(&s->act_clas); + int i; + for (i = 0; i < veci_size(&s->act_clas); i++) + activity[i] >>= 14; + s->cla_inc >>= 14; + s->cla_inc = Abc_MaxInt( s->cla_inc, (1<<10) ); + } + else + { + float* activity = (float *)veci_begin(&s->act_clas); + int i; + for (i = 0; i < veci_size(&s->act_clas); i++) + activity[i] *= (float)1e-20; + s->cla_inc *= (float)1e-20; + } +} +static inline void act_clause_bump(sat_solver3* s, clause *c) +{ + if ( s->ClaActType == 0 ) + { + unsigned* act = (unsigned *)veci_begin(&s->act_clas) + c->lits[c->size]; + *act += s->cla_inc; + if ( *act & 0x80000000 ) + act_clause_rescale(s); + } + else + { + float* act = (float *)veci_begin(&s->act_clas) + c->lits[c->size]; + *act += s->cla_inc; + if (*act > 1e20) + act_clause_rescale(s); + } +} +static inline void act_clause_decay(sat_solver3* s) +{ + if ( s->ClaActType == 0 ) + s->cla_inc += (s->cla_inc >> 10); + else + s->cla_inc *= s->cla_decay; +} + + +//================================================================================================= +// Sorting functions (sigh): + +static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *)) +{ + int i, j, best_i; + void* tmp; + + for (i = 0; i < size-1; i++){ + best_i = i; + for (j = i+1; j < size; j++){ + if (comp(array[j], array[best_i]) < 0) + best_i = j; + } + tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; + } +} + +static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed) +{ + if (size <= 15) + selectionsort(array, size, comp); + + else{ + void* pivot = array[irand(seed, size)]; + void* tmp; + int i = -1; + int j = size; + + for(;;){ + do i++; while(comp(array[i], pivot)<0); + do j--; while(comp(pivot, array[j])<0); + + if (i >= j) break; + + tmp = array[i]; array[i] = array[j]; array[j] = tmp; + } + + sortrnd(array , i , comp, seed); + sortrnd(&array[i], size-i, comp, seed); + } +} + +//================================================================================================= +// Clause functions: + +static inline int sat_clause_compute_lbd( sat_solver3* s, clause* c ) +{ + int i, lev, minl = 0, lbd = 0; + for (i = 0; i < (int)c->size; i++) + { + lev = var_level(s, lit_var(c->lits[i])); + if ( !(minl & (1 << (lev & 31))) ) + { + minl |= 1 << (lev & 31); + lbd++; +// printf( "%d ", lev ); + } + } +// printf( " -> %d\n", lbd ); + return lbd; +} + +/* pre: size > 1 && no variable occurs twice + */ +int sat_solver3_clause_new(sat_solver3* s, lit* begin, lit* end, int learnt) +{ + int fUseBinaryClauses = 1; + int size; + clause* c; + int h; + + assert(end - begin > 1); + assert(learnt >= 0 && learnt < 2); + size = end - begin; + + // do not allocate memory for the two-literal problem clause + if ( fUseBinaryClauses && size == 2 && !learnt ) + { + veci_push(sat_solver3_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1]))); + veci_push(sat_solver3_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0]))); + s->stats.clauses++; + s->stats.clauses_literals += size; + return 0; + } + + // create new clause +// h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 + 1 ) << 1; + h = Sat_MemAppend( &s->Mem, begin, size, learnt, 0 ); + assert( !(h & 1) ); + if ( s->hLearnts == -1 && learnt ) + s->hLearnts = h; + if (learnt) + { + c = clause_read( s, h ); + c->lbd = sat_clause_compute_lbd( s, c ); + assert( clause_id(c) == veci_size(&s->act_clas) ); +// veci_push(&s->learned, h); +// act_clause_bump(s,clause_read(s, h)); + if ( s->ClaActType == 0 ) + veci_push(&s->act_clas, (1<<10)); + else + veci_push(&s->act_clas, s->cla_inc); + s->stats.learnts++; + s->stats.learnts_literals += size; + } + else + { + s->stats.clauses++; + s->stats.clauses_literals += size; + } + + assert(begin[0] >= 0); + assert(begin[0] < s->size*2); + assert(begin[1] >= 0); + assert(begin[1] < s->size*2); + + assert(lit_neg(begin[0]) < s->size*2); + assert(lit_neg(begin[1]) < s->size*2); + + //veci_push(sat_solver3_read_wlist(s,lit_neg(begin[0])),c); + //veci_push(sat_solver3_read_wlist(s,lit_neg(begin[1])),c); + veci_push(sat_solver3_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1]))); + veci_push(sat_solver3_read_wlist(s,lit_neg(begin[1])),(size > 2 ? h : clause_from_lit(begin[0]))); + + return h; +} + + +//================================================================================================= +// Minor (solver) functions: + +static inline int sat_solver3_enqueue(sat_solver3* s, lit l, int from) +{ + int v = lit_var(l); + if ( s->pFreqs[v] == 0 ) +// { + s->pFreqs[v] = 1; +// s->nVarUsed++; +// } + +#ifdef VERBOSEDEBUG + printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l)); +#endif + if (var_value(s, v) != varX) + return var_value(s, v) == lit_sign(l); + else{ +/* + if ( s->pCnfFunc ) + { + if ( lit_sign(l) ) + { + if ( (s->loads[v] & 1) == 0 ) + { + s->loads[v] ^= 1; + s->pCnfFunc( s->pCnfMan, l ); + } + } + else + { + if ( (s->loads[v] & 2) == 0 ) + { + s->loads[v] ^= 2; + s->pCnfFunc( s->pCnfMan, l ); + } + } + } +*/ + // New fact -- store it. +#ifdef VERBOSEDEBUG + printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l)); +#endif + var_set_value(s, v, lit_sign(l)); + var_set_level(s, v, sat_solver3_dl(s)); + s->reasons[v] = from; + s->trail[s->qtail++] = l; + order_assigned(s, v); + return true; + } +} + + +static inline int sat_solver3_decision(sat_solver3* s, lit l){ + assert(s->qtail == s->qhead); + assert(var_value(s, lit_var(l)) == varX); +#ifdef VERBOSEDEBUG + printf(L_IND"assume("L_LIT") ", L_ind, L_lit(l)); + printf( "act = %.20f\n", s->activity[lit_var(l)] ); +#endif + veci_push(&s->trail_lim,s->qtail); + return sat_solver3_enqueue(s,l,0); +} + + +static void sat_solver3_canceluntil(sat_solver3* s, int level) { + int bound; + int lastLev; + int c; + + if (sat_solver3_dl(s) <= level) + return; + + assert( veci_size(&s->trail_lim) > 0 ); + bound = (veci_begin(&s->trail_lim))[level]; + lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1]; + + //////////////////////////////////////// + // added to cancel all assignments +// if ( level == -1 ) +// bound = 0; + //////////////////////////////////////// + + for (c = s->qtail-1; c >= bound; c--) { + int x = lit_var(s->trail[c]); + var_set_value(s, x, varX); + s->reasons[x] = 0; + if ( c < lastLev ) + var_set_polar( s, x, !lit_sign(s->trail[c]) ); + } + //printf( "\n" ); + + for (c = s->qhead-1; c >= bound; c--) + order_unassigned(s,lit_var(s->trail[c])); + + s->qhead = s->qtail = bound; + veci_resize(&s->trail_lim,level); +} + +static void sat_solver3_canceluntil_rollback(sat_solver3* s, int NewBound) { + int c, x; + + assert( sat_solver3_dl(s) == 0 ); + assert( s->qtail == s->qhead ); + assert( s->qtail >= NewBound ); + + for (c = s->qtail-1; c >= NewBound; c--) + { + x = lit_var(s->trail[c]); + var_set_value(s, x, varX); + s->reasons[x] = 0; + } + + for (c = s->qhead-1; c >= NewBound; c--) + order_unassigned(s,lit_var(s->trail[c])); + + s->qhead = s->qtail = NewBound; +} + +static void sat_solver3_record(sat_solver3* s, veci* cls) +{ + lit* begin = veci_begin(cls); + lit* end = begin + veci_size(cls); + int h = (veci_size(cls) > 1) ? sat_solver3_clause_new(s,begin,end,1) : 0; + sat_solver3_enqueue(s,*begin,h); + assert(veci_size(cls) > 0); + if ( h == 0 ) + veci_push( &s->unit_lits, *begin ); + +/* + if (h != 0) { + act_clause_bump(s,clause_read(s, h)); + s->stats.learnts++; + s->stats.learnts_literals += veci_size(cls); + } +*/ +} + +int sat_solver3_count_assigned(sat_solver3* s) +{ + // count top-level assignments + int i, Count = 0; + assert(sat_solver3_dl(s) == 0); + for ( i = 0; i < s->size; i++ ) + if (var_value(s, i) != varX) + Count++; + return Count; +} + +static double sat_solver3_progress(sat_solver3* s) +{ + int i; + double progress = 0; + double F = 1.0 / s->size; + for (i = 0; i < s->size; i++) + if (var_value(s, i) != varX) + progress += pow(F, var_level(s, i)); + return progress / s->size; +} + +//================================================================================================= +// Major methods: + +static int sat_solver3_lit_removable(sat_solver3* s, int x, int minl) +{ + int top = veci_size(&s->tagged); + + assert(s->reasons[x] != 0); + veci_resize(&s->stack,0); + veci_push(&s->stack,x); + + while (veci_size(&s->stack)){ + int v = veci_pop(&s->stack); + assert(s->reasons[v] != 0); + if (clause_is_lit(s->reasons[v])){ + v = lit_var(clause_read_lit(s->reasons[v])); + if (!var_tag(s,v) && var_level(s, v)){ + if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){ + veci_push(&s->stack,v); + var_set_tag(s, v, 1); + }else{ + solver2_clear_tags(s, top); + return 0; + } + } + }else{ + clause* c = clause_read(s, s->reasons[v]); + lit* lits = clause_begin(c); + int i; + for (i = 1; i < clause_size(c); i++){ + int v = lit_var(lits[i]); + if (!var_tag(s,v) && var_level(s, v)){ + if (s->reasons[v] != 0 && ((1 << (var_level(s, v) & 31)) & minl)){ + veci_push(&s->stack,lit_var(lits[i])); + var_set_tag(s, v, 1); + }else{ + solver2_clear_tags(s, top); + return 0; + } + } + } + } + } + return 1; +} + + +/*_________________________________________________________________________________________________ +| +| analyzeFinal : (p : Lit) -> [void] +| +| Description: +| Specialized analysis procedure to express the final conflict in terms of assumptions. +| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and +| stores the result in 'out_conflict'. +|________________________________________________________________________________________________@*/ +/* +void Solver::analyzeFinal(Clause* confl, bool skip_first) +{ + // -- NOTE! This code is relatively untested. Please report bugs! + conflict.clear(); + if (root_level == 0) return; + + vec<char>& seen = analyze_seen; + for (int i = skip_first ? 1 : 0; i < confl->size(); i++){ + Var x = var((*confl)[i]); + if (level[x] > 0) + seen[x] = 1; + } + + int start = (root_level >= trail_lim.size()) ? trail.size()-1 : trail_lim[root_level]; + for (int i = start; i >= trail_lim[0]; i--){ + Var x = var(trail[i]); + if (seen[x]){ + GClause r = reason[x]; + if (r == GClause_NULL){ + assert(level[x] > 0); + conflict.push(~trail[i]); + }else{ + if (r.isLit()){ + Lit p = r.lit(); + if (level[var(p)] > 0) + seen[var(p)] = 1; + }else{ + Clause& c = *r.clause(); + for (int j = 1; j < c.size(); j++) + if (level[var(c[j])] > 0) + seen[var(c[j])] = 1; + } + } + seen[x] = 0; + } + } +} +*/ + +#ifdef SAT_USE_ANALYZE_FINAL + +static void sat_solver3_analyze_final(sat_solver3* s, int hConf, int skip_first) +{ + clause* conf = clause_read(s, hConf); + int i, j, start; + veci_resize(&s->conf_final,0); + if ( s->root_level == 0 ) + return; + assert( veci_size(&s->tagged) == 0 ); +// assert( s->tags[lit_var(p)] == l_Undef ); +// s->tags[lit_var(p)] = l_True; + for (i = skip_first ? 1 : 0; i < clause_size(conf); i++) + { + int x = lit_var(clause_begin(conf)[i]); + if (var_level(s, x) > 0) + var_set_tag(s, x, 1); + } + + start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->root_level]; + for (i = start; i >= (veci_begin(&s->trail_lim))[0]; i--){ + int x = lit_var(s->trail[i]); + if (var_tag(s,x)){ + if (s->reasons[x] == 0){ + assert(var_level(s, x) > 0); + veci_push(&s->conf_final,lit_neg(s->trail[i])); + }else{ + if (clause_is_lit(s->reasons[x])){ + lit q = clause_read_lit(s->reasons[x]); + assert(lit_var(q) >= 0 && lit_var(q) < s->size); + if (var_level(s, lit_var(q)) > 0) + var_set_tag(s, lit_var(q), 1); + } + else{ + clause* c = clause_read(s, s->reasons[x]); + int* lits = clause_begin(c); + for (j = 1; j < clause_size(c); j++) + if (var_level(s, lit_var(lits[j])) > 0) + var_set_tag(s, lit_var(lits[j]), 1); + } + } + } + } + solver2_clear_tags(s,0); +} + +#endif + +static void sat_solver3_analyze(sat_solver3* s, int h, veci* learnt) +{ + lit* trail = s->trail; + int cnt = 0; + lit p = lit_Undef; + int ind = s->qtail-1; + lit* lits; + int i, j, minl; + veci_push(learnt,lit_Undef); + do{ + assert(h != 0); + if (clause_is_lit(h)){ + int x = lit_var(clause_read_lit(h)); + if (var_tag(s, x) == 0 && var_level(s, x) > 0){ + var_set_tag(s, x, 1); + act_var_bump(s,x); + if (var_level(s, x) == sat_solver3_dl(s)) + cnt++; + else + veci_push(learnt,clause_read_lit(h)); + } + }else{ + clause* c = clause_read(s, h); + + if (clause_learnt(c)) + act_clause_bump(s,c); + lits = clause_begin(c); + //printlits(lits,lits+clause_size(c)); printf("\n"); + for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){ + int x = lit_var(lits[j]); + if (var_tag(s, x) == 0 && var_level(s, x) > 0){ + var_set_tag(s, x, 1); + act_var_bump(s,x); + // bump variables propaged by the LBD=2 clause +// if ( s->reasons[x] && clause_read(s, s->reasons[x])->lbd <= 2 ) +// act_var_bump(s,x); + if (var_level(s,x) == sat_solver3_dl(s)) + cnt++; + else + veci_push(learnt,lits[j]); + } + } + } + + while ( !var_tag(s, lit_var(trail[ind--])) ); + + p = trail[ind+1]; + h = s->reasons[lit_var(p)]; + cnt--; + + }while (cnt > 0); + + *veci_begin(learnt) = lit_neg(p); + + lits = veci_begin(learnt); + minl = 0; + for (i = 1; i < veci_size(learnt); i++){ + int lev = var_level(s, lit_var(lits[i])); + minl |= 1 << (lev & 31); + } + + // simplify (full) + for (i = j = 1; i < veci_size(learnt); i++){ + if (s->reasons[lit_var(lits[i])] == 0 || !sat_solver3_lit_removable(s,lit_var(lits[i]),minl)) + lits[j++] = lits[i]; + } + + // update size of learnt + statistics + veci_resize(learnt,j); + s->stats.tot_literals += j; + + + // clear tags + solver2_clear_tags(s,0); + +#ifdef DEBUG + for (i = 0; i < s->size; i++) + assert(!var_tag(s, i)); +#endif + +#ifdef VERBOSEDEBUG + printf(L_IND"Learnt {", L_ind); + for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i])); +#endif + if (veci_size(learnt) > 1){ + int max_i = 1; + int max = var_level(s, lit_var(lits[1])); + lit tmp; + + for (i = 2; i < veci_size(learnt); i++) + if (var_level(s, lit_var(lits[i])) > max){ + max = var_level(s, lit_var(lits[i])); + max_i = i; + } + + tmp = lits[1]; + lits[1] = lits[max_i]; + lits[max_i] = tmp; + } +#ifdef VERBOSEDEBUG + { + int lev = veci_size(learnt) > 1 ? var_level(s, lit_var(lits[1])) : 0; + printf(" } at level %d\n", lev); + } +#endif +} + +//#define TEST_CNF_LOAD + +int sat_solver3_propagate(sat_solver3* s) +{ + int hConfl = 0; + lit* lits; + lit false_lit; + + //printf("sat_solver3_propagate\n"); + while (hConfl == 0 && s->qtail - s->qhead > 0){ + lit p = s->trail[s->qhead++]; + +#ifdef TEST_CNF_LOAD + int v = lit_var(p); + if ( s->pCnfFunc ) + { + if ( lit_sign(p) ) + { + if ( (s->loads[v] & 1) == 0 ) + { + s->loads[v] ^= 1; + s->pCnfFunc( s->pCnfMan, p ); + } + } + else + { + if ( (s->loads[v] & 2) == 0 ) + { + s->loads[v] ^= 2; + s->pCnfFunc( s->pCnfMan, p ); + } + } + } + { +#endif + + veci* ws = sat_solver3_read_wlist(s,p); + int* begin = veci_begin(ws); + int* end = begin + veci_size(ws); + int*i, *j; + + 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; ){ + if (clause_is_lit(*i)){ + + int Lit = clause_read_lit(*i); + if (var_value(s, lit_var(Lit)) == lit_sign(Lit)){ + *j++ = *i++; + continue; + } + + *j++ = *i; + if (!sat_solver3_enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ + hConfl = s->hBinary; + (clause_begin(s->binary))[1] = lit_neg(p); + (clause_begin(s->binary))[0] = clause_read_lit(*i++); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + }else{ + + clause* c = clause_read(s,*i); + lits = clause_begin(c); + + // Make sure the false literal is data[1]: + false_lit = lit_neg(p); + if (lits[0] == false_lit){ + lits[0] = lits[1]; + lits[1] = false_lit; + } + assert(lits[1] == false_lit); + + // If 0th watch is true, then clause is already satisfied. + if (var_value(s, lit_var(lits[0])) == lit_sign(lits[0])) + *j++ = *i; + else{ + // Look for new watch: + lit* stop = lits + clause_size(c); + lit* k; + for (k = lits + 2; k < stop; k++){ + if (var_value(s, lit_var(*k)) != !lit_sign(*k)){ + lits[1] = *k; + *k = false_lit; + veci_push(sat_solver3_read_wlist(s,lit_neg(lits[1])),*i); + goto next; } + } + + *j++ = *i; + // Clause is unit under assignment: + if ( c->lrn ) + c->lbd = sat_clause_compute_lbd(s, c); + if (!sat_solver3_enqueue(s,lits[0], *i)){ + hConfl = *i++; + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } + } + } + next: + i++; + } + + s->stats.inspects += j - veci_begin(ws); + veci_resize(ws,j - veci_begin(ws)); +#ifdef TEST_CNF_LOAD + } +#endif + } + + return hConfl; +} + +//================================================================================================= +// External solver functions: + +sat_solver3* sat_solver3_new(void) +{ + sat_solver3* s = (sat_solver3*)ABC_CALLOC( char, sizeof(sat_solver3)); + +// Vec_SetAlloc_(&s->Mem, 15); + Sat_MemAlloc_(&s->Mem, 17); + s->hLearnts = -1; + s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 ); + s->binary = clause_read( s, s->hBinary ); + + s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit + s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit + s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit + s->nLearntMax = s->nLearntStart; + + // initialize vectors + veci_new(&s->order); + veci_new(&s->trail_lim); + veci_new(&s->tagged); +// veci_new(&s->learned); + veci_new(&s->act_clas); + veci_new(&s->stack); +// veci_new(&s->model); + veci_new(&s->unit_lits); + veci_new(&s->temp_clause); + veci_new(&s->conf_final); + + // initialize arrays + s->wlists = 0; + s->activity = 0; + s->orderpos = 0; + s->reasons = 0; + s->trail = 0; + + // initialize other vars + s->size = 0; + s->cap = 0; + s->qhead = 0; + s->qtail = 0; + + solver_init_activities(s); + veci_new(&s->act_vars); + + s->root_level = 0; +// s->simpdb_assigns = 0; +// s->simpdb_props = 0; + s->random_seed = 91648253; + s->progress_estimate = 0; +// s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2); +// s->binary->size_learnt = (2 << 1); + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.tot_literals = 0; + return s; +} + +sat_solver3* zsat_solver3_new_seed(double seed) +{ + sat_solver3* s = (sat_solver3*)ABC_CALLOC( char, sizeof(sat_solver3)); + +// Vec_SetAlloc_(&s->Mem, 15); + Sat_MemAlloc_(&s->Mem, 15); + s->hLearnts = -1; + s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 ); + s->binary = clause_read( s, s->hBinary ); + + s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit + s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit + s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit + s->nLearntMax = s->nLearntStart; + + // initialize vectors + veci_new(&s->order); + veci_new(&s->trail_lim); + veci_new(&s->tagged); +// veci_new(&s->learned); + veci_new(&s->act_clas); + veci_new(&s->stack); +// veci_new(&s->model); + veci_new(&s->unit_lits); + veci_new(&s->temp_clause); + veci_new(&s->conf_final); + + // initialize arrays + s->wlists = 0; + s->activity = 0; + s->orderpos = 0; + s->reasons = 0; + s->trail = 0; + + // initialize other vars + s->size = 0; + s->cap = 0; + s->qhead = 0; + s->qtail = 0; + + solver_init_activities(s); + veci_new(&s->act_vars); + + s->root_level = 0; +// s->simpdb_assigns = 0; +// s->simpdb_props = 0; + s->random_seed = seed; + s->progress_estimate = 0; +// s->binary = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2); +// s->binary->size_learnt = (2 << 1); + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.tot_literals = 0; + return s; +} + +void sat_solver3_setnvars(sat_solver3* s,int n) +{ + int var; + + if (s->cap < n){ + int old_cap = s->cap; + while (s->cap < n) s->cap = s->cap*2+1; + if ( s->cap < 50000 ) + s->cap = 50000; + + s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2); +// s->vi = ABC_REALLOC(varinfo,s->vi, s->cap); + s->levels = ABC_REALLOC(int, s->levels, s->cap); + s->assigns = ABC_REALLOC(char, s->assigns, s->cap); + s->polarity = ABC_REALLOC(char, s->polarity, s->cap); + s->tags = ABC_REALLOC(char, s->tags, s->cap); + s->loads = ABC_REALLOC(char, s->loads, s->cap); + s->activity = ABC_REALLOC(word, s->activity, s->cap); + s->activity2 = ABC_REALLOC(word, s->activity2,s->cap); + s->pFreqs = ABC_REALLOC(char, s->pFreqs, s->cap); + + if ( s->factors ) + s->factors = ABC_REALLOC(double, s->factors, s->cap); + s->orderpos = ABC_REALLOC(int, s->orderpos, s->cap); + s->reasons = ABC_REALLOC(int, s->reasons, s->cap); + s->trail = ABC_REALLOC(lit, s->trail, s->cap); + s->model = ABC_REALLOC(int, s->model, s->cap); + memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) ); + } + + for (var = s->size; var < n; var++){ + assert(!s->wlists[2*var].size); + assert(!s->wlists[2*var+1].size); + if ( s->wlists[2*var].ptr == NULL ) + veci_new(&s->wlists[2*var]); + if ( s->wlists[2*var+1].ptr == NULL ) + veci_new(&s->wlists[2*var+1]); + + if ( s->VarActType == 0 ) + s->activity[var] = (1<<10); + else if ( s->VarActType == 1 ) + s->activity[var] = 0; + else if ( s->VarActType == 2 ) + s->activity[var] = 0; + else assert(0); + + s->pFreqs[var] = 0; + if ( s->factors ) + s->factors [var] = 0; +// *((int*)s->vi + var) = 0; s->vi[var].val = varX; + s->levels [var] = 0; + s->assigns [var] = varX; + s->polarity[var] = 0; + s->tags [var] = 0; + s->loads [var] = 0; + s->orderpos[var] = veci_size(&s->order); + s->reasons [var] = 0; + s->model [var] = 0; + + /* does not hold because variables enqueued at top level will not be reinserted in the heap + assert(veci_size(&s->order) == var); + */ + veci_push(&s->order,var); + order_update(s, var); + } + + s->size = n > s->size ? n : s->size; +} + +void sat_solver3_delete(sat_solver3* s) +{ +// Vec_SetFree_( &s->Mem ); + Sat_MemFree_( &s->Mem ); + + // delete vectors + veci_delete(&s->order); + veci_delete(&s->trail_lim); + veci_delete(&s->tagged); +// veci_delete(&s->learned); + veci_delete(&s->act_clas); + veci_delete(&s->stack); +// veci_delete(&s->model); + veci_delete(&s->act_vars); + veci_delete(&s->unit_lits); + veci_delete(&s->pivot_vars); + veci_delete(&s->temp_clause); + veci_delete(&s->conf_final); + + // delete arrays + if (s->reasons != 0){ + int i; + for (i = 0; i < s->cap*2; i++) + veci_delete(&s->wlists[i]); + ABC_FREE(s->wlists ); +// ABC_FREE(s->vi ); + ABC_FREE(s->levels ); + ABC_FREE(s->assigns ); + ABC_FREE(s->polarity ); + ABC_FREE(s->tags ); + ABC_FREE(s->loads ); + ABC_FREE(s->activity ); + ABC_FREE(s->activity2); + ABC_FREE(s->pFreqs ); + ABC_FREE(s->factors ); + ABC_FREE(s->orderpos ); + ABC_FREE(s->reasons ); + ABC_FREE(s->trail ); + ABC_FREE(s->model ); + } + + ABC_FREE(s); +} + +void sat_solver3_restart( sat_solver3* s ) +{ + int i; + Sat_MemRestart( &s->Mem ); + s->hLearnts = -1; + s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 ); + s->binary = clause_read( s, s->hBinary ); + + veci_resize(&s->trail_lim, 0); + veci_resize(&s->order, 0); + for ( i = 0; i < s->size*2; i++ ) + s->wlists[i].size = 0; + + s->nDBreduces = 0; + + // initialize other vars + s->size = 0; +// s->cap = 0; + s->qhead = 0; + s->qtail = 0; + + + // variable activities + solver_init_activities(s); + veci_resize(&s->act_clas, 0); + + + s->root_level = 0; +// s->simpdb_assigns = 0; +// s->simpdb_props = 0; + s->random_seed = 91648253; + s->progress_estimate = 0; + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.tot_literals = 0; +} + +void zsat_solver3_restart_seed( sat_solver3* s, double seed ) +{ + int i; + Sat_MemRestart( &s->Mem ); + s->hLearnts = -1; + s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 ); + s->binary = clause_read( s, s->hBinary ); + + veci_resize(&s->trail_lim, 0); + veci_resize(&s->order, 0); + for ( i = 0; i < s->size*2; i++ ) + s->wlists[i].size = 0; + + s->nDBreduces = 0; + + // initialize other vars + s->size = 0; +// s->cap = 0; + s->qhead = 0; + s->qtail = 0; + + solver_init_activities(s); + veci_resize(&s->act_clas, 0); + + s->root_level = 0; +// s->simpdb_assigns = 0; +// s->simpdb_props = 0; + s->random_seed = seed; + s->progress_estimate = 0; + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.tot_literals = 0; +} + +// returns memory in bytes used by the SAT solver +double sat_solver3_memory( sat_solver3* s ) +{ + int i; + double Mem = sizeof(sat_solver3); + for (i = 0; i < s->cap*2; i++) + Mem += s->wlists[i].cap * sizeof(int); + Mem += s->cap * sizeof(veci); // ABC_FREE(s->wlists ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->levels ); + Mem += s->cap * sizeof(char); // ABC_FREE(s->assigns ); + Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity ); + Mem += s->cap * sizeof(char); // ABC_FREE(s->tags ); + Mem += s->cap * sizeof(char); // ABC_FREE(s->loads ); + Mem += s->cap * sizeof(word); // ABC_FREE(s->activity ); + if ( s->activity2 ) + Mem += s->cap * sizeof(word); // ABC_FREE(s->activity ); + if ( s->factors ) + Mem += s->cap * sizeof(double); // ABC_FREE(s->factors ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->orderpos ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->reasons ); + Mem += s->cap * sizeof(lit); // ABC_FREE(s->trail ); + Mem += s->cap * sizeof(int); // ABC_FREE(s->model ); + + Mem += s->order.cap * sizeof(int); + Mem += s->trail_lim.cap * sizeof(int); + Mem += s->tagged.cap * sizeof(int); +// Mem += s->learned.cap * sizeof(int); + Mem += s->stack.cap * sizeof(int); + Mem += s->act_vars.cap * sizeof(int); + Mem += s->unit_lits.cap * sizeof(int); + Mem += s->act_clas.cap * sizeof(int); + Mem += s->temp_clause.cap * sizeof(int); + Mem += s->conf_final.cap * sizeof(int); + Mem += Sat_MemMemoryAll( &s->Mem ); + return Mem; +} + +int sat_solver3_simplify(sat_solver3* s) +{ + assert(sat_solver3_dl(s) == 0); + if (sat_solver3_propagate(s) != 0) + return false; + return true; +} + +void sat_solver3_reducedb(sat_solver3* s) +{ + static abctime TimeTotal = 0; + abctime clk = Abc_Clock(); + Sat_Mem_t * pMem = &s->Mem; + int nLearnedOld = veci_size(&s->act_clas); + int * act_clas = veci_begin(&s->act_clas); + int * pPerm, * pArray, * pSortValues, nCutoffValue; + int i, k, j, Id, Counter, CounterStart, nSelected; + clause * c; + + assert( s->nLearntMax > 0 ); + assert( nLearnedOld == Sat_MemEntryNum(pMem, 1) ); + assert( nLearnedOld == (int)s->stats.learnts ); + + s->nDBreduces++; + + //printf( "Calling reduceDB with %d learned clause limit.\n", s->nLearntMax ); + s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces; +// return; + + // create sorting values + pSortValues = ABC_ALLOC( int, nLearnedOld ); + Sat_MemForEachLearned( pMem, c, i, k ) + { + Id = clause_id(c); +// pSortValues[Id] = act[Id]; + if ( s->ClaActType == 0 ) + pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4); + else + pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28);// | (act_clas[Id] >> 4); + assert( pSortValues[Id] >= 0 ); + } + + // preserve 1/20 of last clauses + CounterStart = nLearnedOld - (s->nLearntMax / 20); + + // preserve 3/4 of most active clauses + nSelected = nLearnedOld*s->nLearntRatio/100; + + // find non-decreasing permutation + pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld ); + assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] ); + nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]]; + ABC_FREE( pPerm ); +// ActCutOff = ABC_INFINITY; + + // mark learned clauses to remove + Counter = j = 0; + Sat_MemForEachLearned( pMem, c, i, k ) + { + assert( c->mark == 0 ); + if ( Counter++ > CounterStart || clause_size(c) < 3 || pSortValues[clause_id(c)] > nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) ) + act_clas[j++] = act_clas[clause_id(c)]; + else // delete + { + c->mark = 1; + s->stats.learnts_literals -= clause_size(c); + s->stats.learnts--; + } + } + assert( s->stats.learnts == (unsigned)j ); + assert( Counter == nLearnedOld ); + veci_resize(&s->act_clas,j); + ABC_FREE( pSortValues ); + + // update ID of each clause to be its new handle + Counter = Sat_MemCompactLearned( pMem, 0 ); + assert( Counter == (int)s->stats.learnts ); + + // update reasons + for ( i = 0; i < s->size; i++ ) + { + if ( !s->reasons[i] ) // no reason + continue; + if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause + continue; + if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause + continue; + c = clause_read( s, s->reasons[i] ); + assert( c->mark == 0 ); + s->reasons[i] = clause_id(c); // updating handle here!!! + } + + // update watches + for ( i = 0; i < s->size*2; i++ ) + { + pArray = veci_begin(&s->wlists[i]); + for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) + { + if ( clause_is_lit(pArray[k]) ) // 2-lit clause + pArray[j++] = pArray[k]; + else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause + pArray[j++] = pArray[k]; + else + { + c = clause_read(s, pArray[k]); + if ( !c->mark ) // useful learned clause + pArray[j++] = clause_id(c); // updating handle here!!! + } + } + veci_resize(&s->wlists[i],j); + } + + // perform final move of the clauses + Counter = Sat_MemCompactLearned( pMem, 1 ); + assert( Counter == (int)s->stats.learnts ); + + // report the results + TimeTotal += Abc_Clock() - clk; + if ( s->fVerbose ) + { + Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) ", + s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld ); + Abc_PrintTime( 1, "Time", TimeTotal ); + } +} + + +// reverses to the previously bookmarked point +void sat_solver3_rollback( sat_solver3* s ) +{ + Sat_Mem_t * pMem = &s->Mem; + int i, k, j; + static int Count = 0; + Count++; + assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size ); + assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail ); + // reset implication queue + sat_solver3_canceluntil_rollback( s, s->iTrailPivot ); + // update order + if ( s->iVarPivot < s->size ) + { + if ( s->activity2 ) + { + s->var_inc = s->var_inc2; + memcpy( s->activity, s->activity2, sizeof(word) * s->iVarPivot ); + } + veci_resize(&s->order, 0); + for ( i = 0; i < s->iVarPivot; i++ ) + { + if ( var_value(s, i) != varX ) + continue; + s->orderpos[i] = veci_size(&s->order); + veci_push(&s->order,i); + order_update(s, i); + } + } + // compact watches + for ( i = 0; i < s->iVarPivot*2; i++ ) + { + cla* pArray = veci_begin(&s->wlists[i]); + for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ ) + { + if ( clause_is_lit(pArray[k]) ) + { + if ( clause_read_lit(pArray[k]) < s->iVarPivot*2 ) + pArray[j++] = pArray[k]; + } + else if ( Sat_MemClauseUsed(pMem, pArray[k]) ) + pArray[j++] = pArray[k]; + } + veci_resize(&s->wlists[i],j); + } + // reset watcher lists + for ( i = 2*s->iVarPivot; i < 2*s->size; i++ ) + s->wlists[i].size = 0; + + // reset clause counts + s->stats.clauses = pMem->BookMarkE[0]; + s->stats.learnts = pMem->BookMarkE[1]; + // rollback clauses + Sat_MemRollBack( pMem ); + + // resize learned arrays + veci_resize(&s->act_clas, s->stats.learnts); + + // initialize other vars + s->size = s->iVarPivot; + if ( s->size == 0 ) + { + // s->size = 0; + // s->cap = 0; + s->qhead = 0; + s->qtail = 0; + + solver_init_activities(s); + + s->root_level = 0; + s->random_seed = 91648253; + s->progress_estimate = 0; + s->verbosity = 0; + + s->stats.starts = 0; + s->stats.decisions = 0; + s->stats.propagations = 0; + s->stats.inspects = 0; + s->stats.conflicts = 0; + s->stats.clauses = 0; + s->stats.clauses_literals = 0; + s->stats.learnts = 0; + s->stats.learnts_literals = 0; + s->stats.tot_literals = 0; + + // initialize rollback + s->iVarPivot = 0; // the pivot for variables + s->iTrailPivot = 0; // the pivot for trail + s->hProofPivot = 1; // the pivot for proof records + } +} + + +int sat_solver3_addclause(sat_solver3* s, lit* begin, lit* end) +{ + int fVerbose = 0; + lit *i,*j; + int maxvar; + lit last; + assert( begin < end ); + if ( fVerbose ) + { + for ( i = begin; i < end; i++ ) + printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 ); + printf( "\n" ); + } + + veci_resize( &s->temp_clause, 0 ); + for ( i = begin; i < end; i++ ) + veci_push( &s->temp_clause, *i ); + begin = veci_begin( &s->temp_clause ); + end = begin + veci_size( &s->temp_clause ); + + // insertion sort + maxvar = lit_var(*begin); + for (i = begin + 1; i < end; i++){ + lit l = *i; + maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar; + for (j = i; j > begin && *(j-1) > l; j--) + *j = *(j-1); + *j = l; + } + sat_solver3_setnvars(s,maxvar+1); + + // delete duplicates + last = lit_Undef; + for (i = j = begin; i < end; i++){ + //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)])); + if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i)) + return true; // tautology + else if (*i != last && var_value(s, lit_var(*i)) == varX) + last = *j++ = *i; + } +// j = i; + + if (j == begin) // empty clause + return false; + + if (j - begin == 1) // unit clause + return sat_solver3_enqueue(s,*begin,0); + + // create new clause + sat_solver3_clause_new(s,begin,j,0); + return true; +} + +static double luby(double y, int x) +{ + int size, seq; + for (size = 1, seq = 0; size < x+1; seq++, size = 2*size + 1); + while (size-1 != x){ + size = (size-1) >> 1; + seq--; + x = x % size; + } + return pow(y, (double)seq); +} + +static void luby_test() +{ + int i; + for ( i = 0; i < 20; i++ ) + printf( "%d ", (int)luby(2,i) ); + printf( "\n" ); +} + +static lbool sat_solver3_search(sat_solver3* s, ABC_INT64_T nof_conflicts) +{ +// double var_decay = 0.95; +// double clause_decay = 0.999; + double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; + ABC_INT64_T conflictC = 0; + veci learnt_clause; + int i; + + assert(s->root_level == sat_solver3_dl(s)); + + s->nRestarts++; + s->stats.starts++; +// s->var_decay = (float)(1 / var_decay ); // move this to sat_solver3_new() +// s->cla_decay = (float)(1 / clause_decay); // move this to sat_solver3_new() +// veci_resize(&s->model,0); + veci_new(&learnt_clause); + + // use activity factors in every even restart + if ( (s->nRestarts & 1) && veci_size(&s->act_vars) > 0 ) +// if ( veci_size(&s->act_vars) > 0 ) + for ( i = 0; i < s->act_vars.size; i++ ) + act_var_bump_factor(s, s->act_vars.ptr[i]); + + // use activity factors in every restart + if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 ) + for ( i = 0; i < s->act_vars.size; i++ ) + act_var_bump_global(s, s->act_vars.ptr[i]); + + for (;;){ + int hConfl = sat_solver3_propagate(s); + if (hConfl != 0){ + // CONFLICT + int blevel; + +#ifdef VERBOSEDEBUG + printf(L_IND"**CONFLICT**\n", L_ind); +#endif + s->stats.conflicts++; conflictC++; + if (sat_solver3_dl(s) == s->root_level){ +#ifdef SAT_USE_ANALYZE_FINAL + sat_solver3_analyze_final(s, hConfl, 0); +#endif + veci_delete(&learnt_clause); + return l_False; + } + + veci_resize(&learnt_clause,0); + sat_solver3_analyze(s, hConfl, &learnt_clause); + blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level; + blevel = s->root_level > blevel ? s->root_level : blevel; + sat_solver3_canceluntil(s,blevel); + sat_solver3_record(s,&learnt_clause); +#ifdef SAT_USE_ANALYZE_FINAL +// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0; // (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions) + if ( learnt_clause.size == 1 ) + var_set_level(s, lit_var(learnt_clause.ptr[0]), 0); +#endif + act_var_decay(s); + act_clause_decay(s); + + }else{ + // NO CONFLICT + int next; + + // Reached bound on number of conflicts: + if ( (!s->fNoRestarts && nof_conflicts >= 0 && conflictC >= nof_conflicts) || (s->nRuntimeLimit && (s->stats.conflicts & 63) == 0 && Abc_Clock() > s->nRuntimeLimit)){ + s->progress_estimate = sat_solver3_progress(s); + sat_solver3_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + return l_Undef; } + + // Reached bound on number of conflicts: + if ( (s->nConfLimit && s->stats.conflicts > s->nConfLimit) || + (s->nInsLimit && s->stats.propagations > s->nInsLimit) ) + { + s->progress_estimate = sat_solver3_progress(s); + sat_solver3_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + return l_Undef; + } + + // Simplify the set of problem clauses: + if (sat_solver3_dl(s) == 0 && !s->fSkipSimplify) + sat_solver3_simplify(s); + + // Reduce the set of learnt clauses: +// if (s->nLearntMax && veci_size(&s->learned) - s->qtail >= s->nLearntMax) + if (s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax) + sat_solver3_reducedb(s); + + // New variable decision: + s->stats.decisions++; + next = order_select(s,(float)random_var_freq); + + if (next == var_Undef){ + // Model found: + int i; + for (i = 0; i < s->size; i++) + s->model[i] = (var_value(s,i)==var1 ? l_True : l_False); + sat_solver3_canceluntil(s,s->root_level); + veci_delete(&learnt_clause); + + /* + veci apa; veci_new(&apa); + for (i = 0; i < s->size; i++) + veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i)))); + printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n"); + veci_delete(&apa); + */ + + return l_True; + } + + if ( var_polar(s, next) ) // positive polarity + sat_solver3_decision(s,toLit(next)); + else + sat_solver3_decision(s,lit_neg(toLit(next))); + } + } + + return l_Undef; // cannot happen +} + +// internal call to the SAT solver +int sat_solver3_solve_internal(sat_solver3* s) +{ + lbool status = l_Undef; + int restart_iter = 0; + veci_resize(&s->unit_lits, 0); + s->nCalls++; + + if (s->verbosity >= 1){ + printf("==================================[MINISAT]===================================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + printf("| | Clauses Literals | Limit Clauses Literals Lit/Cl | |\n"); + printf("==============================================================================\n"); + } + + while (status == l_Undef){ + ABC_INT64_T nof_conflicts; + double Ratio = (s->stats.learnts == 0)? 0.0 : + s->stats.learnts_literals / (double)s->stats.learnts; + if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit ) + break; + if (s->verbosity >= 1) + { + printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", + (double)s->stats.conflicts, + (double)s->stats.clauses, + (double)s->stats.clauses_literals, + (double)0, + (double)s->stats.learnts, + (double)s->stats.learnts_literals, + Ratio, + s->progress_estimate*100); + fflush(stdout); + } + nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) ); + status = sat_solver3_search(s, nof_conflicts); + // quit the loop if reached an external limit + if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit ) + break; + if ( s->nInsLimit && s->stats.propagations > s->nInsLimit ) + break; + if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit ) + break; + } + if (s->verbosity >= 1) + printf("==============================================================================\n"); + + sat_solver3_canceluntil(s,s->root_level); + return status; +} + +// pushing one assumption to the stack of assumptions +int sat_solver3_push(sat_solver3* s, int p) +{ + assert(lit_var(p) < s->size); + veci_push(&s->trail_lim,s->qtail); + s->root_level++; + if (!sat_solver3_enqueue(s,p,0)) + { + int h = s->reasons[lit_var(p)]; + if (h) + { + if (clause_is_lit(h)) + { + (clause_begin(s->binary))[1] = lit_neg(p); + (clause_begin(s->binary))[0] = clause_read_lit(h); + h = s->hBinary; + } + sat_solver3_analyze_final(s, h, 1); + veci_push(&s->conf_final, lit_neg(p)); + } + else + { + veci_resize(&s->conf_final,0); + veci_push(&s->conf_final, lit_neg(p)); + // the two lines below are a bug fix by Siert Wieringa + if (var_level(s, lit_var(p)) > 0) + veci_push(&s->conf_final, p); + } + //sat_solver3_canceluntil(s, 0); + return false; + } + else + { + int fConfl = sat_solver3_propagate(s); + if (fConfl){ + sat_solver3_analyze_final(s, fConfl, 0); + //assert(s->conf_final.size > 0); + //sat_solver3_canceluntil(s, 0); + return false; } + } + return true; +} + +// removing one assumption from the stack of assumptions +void sat_solver3_pop(sat_solver3* s) +{ + assert( sat_solver3_dl(s) > 0 ); + sat_solver3_canceluntil(s, --s->root_level); +} + +void sat_solver3_set_resource_limits(sat_solver3* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) +{ + // set the external limits + s->nRestarts = 0; + s->nConfLimit = 0; + s->nInsLimit = 0; + if ( nConfLimit ) + s->nConfLimit = s->stats.conflicts + nConfLimit; + if ( nInsLimit ) +// s->nInsLimit = s->stats.inspects + nInsLimit; + s->nInsLimit = s->stats.propagations + nInsLimit; + if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) ) + s->nConfLimit = nConfLimitGlobal; + if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) ) + s->nInsLimit = nInsLimitGlobal; +} + +int sat_solver3_solve(sat_solver3* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal) +{ + lbool status; + lit * i; + if ( s->fSolved ) + return l_False; + + if ( s->fVerbose ) + printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio ); + + sat_solver3_set_resource_limits( s, nConfLimit, nInsLimit, nConfLimitGlobal, nInsLimitGlobal ); + +#ifdef SAT_USE_ANALYZE_FINAL + // Perform assumptions: + s->root_level = 0; + for ( i = begin; i < end; i++ ) + if ( !sat_solver3_push(s, *i) ) + { + sat_solver3_canceluntil(s,0); + s->root_level = 0; + return l_False; + } + assert(s->root_level == sat_solver3_dl(s)); +#else + //printf("solve: "); printlits(begin, end); printf("\n"); + for (i = begin; i < end; i++){ +// switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){ + switch (var_value(s, *i)) { + case var1: // l_True: + break; + case varX: // l_Undef + sat_solver3_decision(s, *i); + if (sat_solver3_propagate(s) == 0) + break; + // fallthrough + case var0: // l_False + sat_solver3_canceluntil(s, 0); + return l_False; + } + } + s->root_level = sat_solver3_dl(s); +#endif + + status = sat_solver3_solve_internal(s); + + sat_solver3_canceluntil(s,0); + s->root_level = 0; + return status; +} + +// This LEXSAT procedure should be called with a set of literals (pLits, nLits), +// which defines both (1) variable order, and (2) assignment to begin search from. +// It retuns the LEXSAT assigment that is the same or larger than the given one. +// (It assumes that there is no smaller assignment than the one given!) +// The resulting assignment is returned in the same set of literals (pLits, nLits). +// It pushes/pops assumptions internally and will undo them before terminating. +int sat_solver3_solve_lexsat( sat_solver3* s, int * pLits, int nLits ) +{ + int i, iLitFail = -1; + lbool status; + assert( nLits > 0 ); + // help the SAT solver by setting desirable polarity + sat_solver3_set_literal_polarity( s, pLits, nLits ); + // check if there exists a satisfying assignment + status = sat_solver3_solve_internal( s ); + if ( status != l_True ) // no assignment + return status; + // there is at least one satisfying assignment + assert( status == l_True ); + // find the first mismatching literal + for ( i = 0; i < nLits; i++ ) + if ( pLits[i] != sat_solver3_var_literal(s, Abc_Lit2Var(pLits[i])) ) + break; + if ( i == nLits ) // no mismatch - the current assignment is the minimum one! + return l_True; + // mismatch happens in literal i + iLitFail = i; + // create assumptions up to this literal (as in pLits) - including this literal! + for ( i = 0; i <= iLitFail; i++ ) + if ( !sat_solver3_push(s, pLits[i]) ) // can become UNSAT while adding the last assumption + break; + if ( i < iLitFail + 1 ) // the solver became UNSAT while adding assumptions + status = l_False; + else // solve under the assumptions + status = sat_solver3_solve_internal( s ); + if ( status == l_True ) + { + // we proved that there is a sat assignment with literal (iLitFail) having polarity as in pLits + // continue solving recursively + if ( iLitFail + 1 < nLits ) + status = sat_solver3_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 ); + } + else if ( status == l_False ) + { + // we proved that there is no assignment with iLitFail having polarity as in pLits + assert( Abc_LitIsCompl(pLits[iLitFail]) ); // literal is 0 + // (this assert may fail only if there is a sat assignment smaller than one originally given in pLits) + // now we flip this literal (make it 1), change the last assumption + // and contiue looking for the 000...0-assignment of other literals + sat_solver3_pop( s ); + pLits[iLitFail] = Abc_LitNot(pLits[iLitFail]); + if ( !sat_solver3_push(s, pLits[iLitFail]) ) + printf( "sat_solver3_solve_lexsat(): A satisfying assignment should exist.\n" ); // because we know that the problem is satisfiable + // update other literals to be 000...0 + for ( i = iLitFail + 1; i < nLits; i++ ) + pLits[i] = Abc_LitNot( Abc_LitRegular(pLits[i]) ); + // continue solving recursively + if ( iLitFail + 1 < nLits ) + status = sat_solver3_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 ); + else + status = l_True; + } + // undo the assumptions + for ( i = iLitFail; i >= 0; i-- ) + sat_solver3_pop( s ); + return status; +} + +// This procedure is called on a set of assumptions to minimize their number. +// The procedure relies on the fact that the current set of assumptions is UNSAT. +// It receives and returns SAT solver without assumptions. It returns the number +// of assumptions after minimization. The set of assumptions is returned in pLits. +int sat_solver3_minimize_assumptions( sat_solver3* s, int * pLits, int nLits, int nConfLimit ) +{ + int i, k, nLitsL, nLitsR, nResL, nResR; + if ( nLits == 1 ) + { + // since the problem is UNSAT, we will try to solve it without assuming the last literal + // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed + int status = l_False; + int Temp = s->nConfLimit; + s->nConfLimit = nConfLimit; + status = sat_solver3_solve_internal( s ); + s->nConfLimit = Temp; + return (int)(status != l_False); // return 1 if the problem is not UNSAT + } + assert( nLits >= 2 ); + nLitsL = nLits / 2; + nLitsR = nLits - nLitsL; + // assume the left lits + for ( i = 0; i < nLitsL; i++ ) + if ( !sat_solver3_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver3_pop(s); + return sat_solver3_minimize_assumptions( s, pLits, i+1, nConfLimit ); + } + // solve for the right lits + nResL = sat_solver3_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit ); + for ( i = 0; i < nLitsL; i++ ) + sat_solver3_pop(s); + // swap literals +// assert( nResL <= nLitsL ); +// for ( i = 0; i < nResL; i++ ) +// ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); + veci_resize( &s->temp_clause, 0 ); + for ( i = 0; i < nLitsL; i++ ) + veci_push( &s->temp_clause, pLits[i] ); + for ( i = 0; i < nResL; i++ ) + pLits[i] = pLits[nLitsL+i]; + for ( i = 0; i < nLitsL; i++ ) + pLits[nResL+i] = veci_begin(&s->temp_clause)[i]; + // assume the right lits + for ( i = 0; i < nResL; i++ ) + if ( !sat_solver3_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver3_pop(s); + return sat_solver3_minimize_assumptions( s, pLits, i+1, nConfLimit ); + } + // solve for the left lits + nResR = sat_solver3_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit ); + for ( i = 0; i < nResL; i++ ) + sat_solver3_pop(s); + return nResL + nResR; +} + +// This is a specialized version of the above procedure with several custom changes: +// - makes sure that at least one of the marked literals is preserved in the clause +// - sets literals to zero when they do not have to be used +// - sets literals to zero for disproved variables +int sat_solver3_minimize_assumptions2( sat_solver3* s, int * pLits, int nLits, int nConfLimit ) +{ + int i, k, nLitsL, nLitsR, nResL, nResR; + if ( nLits == 1 ) + { + // since the problem is UNSAT, we will try to solve it without assuming the last literal + // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed + int RetValue = 1, LitNot = Abc_LitNot(pLits[0]); + int status = l_False; + int Temp = s->nConfLimit; + s->nConfLimit = nConfLimit; + + RetValue = sat_solver3_push( s, LitNot ); assert( RetValue ); + status = sat_solver3_solve_internal( s ); + sat_solver3_pop( s ); + + // if the problem is UNSAT, add clause + if ( status == l_False ) + { + RetValue = sat_solver3_addclause( s, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + + s->nConfLimit = Temp; + return (int)(status != l_False); // return 1 if the problem is not UNSAT + } + assert( nLits >= 2 ); + nLitsL = nLits / 2; + nLitsR = nLits - nLitsL; + // assume the left lits + for ( i = 0; i < nLitsL; i++ ) + if ( !sat_solver3_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver3_pop(s); + + // add clauses for these literal + for ( k = i+1; k > nLitsL; k++ ) + { + int LitNot = Abc_LitNot(pLits[i]); + int RetValue = sat_solver3_addclause( s, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + + return sat_solver3_minimize_assumptions2( s, pLits, i+1, nConfLimit ); + } + // solve for the right lits + nResL = sat_solver3_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit ); + for ( i = 0; i < nLitsL; i++ ) + sat_solver3_pop(s); + // swap literals +// assert( nResL <= nLitsL ); + veci_resize( &s->temp_clause, 0 ); + for ( i = 0; i < nLitsL; i++ ) + veci_push( &s->temp_clause, pLits[i] ); + for ( i = 0; i < nResL; i++ ) + pLits[i] = pLits[nLitsL+i]; + for ( i = 0; i < nLitsL; i++ ) + pLits[nResL+i] = veci_begin(&s->temp_clause)[i]; + // assume the right lits + for ( i = 0; i < nResL; i++ ) + if ( !sat_solver3_push(s, pLits[i]) ) + { + for ( k = i; k >= 0; k-- ) + sat_solver3_pop(s); + + // add clauses for these literal + for ( k = i+1; k > nResL; k++ ) + { + int LitNot = Abc_LitNot(pLits[i]); + int RetValue = sat_solver3_addclause( s, &LitNot, &LitNot+1 ); + assert( RetValue ); + } + + return sat_solver3_minimize_assumptions2( s, pLits, i+1, nConfLimit ); + } + // solve for the left lits + nResR = sat_solver3_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit ); + for ( i = 0; i < nResL; i++ ) + sat_solver3_pop(s); + return nResL + nResR; +} + + + +int sat_solver3_nvars(sat_solver3* s) +{ + return s->size; +} + + +int sat_solver3_nclauses(sat_solver3* s) +{ + return s->stats.clauses; +} + + +int sat_solver3_nconflicts(sat_solver3* s) +{ + return (int)s->stats.conflicts; +} + + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bsat/satSolver3.h b/src/sat/bsat/satSolver3.h new file mode 100644 index 00000000..2d2e7ded --- /dev/null +++ b/src/sat/bsat/satSolver3.h @@ -0,0 +1,622 @@ +/************************************************************************************************** +MiniSat -- Copyright (c) 2005, Niklas Sorensson +http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/ + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko + +#ifndef ABC__sat__bsat__satSolver3_h +#define ABC__sat__bsat__satSolver3_h + + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> + +#include "satVec.h" +#include "satClause.h" +#include "misc/util/utilDouble.h" + +ABC_NAMESPACE_HEADER_START + +//================================================================================================= +// Public interface: + +struct sat_solver3_t; +typedef struct sat_solver3_t sat_solver3; + +extern sat_solver3* sat_solver3_new(void); +extern sat_solver3* zsat_solver3_new_seed(double seed); +extern void sat_solver3_delete(sat_solver3* s); + +extern int sat_solver3_addclause(sat_solver3* s, lit* begin, lit* end); +extern int sat_solver3_clause_new(sat_solver3* s, lit* begin, lit* end, int learnt); +extern int sat_solver3_simplify(sat_solver3* s); +extern int sat_solver3_solve(sat_solver3* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); +extern int sat_solver3_solve_internal(sat_solver3* s); +extern int sat_solver3_solve_lexsat(sat_solver3* s, int * pLits, int nLits); +extern int sat_solver3_minimize_assumptions( sat_solver3* s, int * pLits, int nLits, int nConfLimit ); +extern int sat_solver3_minimize_assumptions2( sat_solver3* s, int * pLits, int nLits, int nConfLimit ); +extern int sat_solver3_push(sat_solver3* s, int p); +extern void sat_solver3_pop(sat_solver3* s); +extern void sat_solver3_set_resource_limits(sat_solver3* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); +extern void sat_solver3_restart( sat_solver3* s ); +extern void zsat_solver3_restart_seed( sat_solver3* s, double seed ); +extern void sat_solver3_rollback( sat_solver3* s ); + +extern int sat_solver3_nvars(sat_solver3* s); +extern int sat_solver3_nclauses(sat_solver3* s); +extern int sat_solver3_nconflicts(sat_solver3* s); +extern double sat_solver3_memory(sat_solver3* s); +extern int sat_solver3_count_assigned(sat_solver3* s); + +extern void sat_solver3_setnvars(sat_solver3* s,int n); +extern int sat_solver3_get_var_value(sat_solver3* s, int v); +extern void sat_solver3_set_var_activity(sat_solver3* s, int * pVars, int nVars); + +extern void sat_solver3WriteDimacs( sat_solver3 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars ); +extern void sat_solver3PrintStats( FILE * pFile, sat_solver3 * p ); +extern int * sat_solver3GetModel( sat_solver3 * p, int * pVars, int nVars ); +extern void sat_solver3DoubleClauses( sat_solver3 * p, int iVar ); + +// trace recording +extern void sat_solver3TraceStart( sat_solver3 * pSat, char * pName ); +extern void sat_solver3TraceStop( sat_solver3 * pSat ); +extern void sat_solver3TraceWrite( sat_solver3 * pSat, int * pBeg, int * pEnd, int fRoot ); + +// clause storage +extern void sat_solver3_store_alloc( sat_solver3 * s ); +extern void sat_solver3_store_write( sat_solver3 * s, char * pFileName ); +extern void sat_solver3_store_free( sat_solver3 * s ); +extern void sat_solver3_store_mark_roots( sat_solver3 * s ); +extern void sat_solver3_store_mark_clauses_a( sat_solver3 * s ); +extern void * sat_solver3_store_release( sat_solver3 * s ); + +//================================================================================================= +// Solver representation: + +//struct clause_t; +//typedef struct clause_t clause; + +struct varinfo_t; +typedef struct varinfo_t varinfo; + +struct sat_solver3_t +{ + int size; // nof variables + int cap; // size of varmaps + int qhead; // Head index of queue. + int qtail; // Tail index of queue. + + // clauses + Sat_Mem_t Mem; + int hLearnts; // the first learnt clause + int hBinary; // the special binary clause + clause * binary; + veci* wlists; // watcher lists + + // rollback + int iVarPivot; // the pivot for variables + int iTrailPivot; // the pivot for trail + int hProofPivot; // the pivot for proof records + + // activities + int VarActType; + int ClaActType; + word var_inc; // Amount to bump next variable with. + word var_inc2; // Amount to bump next variable with. + word var_decay; // INVERSE decay factor for variable activity: stores 1/decay. + word* activity; // A heuristic measurement of the activity of a variable. + word* activity2; // backup variable activity + unsigned cla_inc; // Amount to bump next clause with. + unsigned cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + veci act_clas; // contain clause activities + + char * pFreqs; // how many times this variable was assigned a value + int nVarUsed; + +// varinfo * vi; // variable information + int* levels; // + char* assigns; // Current values of variables. + char* polarity; // + char* tags; // + char* loads; // + + int* orderpos; // Index in variable order. + int* reasons; // + lit* trail; + veci tagged; // (contains: var) + veci stack; // (contains: var) + + veci order; // Variable order. (heap) (contains: var) + veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) +// veci model; // If problem is solved, this vector contains the model (contains: lbool). + int * model; // If problem is solved, this vector contains the model (contains: lbool). + veci conf_final; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. + + int root_level; // Level of first proper decision. + int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. + int simpdb_props; // Number of propagations before next 'simplifyDB()'. + double random_seed; + double progress_estimate; + int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything + int fVerbose; + + stats_t stats; + int nLearntMax; // max number of learned clauses + int nLearntStart; // starting learned clause limit + int nLearntDelta; // delta of learned clause limit + int nLearntRatio; // ratio percentage of learned clauses + int nDBreduces; // number of DB reductions + + ABC_INT64_T nConfLimit; // external limit on the number of conflicts + ABC_INT64_T nInsLimit; // external limit on the number of implications + abctime nRuntimeLimit; // external limit on runtime + + veci act_vars; // variables whose activity has changed + double* factors; // the activity factors + int nRestarts; // the number of local restarts + int nCalls; // the number of local restarts + int nCalls2; // the number of local restarts + veci unit_lits; // variables whose activity has changed + veci pivot_vars; // pivot variables + + int fSkipSimplify; // set to one to skip simplification of the clause database + int fNotUseRandom; // do not allow random decisions with a fixed probability + int fNoRestarts; // disables periodic restarts + + int * pGlobalVars; // for experiments with global vars during interpolation + // clause store + void * pStore; + int fSolved; + + // trace recording + FILE * pFile; + int nClauses; + int nRoots; + + veci temp_clause; // temporary storage for a CNF clause + + // CNF loading + void * pCnfMan; // external CNF manager + int(*pCnfFunc)(void * p, int); // external callback +}; + +static inline clause * clause_read( sat_solver3 * s, cla h ) +{ + return Sat_MemClauseHand( &s->Mem, h ); +} + +static int sat_solver3_var_value( sat_solver3* s, int v ) +{ + assert( v >= 0 && v < s->size ); + return (int)(s->model[v] == l_True); +} +static int sat_solver3_var_literal( sat_solver3* s, int v ) +{ + assert( v >= 0 && v < s->size ); + return toLitCond( v, s->model[v] != l_True ); +} +static void sat_solver3_act_var_clear(sat_solver3* s) +{ + int i; + if ( s->VarActType == 0 ) + { + for (i = 0; i < s->size; i++) + s->activity[i] = (1 << 10); + s->var_inc = (1 << 5); + } + else if ( s->VarActType == 1 ) + { + for (i = 0; i < s->size; i++) + s->activity[i] = 0; + s->var_inc = 1; + } + else if ( s->VarActType == 2 ) + { + for (i = 0; i < s->size; i++) + s->activity[i] = Xdbl_Const1(); + s->var_inc = Xdbl_Const1(); + } + else assert(0); +} +static void sat_solver3_compress(sat_solver3* s) +{ + if ( s->qtail != s->qhead ) + { + int RetValue = sat_solver3_simplify(s); + assert( RetValue != 0 ); + (void) RetValue; + } +} +static void sat_solver3_delete_p( sat_solver3 ** ps ) +{ + if ( *ps ) + sat_solver3_delete( *ps ); + *ps = NULL; +} +static void sat_solver3_clean_polarity(sat_solver3* s, int * pVars, int nVars ) +{ + int i; + for ( i = 0; i < nVars; i++ ) + s->polarity[pVars[i]] = 0; +} +static void sat_solver3_set_polarity(sat_solver3* s, int * pVars, int nVars ) +{ + int i; + for ( i = 0; i < s->size; i++ ) + s->polarity[i] = 0; + for ( i = 0; i < nVars; i++ ) + s->polarity[pVars[i]] = 1; +} +static void sat_solver3_set_literal_polarity(sat_solver3* s, int * pLits, int nLits ) +{ + int i; + for ( i = 0; i < nLits; i++ ) + s->polarity[Abc_Lit2Var(pLits[i])] = !Abc_LitIsCompl(pLits[i]); +} + +static int sat_solver3_final(sat_solver3* s, int ** ppArray) +{ + *ppArray = s->conf_final.ptr; + return s->conf_final.size; +} + +static abctime sat_solver3_set_runtime_limit(sat_solver3* s, abctime Limit) +{ + abctime nRuntimeLimit = s->nRuntimeLimit; + s->nRuntimeLimit = Limit; + return nRuntimeLimit; +} + +static int sat_solver3_set_random(sat_solver3* s, int fNotUseRandom) +{ + int fNotUseRandomOld = s->fNotUseRandom; + s->fNotUseRandom = fNotUseRandom; + return fNotUseRandomOld; +} + +static inline void sat_solver3_bookmark(sat_solver3* s) +{ + assert( s->qhead == s->qtail ); + s->iVarPivot = s->size; + s->iTrailPivot = s->qhead; + Sat_MemBookMark( &s->Mem ); + if ( s->activity2 ) + { + s->var_inc2 = s->var_inc; + memcpy( s->activity2, s->activity, sizeof(word) * s->iVarPivot ); + } +} +static inline void sat_solver3_set_pivot_variables( sat_solver3* s, int * pPivots, int nPivots ) +{ + s->pivot_vars.cap = nPivots; + s->pivot_vars.size = nPivots; + s->pivot_vars.ptr = pPivots; +} +static inline int sat_solver3_count_usedvars(sat_solver3* s) +{ + int i, nVars = 0; + for ( i = 0; i < s->size; i++ ) + if ( s->pFreqs[i] ) + { + s->pFreqs[i] = 0; + nVars++; + } + return nVars; +} + +static inline int sat_solver3_add_const( sat_solver3 * pSat, int iVar, int fCompl ) +{ + lit Lits[1]; + int Cid; + assert( iVar >= 0 ); + + Lits[0] = toLitCond( iVar, fCompl ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 1 ); + assert( Cid ); + return 1; +} +static inline int sat_solver3_add_buffer( sat_solver3 * pSat, int iVarA, int iVarB, int fCompl ) +{ + lit Lits[2]; + int Cid; + assert( iVarA >= 0 && iVarB >= 0 ); + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVarB, !fCompl ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 ); + if ( Cid == 0 ) + return 0; + assert( Cid ); + + Lits[0] = toLitCond( iVarA, 1 ); + Lits[1] = toLitCond( iVarB, fCompl ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 ); + if ( Cid == 0 ) + return 0; + assert( Cid ); + return 2; +} +static inline int sat_solver3_add_buffer_enable( sat_solver3 * pSat, int iVarA, int iVarB, int iVarEn, int fCompl ) +{ + lit Lits[3]; + int Cid; + assert( iVarA >= 0 && iVarB >= 0 && iVarEn >= 0 ); + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVarB, !fCompl ); + Lits[2] = toLitCond( iVarEn, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarA, 1 ); + Lits[1] = toLitCond( iVarB, fCompl ); + Lits[2] = toLitCond( iVarEn, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + return 2; +} +static inline int sat_solver3_add_and( sat_solver3 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ) +{ + lit Lits[3]; + int Cid; + + Lits[0] = toLitCond( iVar, !fCompl ); + Lits[1] = toLitCond( iVar0, fCompl0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = toLitCond( iVar, !fCompl ); + Lits[1] = toLitCond( iVar1, fCompl1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = toLitCond( iVar, fCompl ); + Lits[1] = toLitCond( iVar0, !fCompl0 ); + Lits[2] = toLitCond( iVar1, !fCompl1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + return 3; +} +static inline int sat_solver3_add_xor( sat_solver3 * pSat, int iVarA, int iVarB, int iVarC, int fCompl ) +{ + lit Lits[3]; + int Cid; + assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 ); + + Lits[0] = toLitCond( iVarA, !fCompl ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarA, !fCompl ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarA, fCompl ); + Lits[1] = toLitCond( iVarB, 1 ); + Lits[2] = toLitCond( iVarC, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarA, fCompl ); + Lits[1] = toLitCond( iVarB, 0 ); + Lits[2] = toLitCond( iVarC, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + return 4; +} +static inline int sat_solver3_add_mux( sat_solver3 * pSat, int iVarZ, int iVarC, int iVarT, int iVarE, int iComplC, int iComplT, int iComplE, int iComplZ ) +{ + lit Lits[3]; + int Cid; + assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 ); + + Lits[0] = toLitCond( iVarC, 1 ^ iComplC ); + Lits[1] = toLitCond( iVarT, 1 ^ iComplT ); + Lits[2] = toLitCond( iVarZ, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarC, 1 ^ iComplC ); + Lits[1] = toLitCond( iVarT, 0 ^ iComplT ); + Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarC, 0 ^ iComplC ); + Lits[1] = toLitCond( iVarE, 1 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarC, 0 ^ iComplC ); + Lits[1] = toLitCond( iVarE, 0 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + if ( iVarT == iVarE ) + return 4; + + Lits[0] = toLitCond( iVarT, 0 ^ iComplT ); + Lits[1] = toLitCond( iVarE, 0 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 1 ^ iComplZ ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarT, 1 ^ iComplT ); + Lits[1] = toLitCond( iVarE, 1 ^ iComplE ); + Lits[2] = toLitCond( iVarZ, 0 ^ iComplZ ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + return 6; +} +static inline int sat_solver3_add_mux41( sat_solver3 * pSat, int iVarZ, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3 ) +{ + lit Lits[4]; + int Cid; + assert( iVarC0 >= 0 && iVarC1 >= 0 && iVarD0 >= 0 && iVarD1 >= 0 && iVarD2 >= 0 && iVarD3 >= 0 && iVarZ >= 0 ); + + Lits[0] = toLitCond( iVarD0, 1 ); + Lits[1] = toLitCond( iVarC0, 0 ); + Lits[2] = toLitCond( iVarC1, 0 ); + Lits[3] = toLitCond( iVarZ, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarD1, 1 ); + Lits[1] = toLitCond( iVarC0, 1 ); + Lits[2] = toLitCond( iVarC1, 0 ); + Lits[3] = toLitCond( iVarZ, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarD2, 1 ); + Lits[1] = toLitCond( iVarC0, 0 ); + Lits[2] = toLitCond( iVarC1, 1 ); + Lits[3] = toLitCond( iVarZ, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarD3, 1 ); + Lits[1] = toLitCond( iVarC0, 1 ); + Lits[2] = toLitCond( iVarC1, 1 ); + Lits[3] = toLitCond( iVarZ, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + + + Lits[0] = toLitCond( iVarD0, 0 ); + Lits[1] = toLitCond( iVarC0, 0 ); + Lits[2] = toLitCond( iVarC1, 0 ); + Lits[3] = toLitCond( iVarZ, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarD1, 0 ); + Lits[1] = toLitCond( iVarC0, 1 ); + Lits[2] = toLitCond( iVarC1, 0 ); + Lits[3] = toLitCond( iVarZ, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarD2, 0 ); + Lits[1] = toLitCond( iVarC0, 0 ); + Lits[2] = toLitCond( iVarC1, 1 ); + Lits[3] = toLitCond( iVarZ, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarD3, 0 ); + Lits[1] = toLitCond( iVarC0, 1 ); + Lits[2] = toLitCond( iVarC1, 1 ); + Lits[3] = toLitCond( iVarZ, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + return 8; +} +static inline int sat_solver3_add_xor_and( sat_solver3 * pSat, int iVarF, int iVarA, int iVarB, int iVarC ) +{ + // F = (a (+) b) * c + lit Lits[4]; + int Cid; + assert( iVarF >= 0 && iVarA >= 0 && iVarB >= 0 && iVarC >= 0 ); + + Lits[0] = toLitCond( iVarF, 1 ); + Lits[1] = toLitCond( iVarA, 1 ); + Lits[2] = toLitCond( iVarB, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarF, 1 ); + Lits[1] = toLitCond( iVarA, 0 ); + Lits[2] = toLitCond( iVarB, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarF, 1 ); + Lits[1] = toLitCond( iVarC, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarF, 0 ); + Lits[1] = toLitCond( iVarA, 1 ); + Lits[2] = toLitCond( iVarB, 0 ); + Lits[3] = toLitCond( iVarC, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarF, 0 ); + Lits[1] = toLitCond( iVarA, 0 ); + Lits[2] = toLitCond( iVarB, 1 ); + Lits[3] = toLitCond( iVarC, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 4 ); + assert( Cid ); + return 5; +} +static inline int sat_solver3_add_constraint( sat_solver3 * pSat, int iVar, int iVar2, int fCompl ) +{ + lit Lits[2]; + int Cid; + assert( iVar >= 0 ); + + Lits[0] = toLitCond( iVar, fCompl ); + Lits[1] = toLitCond( iVar2, 0 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = toLitCond( iVar, fCompl ); + Lits[1] = toLitCond( iVar2, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 ); + assert( Cid ); + return 2; +} + +static inline int sat_solver3_add_half_sorter( sat_solver3 * pSat, int iVarA, int iVarB, int iVar0, int iVar1 ) +{ + lit Lits[3]; + int Cid; + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVar0, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarA, 0 ); + Lits[1] = toLitCond( iVar1, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 2 ); + assert( Cid ); + + Lits[0] = toLitCond( iVarB, 0 ); + Lits[1] = toLitCond( iVar0, 1 ); + Lits[2] = toLitCond( iVar1, 1 ); + Cid = sat_solver3_addclause( pSat, Lits, Lits + 3 ); + assert( Cid ); + return 3; +} + + +ABC_NAMESPACE_HEADER_END + +#endif |