From 0533fc7de93284c487d848f36259a3f3e441b8df Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 May 2016 14:24:38 -0700 Subject: Experiments with generating sat assignments. --- src/base/wlc/wlc.c | 142 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 142 insertions(+) (limited to 'src/base') diff --git a/src/base/wlc/wlc.c b/src/base/wlc/wlc.c index 8e853181..08e62e6f 100644 --- a/src/base/wlc/wlc.c +++ b/src/base/wlc/wlc.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "wlc.h" +#include "sat/bsat/satStore.h" ABC_NAMESPACE_IMPL_START @@ -127,6 +128,147 @@ void Wlc_GenerateCodeMax4( int nBits ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wlc_BlastFullAdderCtrlCnf( sat_solver * pSat, int a, int ac, int b, int c, int * pc, int * ps, int * piVars ) +{ + int Cnf[12][6] = { // xabc cs // abc cs + + { -1, 0, 0, 0, 0, 0 }, // -000 00 // 000 00 + { -1, 0, 0, 1, 0, 1 }, // -001 01 // 001 01 + { -1, 0, 1, 0, 0, 1 }, // -010 01 // 010 01 + { -1, 0, 1, 1, 1, 0 }, // -011 10 // 011 10 + + { 0,-1, 0, 0, 0, 0 }, // 0-00 00 + { 0,-1, 0, 1, 0, 1 }, // 0-01 01 + { 0,-1, 1, 0, 0, 1 }, // 0-10 01 + { 0,-1, 1, 1, 1, 0 }, // 0-11 10 + + { 1, 1, 0, 0, 0, 1 }, // 1100 01 // 100 01 + { 1, 1, 0, 1, 1, 0 }, // 1101 10 // 101 10 + { 1, 1, 1, 0, 1, 0 }, // 1110 10 // 110 10 + { 1, 1, 1, 1, 1, 1 } // 1111 11 // 111 11 + }; + + int pVars[6] = {a, ac, b, c, *piVars, *piVars+1}; + int i, v, nLits, pLits[6]; + for ( i = 0; i < 12; i++ ) + { + if ( i == 7 ) + { + int x = 0; + } + nLits = 0; + for ( v = 0; v < 6; v++ ) + { + if ( Cnf[i][v] == -1 ) + continue; + if ( pVars[v] == 0 ) // const 0 + { + if ( Cnf[i][v] == 0 ) + continue; + if ( Cnf[i][v] == 1 ) + break; + } + if ( pVars[v] == -1 ) // const -1 + { + if ( Cnf[i][v] == 0 ) + break; + if ( Cnf[i][v] == 1 ) + continue; + } + pLits[nLits++] = Abc_Var2Lit( pVars[v], Cnf[i][v] ); + } + if ( v < 6 ) + continue; + assert( nLits > 2 ); + sat_solver_addclause( pSat, pLits, pLits + nLits ); + } + *pc = (*piVars)++; + *ps = (*piVars)++; +} +void Wlc_BlastMultiplierCnf( sat_solver * pSat, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vTemp, Vec_Int_t * vRes, int * piVars ) +{ + int * pRes, * pArgC, * pArgS, a, b, Carry = 0; + assert( nArgA > 0 && nArgB > 0 ); + // prepare result + Vec_IntFill( vRes, nArgA + nArgB, 0 ); + pRes = Vec_IntArray( vRes ); + // prepare intermediate storage + Vec_IntFill( vTemp, 2 * nArgA, 0 ); + pArgC = Vec_IntArray( vTemp ); + pArgS = pArgC + nArgA; + // create matrix + for ( b = 0; b < nArgB; b++ ) + for ( a = 0; a < nArgA; a++ ) + Wlc_BlastFullAdderCtrlCnf( pSat, pArgA[a], pArgB[b], pArgS[a], pArgC[a], &pArgC[a], a ? &pArgS[a-1] : &pRes[b], piVars ); + // final addition + pArgS[nArgA-1] = 0; + for ( a = 0; a < nArgA; a++ ) + Wlc_BlastFullAdderCtrlCnf( pSat, -1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], piVars ); +} +sat_solver * Wlc_BlastMultiplierCnfMain( int nBits ) +{ + Vec_Int_t * vRes1 = Vec_IntAlloc( 2*nBits ); + Vec_Int_t * vRes2 = Vec_IntAlloc( 2*nBits ); + Vec_Int_t * vTemp = Vec_IntAlloc( 2*nBits ); + + int * pArgA = ABC_ALLOC( int, nBits ); + int * pArgB = ABC_ALLOC( int, nBits ); + int i, Ent1, Ent2, nVars = 1 + 2*nBits; + int nVarsAll = 1 + 4*nBits + 4*nBits*(nBits + 1); + + sat_solver * pSat = sat_solver_new(); + sat_solver_setnvars( pSat, nVarsAll ); + + for ( i = 0; i < nBits; i++ ) + pArgA[i] = 1 + i, pArgB[i] = 1 + nBits + i; + Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes1, &nVars ); + + for ( i = 0; i < nBits; i++ ) + pArgA[i] = 1 + nBits + i, pArgB[i] = 1 + i; + Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes2, &nVars ); + + Vec_IntClear( vTemp ); + Vec_IntForEachEntryTwo( vRes1, vRes2, Ent1, Ent2, i ) + { + Vec_IntPush( vTemp, Abc_Var2Lit(nVars, 0) ); + sat_solver_add_xor( pSat, Ent1, Ent2, nVars++, 0 ); + } + assert( nVars == nVarsAll ); + sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); + + ABC_FREE( pArgA ); + ABC_FREE( pArgB ); + Vec_IntFree( vRes1 ); + Vec_IntFree( vRes2 ); + Vec_IntFree( vTemp ); + return pSat; +} +void Wlc_BlastMultiplierCnfTest( int nBits ) +{ + abctime clk = Abc_Clock(); + sat_solver * pSat = Wlc_BlastMultiplierCnfMain( nBits ); + int i, status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); + Sat_SolverWriteDimacs( pSat, "test_mult.cnf", NULL, NULL, 0 ); + for ( i = 0; i < sat_solver_nvars(pSat); i++ ) + printf( "%d=%d ", i, sat_solver_var_value(pSat, i) ); + printf( "\n" ); + + printf( "Verifying for %d bits: %s ", nBits, status == l_True ? "SAT" : "UNSAT" ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + sat_solver_delete( pSat ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3