From 89d4ac502908d4b41edaccfb858fef584374728d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 12 Apr 2016 19:44:21 -0700 Subject: Adding new implementation of LEXSAT. --- src/sat/bmc/bmcClp.c | 7 ++++- src/sat/bsat/satSolver.c | 68 ++++++++++++++++++++++++++++++++++++++++++++++++ src/sat/bsat/satSolver.h | 1 + 3 files changed, 75 insertions(+), 1 deletion(-) (limited to 'src') diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index eb924123..8a69fe56 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -592,7 +592,7 @@ int Bmc_CollapseExpand2( sat_solver * pSat, sat_solver * pSatOn, Vec_Int_t * vLi SeeAlso [] ***********************************************************************/ -int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit ) +int Bmc_ComputeCanonical2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit ) { int i, k, iLit, status = l_Undef; for ( i = 0; i < Vec_IntSize(vLits); i++ ) @@ -621,6 +621,11 @@ int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTem assert( status == l_True ); return status; } +int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTemp, int nBTLimit ) +{ + sat_solver_set_resource_limits( pSat, nBTLimit, 0, 0, 0 ); + return sat_solver_solve_lexsat( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) ); +} /**Function************************************************************* diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index ba5834f9..b9ab0740 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -1885,6 +1885,74 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit 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_solver_solve_lexsat( sat_solver* s, int * pLits, int nLits ) +{ + int i, iLitFail = -1; + lbool status; + assert( nLits > 0 ); + // help the SAT solver by setting desirable polarity + sat_solver_set_literal_polarity( s, pLits, nLits ); + // check if there exists a satisfying assignment + status = sat_solver_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_solver_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_solver_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_solver_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_solver_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_solver_pop( s ); + pLits[iLitFail] = Abc_LitNot(pLits[iLitFail]); + if ( !sat_solver_push(s, pLits[iLitFail]) ) + printf( "sat_solver_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_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 ); + else + status = l_True; + } + // undo the assumptions + for ( i = iLitFail; i >= 0; i-- ) + sat_solver_pop( s ); + return status; +} + int sat_solver_nvars(sat_solver* s) { diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 401ac213..e729d2c8 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -49,6 +49,7 @@ extern int sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, in extern int sat_solver_simplify(sat_solver* s); extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); extern int sat_solver_solve_internal(sat_solver* s); +extern int sat_solver_solve_lexsat(sat_solver* s, int * pLits, int nLits); extern int sat_solver_push(sat_solver* s, int p); extern void sat_solver_pop(sat_solver* s); extern void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); -- cgit v1.2.3