luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experiments with Glucose.

This commit is contained in:
Alan Mishchenko 2017-09-07 22:59:59 -07:00
parent 32312c43f8
commit 03e7b7209e
4 changed files with 157 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

140
src/sat/glucose/AbcGlucose.cpp
View File

@ -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<int>*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<Lit> 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");

38
src/sat/glucose/Glucose.cpp
View File

@ -224,6 +224,12 @@ bool Solver::addClause_(vec<Lit>& 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<Watcher>& ws = watches[p];
Watcher *i, *j, *end;
num_props++;
// First, Propagate binary clauses
// First, Propagate binary clauses
vec<Watcher>& wbin = watchesBin[p];
for(int k = 0;k<wbin.size();k++) {
Lit imp = wbin[k].blocker;
if(value(imp) == l_False) {
return wbin[k].cref;
}
if(value(imp) == l_Undef) {
uncheckedEnqueue(imp,wbin[k].cref);
}
}
for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){
// Try to avoid inspecting the clause:
@ -836,7 +835,6 @@ CRef Solver::propagate()
Lit first = c[0];
Watcher w = Watcher(cr, first);
if (first != blocker && value(first) == l_True){
*j++ = w; continue; }
// Look for new watch:
@ -912,40 +910,35 @@ struct reduceDB_lt {
// Main criteria... Like in MiniSat we keep all binary clauses
if(ca[x].size()> 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<CRef>& cs)
{
int i, j;
for (i = j = 0; i < cs.size(); i++){
Clause& c = ca[cs[i]];
if (satisfied(c))
removeClause(cs[i]);
else

3
src/sat/glucose/SimpSolver.cpp
View File

@ -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 );
}

3
src/sat/glucose/Solver.h
View File

@ -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<int> user_vec;
// Problem specification:
//
@ -229,7 +230,7 @@ protected:
vec<char> polarity; // The preferred polarity of each variable.
vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<int> nbpos;
vec<int> nbpos;
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
vec<VarData> 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).