From 03e7b7209ea4a8b3810a8c5ecb99d6953d0d2c07 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 7 Sep 2017 22:59:59 -0700 Subject: Experiments with Glucose. --- src/sat/glucose/AbcGlucose.cpp | 140 ++++++++++++++++++++++++++++++++++++++++- src/sat/glucose/Glucose.cpp | 38 +++++------ src/sat/glucose/SimpSolver.cpp | 3 + src/sat/glucose/Solver.h | 3 +- 4 files changed, 157 insertions(+), 27 deletions(-) diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 8e82e654..8d8868ce 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -245,6 +245,49 @@ int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s) return ((Gluco::Solver*)s)->conflicts; } +int bmcg_sat_solver_minimize_assumptions(bmcg_sat_solver * s, int * plits, int nlits) +{ + vec*array = &((Gluco::Solver*)s)->user_vec; + int i, nlitsL, nlitsR, nresL, nresR, status; + if ( nlits == 1 ) + { + // since the problem is UNSAT, we try to solve it without assuming the last literal + // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed + status = bmcg_sat_solver_solve( s, NULL, 0 ); + return status != -1; // return 1 if the problem is not UNSAT + } + assert( nlits >= 2 ); + nlitsL = nlits / 2; + nlitsR = nlits - nlitsL; + // solve with these assumptions + status = bmcg_sat_solver_solve( s, plits, nlitsL ); + if ( status == -1 ) // these are enough + return bmcg_sat_solver_minimize_assumptions( s, plits, nlitsL ); + // these are not enough + // solve for the right lits +// assume left bits + nresL = nlitsR == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits + nlitsL, nlitsR ); +// unassume left bits + // swap literals + array->clear(); + for ( i = 0; i < nlitsL; i++ ) + array->push(plits[i]); + for ( i = 0; i < nresL; i++ ) + plits[i] = plits[nlitsL+i]; + for ( i = 0; i < nlitsL; i++ ) + plits[nresL+i] = (*array)[i]; + // solve with these assumptions +// assume right bits + status = bmcg_sat_solver_solve( s, plits, nresL ); + if ( status == -1 ) // these are enough +// unassume right bits + return nresL; + // solve for the left lits + nresR = nlitsL == 1 ? 1 : bmcg_sat_solver_minimize_assumptions( s, plits + nresL, nlitsL ); +// unassume right bits + return nresL + nresR; +} + /**Function************************************************************* Synopsis [] @@ -298,7 +341,7 @@ void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars ) ***********************************************************************/ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& S ) { - //abctime clk = Abc_Clock(); + abctime clk = Abc_Clock(); int * pLit, * pStop, i; Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ ); for ( i = 0; i < pCnf->nClauses; i++ ) @@ -315,12 +358,104 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& S ) S.addClause(lits); } Vec_Int_t * vCnfIds = Vec_IntAllocArrayCopy(pCnf->pVarNums,pCnf->nVars); + printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Cnf_DataFree(pCnf); + return vCnfIds; +} + +// procedure below does not work because glucose_solver_addclause() expects Solver +Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S ) +{ + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ ); + for ( int i = 0; i < pCnf->nClauses; i++ ) + if ( !glucose_solver_addclause( &S, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) + assert( 0 ); + Vec_Int_t * vCnfIds = Vec_IntAllocArrayCopy(pCnf->pVarNums,pCnf->nVars); //printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals ); //Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Cnf_DataFree(pCnf); return vCnfIds; } + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Glucose_GenerateSop( Gia_Man_t * p ) +{ + bmcg_sat_solver * pSat[2] = { bmcg_sat_solver_start(), bmcg_sat_solver_start() }; + + // generate CNF for the on-set and off-set + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 0/*fAddOrCla*/, 0, 0/*verbose*/ ); + int i,n,nVars = Gia_ManCiNum(p); + int iFirstVar = pCnf->nVars - nVars; + assert( Gia_ManCoNum(p) == 1 ); + for ( n = 0; n < 2; n++ ) + { + int Lit = Abc_Var2Lit( 1, !n ); // output variable is 1 + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !bmcg_sat_solver_addclause( pSat[n], pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) + assert( 0 ); + if ( !bmcg_sat_solver_addclause( pSat[n], &Lit, 1 ) ) + assert( 0 ); + } + Cnf_DataFree( pCnf ); + + // generate assignments + Vec_Int_t * vLits = Vec_IntAlloc( nVars ); + Vec_Str_t * vCube = Vec_StrAlloc( nVars + 4 ); + while ( 1 ) + { + // generate onset minterm + int status = bmcg_sat_solver_solve( pSat[1], NULL, 0 ); + if ( status == -1 ) + break; + assert( status == 1 ); + Vec_IntClear( vLits ); + for ( i = 0; i < nVars; i++ ) + Vec_IntPush( vLits, Abc_Var2Lit(iFirstVar+i, !bmcg_sat_solver_read_cex_varvalue(pSat[1], iFirstVar+i)) ); + // expand it against offset + status = bmcg_sat_solver_solve( pSat[0], Vec_IntArray(vLits), Vec_IntSize(vLits) ); + assert( status == -1 ); + int * pFinal, nFinal = bmcg_sat_solver_final( pSat[0], &pFinal ); + // print cube + Vec_StrFill( vCube, nVars, '-' ); + Vec_StrPrintF( vCube, " 1\n\0" ); + for ( i = 0; i < nFinal; i++ ) + Vec_StrWriteEntry( vCube, Abc_Lit2Var(pFinal[i]) - iFirstVar, (char)('0' + Abc_LitIsCompl(pFinal[i])) ); + printf( "%s", Vec_StrArray(vCube) ); + // add blocking clause + if ( !bmcg_sat_solver_addclause( pSat[1], pFinal, nFinal ) ) + break; + } + Vec_IntFree( vLits ); + Vec_StrFree( vCube ); + + bmcg_sat_solver_stop( pSat[0] ); + bmcg_sat_solver_stop( pSat[1] ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars) { abctime clk = Abc_Clock(); @@ -329,6 +464,7 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars) S.verbosity = pPars->verb; S.verbEveryConflicts = 50000; S.showModel = false; + //S.verbosity = 2; S.setConfBudget( pPars->nConfls > 0 ? (int64_t)pPars->nConfls : -1 ); S.parsing = 1; @@ -347,7 +483,7 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars) S.eliminate(true); vec dummy; - lbool ret = S.solveLimited(dummy); + lbool ret = S.solveLimited(dummy, 0); if ( pPars->verb ) glucose_print_stats(S, Abc_Clock() - clk); printf(ret == l_True ? "SATISFIABLE" : ret == l_False ? "UNSATISFIABLE" : "INDETERMINATE"); diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index e90bf402..479f08f9 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/src/sat/glucose/Glucose.cpp @@ -224,6 +224,12 @@ bool Solver::addClause_(vec& ps) assert(decisionLevel() == 0); if (!ok) return false; + if ( 0 ) { + for ( int i = 0; i < ps.size(); i++ ) + printf( "%d ", ps[i] ); + printf( "\n" ); + } + // Check if clause is satisfied and remove false/duplicate literals: sort(ps); @@ -797,25 +803,18 @@ CRef Solver::propagate() vec& ws = watches[p]; Watcher *i, *j, *end; num_props++; - - // First, Propagate binary clauses + // First, Propagate binary clauses vec& wbin = watchesBin[p]; - for(int k = 0;k 2 && ca[y].size()==2) return 1; - if(ca[y].size()>2 && ca[x].size()==2) return 0; + if(ca[y].size()> 2 && ca[x].size()==2) return 0; if(ca[x].size()==2 && ca[y].size()==2) return 0; // Second one based on literal block distance if(ca[x].lbd()> ca[y].lbd()) return 1; if(ca[x].lbd()< ca[y].lbd()) return 0; - // Finally we can use old activity or size, we choose the last one - return ca[x].activity() < ca[y].activity(); - //return x->size() < y->size(); - - //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } + return ca[x].activity() < ca[y].activity(); + //return x->size() < y->size(); + //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); } } }; void Solver::reduceDB() -{ - - int i, j; +{ + int i, j; nbReduceDB++; sort(learnts, reduceDB_lt(ca)); // We have a lot of "good" clauses, it is difficult to compare them. Keep more ! if(ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd()<=3) nbclausesbeforereduce +=specialIncReduceDB; // Useless :-) - if(ca[learnts.last()].lbd()<=5) nbclausesbeforereduce +=specialIncReduceDB; - + if(ca[learnts.last()].lbd()<=5) nbclausesbeforereduce +=specialIncReduceDB; // Don't delete binary or locked clauses. From the rest, delete clauses from the first half // Keep clauses which seem to be usefull (their lbd was reduce during this sequence) int limit = learnts.size() / 2; - for (i = j = 0; i < learnts.size(); i++){ Clause& c = ca[learnts[i]]; if (c.lbd()>2 && c.size() > 2 && c.canBeDel() && !locked(c) && (i < limit)) { @@ -965,12 +958,9 @@ void Solver::reduceDB() void Solver::removeSatisfied(vec& cs) { - int i, j; for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; - - if (satisfied(c)) removeClause(cs[i]); else diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp index 566472fe..83d97e77 100644 --- a/src/sat/glucose/SimpSolver.cpp +++ b/src/sat/glucose/SimpSolver.cpp @@ -604,6 +604,7 @@ void SimpSolver::extendModel() bool SimpSolver::eliminate(bool turn_off_elim) { + abctime clk = Abc_Clock(); if (!simplify()) return false; else if (!use_simplification) @@ -690,6 +691,7 @@ bool SimpSolver::eliminate(bool turn_off_elim) printf("c | Eliminated clauses: %10.2f Mb |\n", double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024)); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return ok; } @@ -702,6 +704,7 @@ void SimpSolver::cleanUpClauses() if (ca[clauses[i]].mark() == 0) clauses[j++] = clauses[i]; clauses.shrink(i - j); + printf( "Simplication removed %d variables and %d clauses. ", eliminated_vars, i - j ); } diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h index dfc8f954..3a90f847 100644 --- a/src/sat/glucose/Solver.h +++ b/src/sat/glucose/Solver.h @@ -60,6 +60,7 @@ public: bool terminate_search_early; // used to stop the solver early if it as instructed by an external caller int * pstop; // another callback uint64_t nRuntimeLimit; // runtime limit + vec user_vec; // Problem specification: // @@ -229,7 +230,7 @@ protected: vec polarity; // The preferred polarity of each variable. vec decision; // Declares if a variable is eligible for selection in the decision heuristic. vec trail; // Assignment stack; stores all assigments made in the order they were made. - vec nbpos; + vec nbpos; vec trail_lim; // Separator indices for different decision levels in 'trail'. vec vardata; // Stores reason and level for each variable. int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). -- cgit v1.2.3