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

Merge pull request #443 from MyskYko/fix4 

QBF using CaDiCaL
This commit is contained in:
alanminko 2025-11-06 12:46:13 -08:00 committed by GitHub
parent cb971e07a3 13205ccbb3
commit 3109172462
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
8 changed files with 101 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
src/aig/gia/giaQbf.c
View File

@ -23,6 +23,7 @@
#include "sat/bsat/satStore.h"
#include "misc/extra/extra.h"
#include "sat/glucose/AbcGlucose.h"
#include "sat/cadical/cadicalSolver.h"
#include "misc/util/utilTruth.h"
#include "base/io/ioResub.h"
@ -45,6 +46,7 @@ struct Qbf_Man_t_
sat_solver * pSatVer; // verification instance
sat_solver * pSatSyn; // synthesis instance
bmcg_sat_solver*pSatSynG; // synthesis instance
cadical_solver* pSatSynC; // synthesis instance
Vec_Int_t * vValues; // variable values
Vec_Int_t * vParMap; // parameter mapping
Vec_Int_t * vLits; // literals for the SAT solver
@ -534,7 +536,7 @@ void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars )
SeeAlso []
***********************************************************************/
Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fVerbose )
Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fCadical, int fVerbose )
{
Qbf_Man_t * p;
Cnf_Dat_t * pCnf;
@ -551,11 +553,13 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fVerbos
p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
p->pSatSyn = sat_solver_new();
p->pSatSynG = fGlucose ? bmcg_sat_solver_start() : NULL;
p->pSatSynC = fCadical ? cadical_solver_new() : 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 );
if ( p->pSatSynC ) cadical_solver_setnvars( p->pSatSynC, nPars );
Cnf_DataFree( pCnf );
return p;
}
@ -564,6 +568,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 );
if ( p->pSatSynC ) cadical_solver_delete( p->pSatSynC );
Vec_IntFree( p->vLits );
Vec_IntFree( p->vValues );
Vec_IntFree( p->vParMap );
@ -749,6 +754,21 @@ int Gia_QbfAddCofactorG( Qbf_Man_t * p, Gia_Man_t * pCof )
Cnf_DataFree( pCnf );
return 1;
}
int Gia_QbfAddCofactorC( 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, cadical_solver_nvars(p->pSatSynC), iFirstVar, iFirstVar + Gia_ManPiNum(p->pGia) );
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !cadical_solver_addclause( p->pSatSynC, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
{
Cnf_DataFree( pCnf );
return 0;
}
Cnf_DataFree( pCnf );
return 1;
}
/**Function*************************************************************
@ -766,16 +786,20 @@ 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, p->pSatSynG ? bmcg_sat_solver_read_cex_varvalue(p->pSatSynG, i) : sat_solver_var_value(p->pSatSyn, i) );
Vec_IntPush( vValues, p->pSatSynC ? cadical_solver_get_var_value(p->pSatSynC, i) :
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 =%7d ", p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) );
printf( "Cla =%7d ", p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) );
printf( "Conf =%9d ", p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) );
printf( "Var =%7d ", p->pSatSynC ? cadical_solver_nvars(p->pSatSynC) :
p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) );
printf( "Cla =%7d ", p->pSatSynC ? cadical_solver_nclauses(p->pSatSynC) :
p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) );
printf( "Conf =%9d ", p->pSatSynC ? cadical_solver_nconflicts(p->pSatSynC) :
p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
@ -869,9 +893,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 nEncVars, int fGlucose, int fVerbose )
int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fVerbose )
{
Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fVerbose );
Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fCadical, fVerbose );
Gia_Man_t * pCof;
int i, status, RetValue = 0;
abctime clk;
@ -886,12 +910,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 = p->pSatSynG ? Gia_QbfAddCofactorG( p, pCof ) : Gia_QbfAddCofactor( p, pCof );
status = p->pSatSynC ? Gia_QbfAddCofactorC( p, pCof ) :
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();
if ( p->pSatSynG )
if ( p->pSatSynC )
status = cadical_solver_solve( p->pSatSynC, NULL, NULL, 0, 0, 0, 0 );
else 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 );

13
src/base/abci/abc.c
View File

@ -51291,7 +51291,7 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars );
extern void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars );
extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fVerbose );
extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fVerbose );
int c, nPars = -1;
int nIterLimit = 0;
int nConfLimit = 0;
@ -51300,9 +51300,10 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
int fDumpCnf = 0;
int fDumpCnf2 = 0;
int fGlucose = 0;
int fCadical = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdegvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdegcvh" ) ) != EOF )
{
switch ( c )
{
@ -51370,6 +51371,9 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
fGlucose ^= 1;
break;
case 'c':
fCadical ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -51404,11 +51408,11 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
else if ( fDumpCnf2 )
Gia_QbfDumpFileInv( pAbc->pGia, nPars );
else
Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fVerbose );
Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fCadical, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &qbf [-PICTK num] [-degvh]\n" );
Abc_Print( -2, "usage: &qbf [-PICTK num] [-degcvh]\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 );
@ -51418,6 +51422,7 @@ usage:
Abc_Print( -2, "\t-d : toggle dumping QDIMACS file instead of solving (complemented QBF) [default = %s]\n", fDumpCnf? "yes": "no" );
Abc_Print( -2, "\t-e : toggle dumping QDIMACS file instead of solving (original QBF) [default = %s]\n", fDumpCnf2? "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-c : toggle using CaDiCaL by Armin Biere [default = %s]\n", fCadical? "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\n");
Abc_Print( -2, "\t As an example of using this command, consider specification (the three-input AND-gate) and implementation\n");

4
src/sat/cadical/cadical.hpp
View File

@ -982,6 +982,10 @@ public:
//
static void build (FILE *file, const char *prefix = "c ");
// Extra APIs
int clauses ();
int conflicts ();
private:
//==== start of state ====================================================

30
src/sat/cadical/cadicalSolver.c
View File

@ -261,6 +261,36 @@ int cadical_solver_get_var_value(cadical_solver* s, int v) {
return ccadical_val((CCaDiCaL*)s->p, v + 1) > 0;
}
/**Function*************************************************************
Synopsis [get number of clauses]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int cadical_solver_nclauses(cadical_solver* s) {
return ccadical_clauses((CCaDiCaL*)s->p);
}
/**Function*************************************************************
Synopsis [get number of conflicts]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int cadical_solver_nconflicts(cadical_solver* s) {
return ccadical_conflicts((CCaDiCaL*)s->p);
}
/**Function*************************************************************

2
src/sat/cadical/cadicalSolver.h
View File

@ -65,6 +65,8 @@ extern int cadical_solver_nvars(cadical_solver* s);
extern int cadical_solver_addvar(cadical_solver* s);
extern void cadical_solver_setnvars(cadical_solver* s,int n);
extern int cadical_solver_get_var_value(cadical_solver* s, int v);
extern int cadical_solver_nclauses(cadical_solver* s);
extern int cadical_solver_nconflicts(cadical_solver* s);
extern Vec_Int_t * cadical_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose );
ABC_NAMESPACE_HEADER_END

8
src/sat/cadical/cadical_ccadical.cpp
View File

@ -208,4 +208,12 @@ int ccadical_is_inconsistent(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->inconsistent ();
}
int ccadical_clauses(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->clauses ();
}
int ccadical_conflicts(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->conflicts ();
}
ABC_NAMESPACE_IMPL_END

10
src/sat/cadical/cadical_solver.cpp
View File

@ -1759,6 +1759,16 @@ void Solver::error (const char *fmt, ...) {
va_end (ap);
}
/*------------------------------------------------------------------------*/
int Solver::clauses () {
return internal->stats.added.total;
}
int Solver::conflicts () {
return internal->stats.conflicts;
}
} // namespace CaDiCaL
ABC_NAMESPACE_IMPL_END

2
src/sat/cadical/ccadical.h
View File

@ -58,6 +58,8 @@ int ccadical_reserve_difference (CCaDiCaL *, int number_of_vars);
void ccadical_reserve(CCaDiCaL *, int min_max_var);
int ccadical_is_inconsistent(CCaDiCaL *);
int ccadical_clauses(CCaDiCaL *);
int ccadical_conflicts(CCaDiCaL *);
/*------------------------------------------------------------------------*/