Skip to content

A
abc
Commit c1b4b79e by Alan Mishchenko
Options

Integrating Glucose into &qbf.

parent 1e1d41f3
Showing with 46 additions and 18 deletions
src/aig/gia/giaQbf.c
......@@ -22,6 +22,7 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "misc/extra/extra.h"
#include "sat/glucose/AbcGlucose.h"
ABC_NAMESPACE_IMPL_START
......@@ -41,6 +42,7 @@ struct Qbf_Man_t_
int iParVarBeg; // SAT var ID of the first par variable in the ver solver
sat_solver * pSatVer; // verification instance
sat_solver * pSatSyn; // synthesis instance
bmcg_sat_solver*pSatSynG; // synthesis instance
Vec_Int_t * vValues; // variable values
Vec_Int_t * vParMap; // parameter mapping
Vec_Int_t * vLits; // literals for the SAT solver
......@@ -284,7 +286,7 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars )
SeeAlso []
***********************************************************************/
Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose )
Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fVerbose )
{
Qbf_Man_t * p;
Cnf_Dat_t * pCnf;
......@@ -300,10 +302,12 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose )
p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
p->pSatSyn = sat_solver_new();
p->pSatSynG = fGlucose ? bmcg_sat_solver_start() : NULL;
p->vValues = Vec_IntAlloc( Gia_ManPiNum(pGia) );
p->vParMap = Vec_IntStartFull( nPars );
p->vLits = Vec_IntAlloc( nPars );
sat_solver_setnvars( p->pSatSyn, nPars );
if ( p->pSatSynG ) bmcg_sat_solver_set_nvars( p->pSatSynG, nPars );
Cnf_DataFree( pCnf );
return p;
}
......@@ -311,6 +315,7 @@ void Gia_QbfFree( Qbf_Man_t * p )
{
sat_solver_delete( p->pSatVer );
sat_solver_delete( p->pSatSyn );
if ( p->pSatSynG ) bmcg_sat_solver_stop( p->pSatSynG );
Vec_IntFree( p->vLits );
Vec_IntFree( p->vValues );
Vec_IntFree( p->vParMap );
......@@ -481,6 +486,21 @@ int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof )
return 0;
return 1;
}
int Gia_QbfAddCofactorG( Qbf_Man_t * p, Gia_Man_t * pCof )
{
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 );
int i, iFirstVar = pCnf->nVars - Gia_ManPiNum(pCof); //-1
pCnf->pMan = NULL;
Cnf_SpecialDataLift( pCnf, bmcg_sat_solver_varnum(p->pSatSynG), iFirstVar, iFirstVar + Gia_ManPiNum(p->pGia) );
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !bmcg_sat_solver_addclause( p->pSatSynG, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
{
Cnf_DataFree( pCnf );
return 0;
}
Cnf_DataFree( pCnf );
return 1;
}
/**Function*************************************************************
......@@ -498,16 +518,16 @@ void Gia_QbfOnePattern( Qbf_Man_t * p, Vec_Int_t * vValues )
int i;
Vec_IntClear( vValues );
for ( i = 0; i < p->nPars; i++ )
Vec_IntPush( vValues, sat_solver_var_value(p->pSatSyn, i) );
Vec_IntPush( vValues, p->pSatSynG ? bmcg_sat_solver_read_cex_varvalue(p->pSatSynG, i) : sat_solver_var_value(p->pSatSyn, i) );
}
void Gia_QbfPrint( Qbf_Man_t * p, Vec_Int_t * vValues, int Iter )
{
printf( "%5d : ", Iter );
assert( Vec_IntSize(vValues) == p->nVars );
Vec_IntPrintBinary( vValues ); printf( " " );
printf( "Var = %6d ", sat_solver_nvars(p->pSatSyn) );
printf( "Cla = %6d ", sat_solver_nclauses(p->pSatSyn) );
printf( "Conf = %6d ", sat_solver_nconflicts(p->pSatSyn) );
printf( "Var = %6d ", p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) );
printf( "Cla = %6d ", p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) );
printf( "Conf = %6d ", p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
......@@ -601,9 +621,9 @@ void Gia_QbfLearnConstraint( Qbf_Man_t * p, Vec_Int_t * vValues )
SeeAlso []
***********************************************************************/
int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fVerbose )
int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fGlucose, int fVerbose )
{
Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fVerbose );
Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fVerbose );
Gia_Man_t * pCof;
int i, status, RetValue = 0;
abctime clk;
......@@ -618,12 +638,15 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
// generate next constraint
assert( Vec_IntSize(p->vValues) == p->nVars );
pCof = Gia_QbfCofactor( pGia, nPars, p->vValues, p->vParMap );
status = Gia_QbfAddCofactor( p, pCof );
status = p->pSatSynG ? Gia_QbfAddCofactorG( p, pCof ) : Gia_QbfAddCofactor( p, pCof );
Gia_ManStop( pCof );
if ( status == 0 ) { RetValue = 1; break; }
// synthesize next assignment
clk = Abc_Clock();
status = sat_solver_solve( p->pSatSyn, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
if ( p->pSatSynG )
status = bmcg_sat_solver_solve( p->pSatSynG, NULL, 0 );
else
status = sat_solver_solve( p->pSatSyn, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
p->clkSat += Abc_Clock() - clk;
if ( fVerbose )
Gia_QbfPrint( p, p->vValues, i );
......
src/base/abci/abc.c
......@@ -25173,7 +25173,7 @@ usage:
Abc_Print( -2, "\t-u : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "not" );
Abc_Print( -2, "\t-r : toggle disabling periodic restarts [default = %s]\n", pPars->fNoRestarts? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using Satoko instead of build-in MiniSAT [default = %s]\n", pPars->fUseSatoko? "yes": "no" );
Abc_Print( -2, "\t-g : toggle using Glucose instead of build-in MiniSAT [default = %s]\n",pPars->fUseGlucose? "yes": "no" );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n",pPars->fUseGlucose? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
......@@ -40402,7 +40402,7 @@ usage:
Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd );
Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 [default = %s]\n", pPars->fUseGlucose? "Glucose" : "Satoko" );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fUseGlucose? "Glucose" : "Satoko" );
Abc_Print( -2, "\t-e : toggle using variable eliminatation [default = %s]\n", pPars->fUseEliminate?"yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
......@@ -41017,15 +41017,16 @@ usage:
int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars );
extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fVerbose );
extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fGlucose, int fVerbose );
int c, nPars = -1;
int nIterLimit = 0;
int nConfLimit = 0;
int nTimeOut = 0;
int fDumpCnf = 0;
int fGlucose = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PICTdvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PICTdgvh" ) ) != EOF )
{
switch ( c )
{
......@@ -41076,6 +41077,9 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDumpCnf ^= 1;
break;
case 'g':
fGlucose ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -41108,17 +41112,18 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fDumpCnf )
Gia_QbfDumpFile( pAbc->pGia, nPars );
else
Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, fVerbose );
Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, fGlucose, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &qbf [-PICT num] [-dvh]\n" );
Abc_Print( -2, "usage: &qbf [-PICT num] [-dgvh]\n" );
Abc_Print( -2, "\t solves QBF problem EpVxM(p,x)\n" );
Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars );
Abc_Print( -2, "\t-I num : quit after the given iteration even if unsolved [default = %d]\n", nIterLimit );
Abc_Print( -2, "\t-C num : conflict limit per problem [default = %d]\n", nConfLimit );
Abc_Print( -2, "\t-T num : global timeout [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-d : toggle dumping QDIMACS file instead of solving [default = %s]\n", fDumpCnf? "yes": "no" );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", fGlucose? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
src/sat/glucose/AbcGlucose.cpp
......@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver Glucose 3.0.]
PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.]
Synopsis [Interface to Glucose.]
......
src/sat/glucose/AbcGlucose.h
......@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver Glucose 3.0.]
PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.]
Synopsis [Interface to Glucose.]
......
src/sat/glucose/AbcGlucoseCmd.cpp
......@@ -4,7 +4,7 @@
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT solver Glucose 3.0.]
PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.]
Synopsis [Interface to Glucose.]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment