From 039f05cb56a6708226eba0645bb66a9e04b4786f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 27 Jul 2023 20:50:02 -0700 Subject: [PATCH] Adding preprocessing to command &splitsat. --- src/base/abci/abc.c | 14 +++++++++----- src/sat/cnf/cnfUtil.c | 36 ++++++++++++++++++++++++++++-------- 2 files changed, 37 insertions(+), 13 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a86c4848b..76b56d5f4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -46097,10 +46097,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Cnf_SplitSat( char * pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fVerbose ); - int c, iVarBeg = 0, iVarEnd = ABC_INFINITY, nLits = 10, Value = 2, TimeOut = 5, nProcs = 1, nIters = 1, Seed = 0, fVerbose = 0; char * pFileName = NULL; + extern void Cnf_SplitSat( char * pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose ); + int c, iVarBeg = 0, iVarEnd = ABC_INFINITY, nLits = 10, Value = 2, TimeOut = 5, nProcs = 1, nIters = 1, Seed = 0, fPrepro = 0, fVerbose = 0; char * pFileName = NULL; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "BENVTPISvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "BENVTPISpvh" ) ) != EOF ) { switch ( c ) { @@ -46192,6 +46192,9 @@ int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Seed < 0 ) goto usage; break; + case 'p': + fPrepro ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -46218,11 +46221,11 @@ int Abc_CommandAbc9SplitSat( Abc_Frame_t * pAbc, int argc, char ** argv ) } fclose( pFile ); } - Cnf_SplitSat( pFileName, iVarBeg, iVarEnd, nLits, Value, TimeOut, nProcs, nIters, Seed, fVerbose ); + Cnf_SplitSat( pFileName, iVarBeg, iVarEnd, nLits, Value, TimeOut, nProcs, nIters, Seed, fPrepro, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &splitsat [-BENVTPIS num] [-vh]\n" ); + Abc_Print( -2, "usage: &splitsat [-BENVTPIS num] [-pvh]\n" ); Abc_Print( -2, "\t solves CNF-based SAT problem by randomized case-splitting\n" ); Abc_Print( -2, "\t-B num : the first CNF variable to use for splitting [default = %d]\n", iVarBeg ); Abc_Print( -2, "\t-E num : the last CNF variable to use for splitting [default = %d]\n", iVarEnd ); @@ -46232,6 +46235,7 @@ usage: Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs ); Abc_Print( -2, "\t-I num : the max number of iterations (0 = infinity) [default = %d]\n", nIters ); Abc_Print( -2, "\t-S num : the random seed used to generate cofactors [default = %d]\n", Seed ); + Abc_Print( -2, "\t-p : toggle using SatELIte (http://minisat.se/SatELite.html) [default = %s]\n", fPrepro? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index 9d1bb9722..ac6d0ebf1 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -74,11 +74,15 @@ Vec_Int_t *Cnf_RunSolverOnce(int Id, int Rand, int TimeOut, int fVerbose) else sprintf(pCommand, "%s --seed=%d %s %s > %s", pKissat, Rand, fVerboseSolver ? "" : "-q", FileNameIn, FileNameOut); //printf( "Thread command: %s\n", pCommand); - if (system(pCommand) == -1) { - fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand); - return 0; + FILE * pFile = fopen(FileNameIn, "rb"); + if ( pFile != NULL ) { + fclose( pFile ); + if (system(pCommand) == -1) { + fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand); + return 0; + } + vRes = Exa4_ManParse(FileNameOut); // FileNameOut is removed here } - vRes = Exa4_ManParse(FileNameOut); // FileNameOut is removed here if (fVerbose) { double SolvingTime = ((double)(Abc_Clock() - clkTotal))/((double)CLOCKS_PER_SEC); if (vRes) @@ -741,7 +745,7 @@ Vec_Int_t *Cnf_GenRandLits(int iVarBeg, int iVarEnd, int nLits, int Value, int R fflush(stdout); return vLits; } -void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fVerbose) +void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, int nLits, int Value, int Rand, int fPrepro, int fVerbose) { Cnf_Dat_t *p = Cnf_DataReadFromFile(pFileName); int k; if (iVarEnd == ABC_INFINITY) @@ -751,7 +755,18 @@ void Cnf_SplitCnfFile(char * pFileName, int nParts, int iVarBeg, int iVarEnd, in Vec_Int_t *vLits = Cnf_GenRandLits(iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose); Cnf_Dat_t *pCnf = Cnf_DataDupCofArray(p, vLits); char FileName[100]; sprintf(FileName, "%02d.cnf", k); - Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL); + if ( fPrepro ) { + char Command[1000]; + sprintf(Command, "satelite --verbosity=0 -pre temp.cnf %s", FileName); + Cnf_DataWriteIntoFile(pCnf, "temp.cnf", 0, NULL, NULL); + if (system(Command) == -1) { + fprintf(stdout, "Command \"%s\" did not succeed. Preprocessing skipped.\n", Command); + Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL); + } + unlink("temp.cnf"); + } + else + Cnf_DataWriteIntoFile(pCnf, FileName, 0, NULL, NULL); Cnf_DataFree(pCnf); Vec_IntFree(vLits); } @@ -765,7 +780,7 @@ void Cnf_SplitCnfCleanup(int nParts) unlink(FileName); } } -void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fVerbose) +void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Value, int TimeOut, int nProcs, int nIters, int Seed, int fPrepro, int fVerbose) { abctime clk = Abc_Clock(); Vec_Int_t *vSol = NULL; @@ -778,9 +793,14 @@ void Cnf_SplitSat(char *pFileName, int iVarBeg, int iVarEnd, int nLits, int Valu Rand = Abc_Random(0); for (i = 0; i < nIters && !vSol; i++) { - Cnf_SplitCnfFile(pFileName, nProcs, iVarBeg, iVarEnd, nLits, Value, Rand, fVerbose); + abctime clk2 = Abc_Clock(); + Cnf_SplitCnfFile(pFileName, nProcs, iVarBeg, iVarEnd, nLits, Value, Rand, fPrepro, fVerbose); vSol = Cnf_RunSolver(nProcs, TimeOut, fVerbose); Cnf_SplitCnfCleanup(nProcs); + if (fVerbose) { + printf( "Finished iteration %d. ", i); + Abc_PrintTime(0, "Time", Abc_Clock() - clk2); + } } printf("%solution is found. ", vSol ? "S" : "No s"); Abc_PrintTime(0, "Total time", Abc_Clock() - clk);