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

Experiments with SAT solving.

This commit is contained in:
Alan Mishchenko 2023-10-20 20:53:43 -07:00
parent 3c4c558656
commit 72b423ba14
4 changed files with 361 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

113
src/aig/gia/giaUtil.c
View File

@ -3161,6 +3161,119 @@ void Gia_ManPrintArray( Gia_Man_t * p )
printf( "};\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_GetMValue( int i, int nIns, int Mint, unsigned Truth )
{
assert( i >= 0 && i < 16 );
if ( i < nIns )
return (Mint >> i) & 1;
if ( i == nIns )
{
if ( Mint < (1 << nIns) )
return (Truth >> Mint) & 1;
else
return ((Truth >> (Mint-(1 << nIns))) & 1) == 0;
}
else
return 1;
}
void Gia_ManTestProblem()
{
unsigned Truth = 0xFE;
int i, j, k, c, nIns = 3, nAux = 3;
int nTotal = nIns + 1 + nAux;
int nPairs = nTotal * (nTotal - 1) / 2;
int nMints = (1 << (nIns+1));
int M[64][100] = {{0}};
float Value[64] = {0};
float Solution[100] = {0};
assert( nMints <= 64 );
assert( nPairs <= 100 );
// 7 nodes: 3 inputs + 1 output + 3 aux
// 7*6/2 = 21 pairs
// 16 minterms
for ( k = 0; k < nMints; k++ )
{
for ( i = c = 0; i < nTotal; i++ )
for ( j = i+1; j < nTotal; j++ )
{
int iVal = Gia_GetMValue( i, nIns, k, Truth );
int jVal = Gia_GetMValue( j, nIns, k, Truth );
M[k][c++] = iVal == jVal ? 1 : -1;
}
Value[k] = k < (1 << nIns) ? -1 : 1;
assert( c == nPairs );
}
for ( k = 0; k < nMints; k++ )
{
for ( c = 0; c < nPairs; c++ )
printf( "%2d ", M[k][c] );
printf( "%3f\n", Value[k] );
}
// solve
float Delta = 0.02;
for ( i = 0; i < 100; i++ )
{
float Error = 0;
for ( k = 0; k < nMints; k++ )
Error += Value[k] > 0 ? Value[k] : -Value[k];
printf( "Round %3d : Error = %5f ", i, Error );
for ( c = 0; c < nPairs; c++ )
printf( "%2f ", Solution[c] );
printf( "\n" );
//if ( Error < 1 )
// Delta /= 10;
for ( c = 0; c < nPairs; c++ )
{
int Count = 0;
for ( k = 0; k < nMints; k++ )
if ( (M[k][c] > 0 && Value[k] > 0) || (M[k][c] < 0 && Value[k] < 0) )
Count++;
else
Count--;
if ( Count == 0 )
continue;
printf( "Count = %3d ", Count );
if ( Count > 0 )
{
printf( "Increasing %d by %f\n", c, Delta );
Solution[c] += Delta;
for ( k = 0; k < nMints; k++ )
if ( M[k][c] > 0 )
Value[k] -= Delta;
else
Value[k] -= Delta;
}
else
{
printf( "Reducing %d by %f\n", c, Delta );
Solution[c] -= Delta;
for ( k = 0; k < nMints; k++ )
if ( M[k][c] > 0 )
Value[k] += Delta;
else
Value[k] += Delta;
}
}
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

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

@ -139,6 +139,7 @@ static int Abc_CommandTestDec ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandTestNpn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestRPO ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestTruth ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRunSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRunEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRunGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRunTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -914,6 +915,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "testnpn", Abc_CommandTestNpn, 0 );
Cmd_CommandAdd( pAbc, "LogiCS", "testrpo", Abc_CommandTestRPO, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "testtruth", Abc_CommandTestTruth, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "runsat", Abc_CommandRunSat, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "runeco", Abc_CommandRunEco, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "rungen", Abc_CommandRunGen, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "xec", Abc_CommandRunTest, 0 );
@ -7168,6 +7170,93 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandRunSat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pFile = NULL;
char * pFileCnf = NULL;
int c, i, fWalk = 0, fKissat = 0, nIters = 10, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Ikwvh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
nIters = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nIters < 0 )
goto usage;
break;
case 'k':
fKissat ^= 1;
break;
case 'w':
fWalk ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( fKissat + fWalk != 1 ) {
printf( "Exactly one SAT solver should be selected.\n" );
return 1;
}
if ( argc != globalUtilOptind + 1 )
goto usage;
pFileCnf = argv[globalUtilOptind];
pFile = fopen( pFileCnf, "rb" );
if ( pFile == NULL ) {
printf( "The file \"%s\" cannot be found.\n", pFileCnf );
return 1;
}
fclose( pFile );
abctime clk = Abc_Clock();
for ( i = 0; i < nIters; i++ ) {
char pCommand[1000];
if ( fKissat )
sprintf( pCommand, "kissat -q --seed=%d %s", i, pFileCnf );
else if ( fWalk )
sprintf( pCommand, "walk -s%d %s", i, pFileCnf );
if (system(pCommand) == -1) {
fprintf(stdout, "Command \"%s\" did not succeed.\n", pCommand);
return 0;
}
}
printf( "Performed %d iterations of SAT solving. ", nIters );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return 0;
usage:
Abc_Print( -2, "usage: runsat [-I num] [-kwvh] <cnf_file>\n" );
Abc_Print( -2, "\t performs randomized iterations of SAT solving\n" );
Abc_Print( -2, "\t-I num : the number of iterations [default = %d]\n", nIters );
Abc_Print( -2, "\t-k : toggle using Kissat (binary name \"kissat\") [default = %s]\n", fKissat? "yes": "no" );
Abc_Print( -2, "\t-w : toggle using WalkSat (binary name \"walk\") [default = %s]\n", fWalk? "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;
}
/**Function*************************************************************
Synopsis []
@ -14622,7 +14711,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
*/
//Gia_ManTestProblem();
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );

