Skip to content

Added option -c to call CaDiCaL solver inside bmc3 engine (bmc3 -c) #507

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
alanminko merged 1 commit into from
May 15, 2026
Merged

Added option -c to call CaDiCaL solver inside bmc3 engine (bmc3 -c) #507

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion src/base/abci/abc.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30691,7 +30691,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzhc" ) ) != EOF )
{
switch ( c )
{
Expand Down Expand Up @@ -30866,6 +30866,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
pPars->fUseGlucose ^= 1;
break;
case 'c':
pPars->fUseCadical ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
Expand Down Expand Up @@ -30960,6 +30963,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -2, "\t-r : toggle disabling periodic restarts [default = %s]\n", pPars->fNoRestarts? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using Satoko by Bruno Schmitt [default = %s]\n", pPars->fUseSatoko? "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-c : toggle using CaDiCaL by Armin Biere, University of Freiburg [default = %s]\n",pPars->fUseCadical? "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");
Expand Down
1 change: 1 addition & 0 deletions src/sat/bmc/bmc.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,7 @@ struct Saig_ParBmc_t_
int fNoRestarts; // disables periodic restarts
int fUseSatoko; // enables using Satoko
int fUseGlucose; // enables using Glucose 3.0
int fUseCadical; // enables using CaDiCaL
int nLearnedStart; // starting learned clause limit
int nLearnedDelta; // delta of learned clause limit
int nLearnedPerce; // ratio of learned clause limit
Expand Down
74 changes: 63 additions & 11 deletions src/sat/bmc/bmcBmc3.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,21 @@
#include "sat/bsat/satStore.h"
#include "sat/satoko/satoko.h"
#include "sat/glucose/AbcGlucose.h"
#include "sat/cadical/cadicalSolver.h"
#include "sat/cadical/ccadical.h"
#include "misc/vec/vecHsh.h"
#include "misc/vec/vecWec.h"
#include "bmc.h"

ABC_NAMESPACE_IMPL_START

static inline void Bmc3_CadicalSetRuntimeLimit( cadical_solver * pSat4, abctime nSeconds )
{
if ( pSat4 == NULL || nSeconds <= 0 )
return;
ccadical_limit( (CCaDiCaL *)pSat4->p, "seconds", nSeconds );
}

////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
Expand Down Expand Up @@ -64,6 +73,7 @@ struct Gia_ManBmc_t_
sat_solver * pSat; // SAT solver
satoko_t * pSat2; // SAT solver
bmcg_sat_solver * pSat3; // SAT solver
cadical_solver * pSat4; // SAT solver
int nSatVars; // SAT variables
int nObjNums; // SAT objects
int nWordNum; // unsigned words for ternary simulation
Expand Down Expand Up @@ -718,7 +728,7 @@ Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap )
SeeAlso []

***********************************************************************/
Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose )
Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose, int fUseCadical )
{
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
Expand Down Expand Up @@ -763,6 +773,11 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLi
for ( i = 0; i < 1000; i++ )
bmcg_sat_solver_addvar( p->pSat3 );
}
else if ( fUseCadical )
{
p->pSat4 = cadical_solver_new();
cadical_solver_setnvars(p->pSat4, 1000);
}
else
{
p->pSat = sat_solver_new();
Expand Down Expand Up @@ -806,9 +821,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
p->pSat ? p->pSat->nLearntDelta : 0,
p->pSat ? p->pSat->nLearntRatio : 0,
p->pSat ? p->pSat->nDBreduces : 0,
p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2),
p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2),
nUsedVars,
100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) );
100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) );
Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n",
p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps );
}
Expand All @@ -830,6 +845,7 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
if ( p->pSat ) sat_solver_delete( p->pSat );
if ( p->pSat2 ) satoko_destroy( p->pSat2 );
if ( p->pSat3 ) bmcg_sat_solver_stop( p->pSat3 );
if ( p->pSat4 ) cadical_solver_delete( p->pSat4 );
ABC_FREE( p->pTime4Outs );
Vec_IntFree( p->vData );
Hsh_IntManStop( p->vHash );
Expand Down Expand Up @@ -1029,6 +1045,11 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
if ( !bmcg_sat_solver_addclause( p->pSat3, ClaLits, nClaLits ) )
assert( 0 );
}
else if ( p->pSat4 )
{
if ( !cadical_solver_addclause( p->pSat4, ClaLits, ClaLits+nClaLits ) )
assert( 0 );
}
else
{
if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) )
Expand Down Expand Up @@ -1287,6 +1308,11 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
for ( i = bmcg_sat_solver_varnum(p->pSat3); i < p->nSatVars; i++ )
bmcg_sat_solver_addvar( p->pSat3 );
}
else if ( p->pSat4 )
{
for ( i = cadical_solver_nvars(p->pSat4); i < p->nSatVars; i++ )
cadical_solver_addvar( p->pSat4 );
}
else
sat_solver_setnvars( p->pSat, p->nSatVars );
return Lit;
Expand Down Expand Up @@ -1411,6 +1437,11 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
if ( iLit != ~0 && bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(iLit)) )
Abc_InfoSetBit( pCex->pData, iBit + k );
}
else if ( p->pSat4)
{
if ( iLit != ~0 && cadical_solver_get_var_value(p->pSat4, lit_var(iLit)) )
Abc_InfoSetBit( pCex->pData, iBit + k );
}
else
{
if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
Expand Down Expand Up @@ -1445,6 +1476,10 @@ int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit )
bmcg_sat_solver_set_conflict_budget( p->pSat3, p->pPars->nConfLimit );
return bmcg_sat_solver_solve( p->pSat3, &Lit, 1 );
}
else if ( p->pSat4 )
{
return cadical_solver_solve( p->pSat4, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
}
else
return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
}
Expand Down Expand Up @@ -1482,7 +1517,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
// create BMC manager
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose );
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose, pPars->fUseCadical );
p->pPars = pPars;
if ( p->pSat )
{
Expand All @@ -1498,6 +1533,10 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
{
// satoko_set_runid(p->pSat3, p->pPars->RunId);
// satoko_set_stop_func(p->pSat3, p->pPars->pFuncStop);
}
else if ( p->pSat4 )
{

}
else
{
Expand All @@ -1522,6 +1561,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
satoko_set_runtime_limit( p->pSat2, nTimeToStop );
else if ( p->pSat3 )
bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
else if ( p-> pSat4 )
Bmc3_CadicalSetRuntimeLimit( p->pSat4, nTimeToStop );
else
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
Expand Down Expand Up @@ -1659,6 +1700,8 @@ clkOther += Abc_Clock() - clk2;
satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
else if ( p->pSat3 )
bmcg_sat_solver_set_runtime_limit( p->pSat3, p->pTime4Outs[i] + Abc_Clock() );
else if ( p-> pSat4 )
Bmc3_CadicalSetRuntimeLimit( p->pSat4, p->pTime4Outs[i] + Abc_Clock() );
else
sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
}
Expand Down Expand Up @@ -1690,6 +1733,8 @@ nTimeUnsat += clkSatRun;
status = satoko_add_clause( p->pSat2, &Lit, 1 );
else if ( p->pSat3 )
status = bmcg_sat_solver_addclause( p->pSat3, &Lit, 1 );
else if ( p->pSat4 )
status = cadical_solver_addclause( p->pSat4, &Lit, &Lit + 1 );
else
status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
assert( status );
Expand Down Expand Up @@ -1721,12 +1766,12 @@ nTimeSat += clkSatRun;
{
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
// Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
// Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
// ABC_PRT( "Time", Abc_Clock() - clk );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
Abc_Print( 1, "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) );
Abc_Print( 1, "%4.0f MB", 1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) );
Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
Expand Down Expand Up @@ -1773,6 +1818,8 @@ nTimeSat += clkSatRun;
satoko_set_runtime_limit( p->pSat2, nTimeToStop );
else if ( p->pSat3 )
bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
else if ( p->pSat4 )
Bmc3_CadicalSetRuntimeLimit ( p->pSat4, nTimeToStop );
else
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
Expand All @@ -1798,6 +1845,11 @@ nTimeSat += clkSatRun;
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
continue;
}
else if (p->pSat4)
{
if ( cadical_solver_get_var_value(p->pSat4, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
continue;
}
else
{
if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
Expand Down Expand Up @@ -1841,19 +1893,19 @@ nTimeUndec += clkSatRun;
}
if ( pPars->fVerbose )
{
if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 )
if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 )
{
fFirst = 0;
// Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
}
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
// Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
// Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
// Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
if ( pPars->fSolveAll )
Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts );
if ( pPars->nTimeOutOne )
Expand Down
1 change: 1 addition & 0 deletions src/sat/cadical/cadical.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1058,6 +1058,7 @@ class Solver {
// Extra APIs
int clauses ();
int conflicts ();
int learned ();

private:
//==== start of state ====================================================
Expand Down
15 changes: 15 additions & 0 deletions src/sat/cadical/cadicalSolver.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -297,6 +297,21 @@ int cadical_solver_nconflicts(cadical_solver* s) {
return ccadical_conflicts((CCaDiCaL*)s->p);
}

/**Function*************************************************************

Synopsis [get number of learned clauses]

Description []

SideEffects []

SeeAlso []

***********************************************************************/
int cadical_solver_nlearned(cadical_solver* s) {
return ccadical_learned((CCaDiCaL*)s->p);
}


/**Function*************************************************************

Expand Down
1 change: 1 addition & 0 deletions src/sat/cadical/cadicalSolver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@ 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 int cadical_solver_nlearned(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
Expand Down
4 changes: 4 additions & 0 deletions src/sat/cadical/cadical_ccadical.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -228,4 +228,8 @@ int ccadical_conflicts(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->conflicts ();
}

int ccadical_learned(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->learned ();
}

ABC_NAMESPACE_IMPL_END
4 changes: 4 additions & 0 deletions src/sat/cadical/cadical_solver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1853,6 +1853,10 @@ int Solver::conflicts () {
return internal->stats.conflicts;
}

int Solver::learned () {
return internal->stats.learned.clauses;
}

} // namespace CaDiCaL

ABC_NAMESPACE_IMPL_END
1 change: 1 addition & 0 deletions src/sat/cadical/ccadical.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ void ccadical_resize(CCaDiCaL *, int min_max_var);
int ccadical_is_inconsistent(CCaDiCaL *);
int ccadical_clauses(CCaDiCaL *);
int ccadical_conflicts(CCaDiCaL *);
int ccadical_learned(CCaDiCaL *);

/*------------------------------------------------------------------------*/

Expand Down
Loading