71
src/base/io/io.c
View File

@ -52,6 +52,7 @@ static int IoCommandReadInit ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadPlaMo ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadGig ( Abc_Frame_t * pAbc, int argc, char **argv );
@ -124,6 +125,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_plamo", IoCommandReadPlaMo, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_cnf", IoCommandReadCnf, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_status", IoCommandReadStatus, 0 );
Cmd_CommandAdd( pAbc, "I/O", "&read_gig", IoCommandReadGig, 0 );
@ -1209,6 +1211,75 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadCnf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Ptr_t * Io_FileReadCnf( char * pFileName );
FILE * pFile;
Abc_Ntk_t * pNtk;
Vec_Ptr_t * vSops;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
pFile = fopen( argv[globalUtilOptind], "rb" );
if ( pFile == NULL )
{
printf( "The file \"%s\" cannot be found.\n", argv[globalUtilOptind] );
return 1;
}
else
fclose( pFile );
vSops = Io_FileReadCnf( argv[globalUtilOptind] );
if ( Vec_PtrSize(vSops) == 0 )
{
Vec_PtrFreeFree( vSops );
fprintf( pAbc->Err, "Reading CNF file has failed.\n" );
return 1;
}
pNtk = Abc_NtkCreateWithNodes( vSops );
Vec_PtrFreeFree( vSops );
if ( pNtk == NULL )
{
fprintf( pAbc->Err, "Deriving the network has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
Abc_FrameClearVerifStatus( pAbc );
return 0;
usage:
fprintf( pAbc->Err, "usage: read_cnf [-h] <file>\n" );
fprintf( pAbc->Err, "\t creates network with one node\n" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : file name with the truth table\n" );
return 1;
}
/**Function*************************************************************
Synopsis []

87
src/base/io/ioUtil.c
View File

@ -920,6 +920,93 @@ void Io_TransformSF2PLA( char * pNameIn, char * pNameOut )
ABC_FREE( pBuffer );
}
/**Function*************************************************************
Synopsis [Reads CNF from file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars )
{
Vec_Int_t * vLevel; int i, k, Num;
int nSize = (nVars + 3)*Vec_WecSize(vNums);
char * pStr = ABC_ALLOC( char, nSize+1 );
memset( pStr, '-', nSize );
pStr[nSize] = 0;
Vec_WecForEachLevel( vNums, vLevel, i )
{
char * pCube = pStr + (nVars + 3)*i;
Vec_IntForEachEntry( vLevel, Num, k )
pCube[Abc_Lit2Var(Num)] = '0' + Abc_LitIsCompl(Num);
pCube[nVars+0] = ' ';
pCube[nVars+1] = '1';
pCube[nVars+2] = '\n';
}
return pStr;
}
Vec_Ptr_t * Io_FileReadCnf( char * pFileName )
{
Vec_Ptr_t * vSops = Vec_PtrAlloc( 1 );
Vec_Wec_t * vNums = Vec_WecAlloc( 100 );
Vec_Int_t * vLevel;
char * pThis, pLine[10000];
int nVars = -1, nClas = -1;
FILE * pFile = fopen( pFileName, "rb" );
if ( pFile == NULL ) {
printf( "Cannot open file \"%s\" for reading.\n", pFileName );
return NULL;
}
while ( fgets( pLine, 10000, pFile ) )
{
if ( pLine[0] == 'c' )
continue;
if ( pLine[0] == 'p' )
{
pThis = strtok(pLine+1, " \t\n\r");
if ( strcmp(pThis, "cnf") )
{
Vec_PtrFree( vSops );
Vec_WecFree( vNums );
fclose( pFile );
printf( "Wrong file format.\n" );
return NULL;
}
pThis = strtok(NULL, " \t\n\r");
nVars = atoi(pThis);
pThis = strtok(NULL, " \t\n\r");
nClas = atoi(pThis);
continue;
}
pThis = strtok(pLine, " \t\n\r");
if ( pThis == NULL )
continue;
vLevel = Vec_WecPushLevel( vNums );
while ( pThis ) {
int fComp, Temp = atoi(pThis);
if ( Temp == 0 )
break;
fComp = Temp < 0;
Temp = Temp < 0 ? -Temp : Temp;
Temp -= 1;
assert( Temp < nVars );
Vec_IntPush( vLevel, Abc_Var2Lit(Temp, fComp) );
pThis = strtok(NULL, " \t\n\r");
}
}
fclose( pFile );
if ( nClas != Vec_WecSize(vNums) )
printf( "Warning: The number of clauses (%d) listed is different from the actual number (%d).\n", nClas, Vec_WecSize(vNums) );
//Vec_WecPrint( vNums, 0 );
Vec_PtrPush( vSops, Io_ConvertNumsToSop(vNums, nVars) );
Vec_WecFree( vNums );
return vSops;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////