/**CFile****************************************************************
FileName [giaSatMap.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaSatMap.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "sat/bsat/satStore.h"
#include "misc/vec/vecWec.h"
#include "misc/util/utilNam.h"
#include "map/scl/sclCon.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// operation manager
typedef struct Sbm_Man_t_ Sbm_Man_t;
struct Sbm_Man_t_
{
sat_solver * pSat; // SAT solver
Vec_Int_t * vCardVars; // candinality variables
int LogN; // max vars
int FirstVar; // first variable to be used
int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2)
int nInputs; // the number of inputs
// window
Vec_Int_t * vRoots; // output drivers to be mapped (root -> lit)
Vec_Wec_t * vCuts; // cuts (cut -> node lit + fanin lits)
Vec_Wec_t * vObjCuts; // cuts (obj -> node lit + cut lits)
Vec_Int_t * vSolCuts; // current solution (index -> cut)
Vec_Int_t * vCutGates; // gates (cut -> gate)
Vec_Wrd_t * vCutAreas; // area of each cut
// solver
Vec_Int_t * vAssump; // assumptions (root nodes)
Vec_Int_t * vPolar; // polarity of nodes and cuts
// timing
Vec_Int_t * vArrs; // arrivals for the inputs (input -> time)
Vec_Int_t * vReqs; // required for the outputs (root -> time)
// internal
Vec_Int_t * vLit2Used; // current solution (lit -> used)
Vec_Int_t * vDelays; // node arrivals (lit -> time)
Vec_Int_t * vReason; // timing reasons (lit -> cut)
};
/*
Cuts in p->vCuts have 0-based numbers and are expressed in terms of object literals.
Cuts in p->vObjCuts are expressed in terms of the obj-lit + cut-lits (i + p->FirstVar)
Unit cuts for each polarity are ordered in the end.
*/
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Verify solution. Create polarity and assumptions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbm_ManCheckSol( Sbm_Man_t * p, Vec_Int_t * vSol )
{
//int K = Vec_IntSize(vSol) - 1;
int i, j, Lit, Cut;
int RetValue = 1;
Vec_Int_t * vCut;
// clear polarity and assumptions
Vec_IntClear( p->vPolar );
// mark used literals
Vec_IntFill( p->vLit2Used, Vec_WecSize(p->vObjCuts) + p->nInputs, 0 );
Vec_IntForEachEntry( p->vSolCuts, Cut, i )
{
if ( Cut < 0 ) // input inverter variable
{
Vec_IntWriteEntry( p->vLit2Used, -Cut, 1 );
Vec_IntPush( p->vPolar, -Cut );
continue;
}
Vec_IntPush( p->vPolar, p->FirstVar + Cut );
vCut = Vec_WecEntry( p->vCuts, Cut );
Lit = Vec_IntEntry( vCut, 0 ) - p->LitShift; // obj literal
if ( Vec_IntEntry(p->vLit2Used, Lit) )
continue;
Vec_IntWriteEntry( p->vLit2Used, Lit, 1 );
Vec_IntPush( p->vPolar, Lit ); // literal variable
}
// check that the output literals are used
Vec_IntForEachEntry( p->vRoots, Lit, i )
{
if ( Vec_IntEntry(p->vLit2Used, Lit) == 0 )
printf( "Output literal %d has no cut.\n", Lit ), RetValue = 0;
}
// check internal nodes
Vec_IntForEachEntry( p->vSolCuts, Cut, i )
{
if ( Cut < 0 )
continue;
vCut = Vec_WecEntry( p->vCuts, Cut );
Vec_IntForEachEntryStart( vCut, Lit, j, 1 )
if ( Lit - p->LitShift < 0 )
{
assert( Abc_LitIsCompl(Lit) );
if ( Vec_IntEntry(p->vLit2Used, Vec_WecSize(p->vObjCuts) + Abc_Lit2Var(Lit)-1) == 0 )
printf( "Inverter of input %d of cut %d is not mapped.\n", Abc_Lit2Var(Lit)-1, Cut ), RetValue = 0;
}
else if ( Vec_IntEntry(p->vLit2Used, Lit - p->LitShift) == 0 )
printf( "Internal literal %d of cut %d is not mapped.\n", Lit - p->LitShift, Cut ), RetValue = 0;
// create polarity
Vec_IntPush( p->vPolar, p->FirstVar + Cut ); // cut variable
}
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Sbm_ManCreateCnf( Sbm_Man_t * p )
{
int i, k, Lit, Lits[2], value;
Vec_Int_t * vLits, * vCutOne, * vLitsPrev;
// sat_solver_rollback( p->Sat );
if ( !Sbm_ManCheckSol(p, p->vSolCuts) )
return 0;
// increase var count
assert( p->FirstVar == sat_solver_nvars(p->pSat) );
sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WecSize(p->vCuts) );
// iterate over arrays containing obj-lit cuts (neg-obj-lit cut-lits followed by pos-obj-lit cut-lits)
vLitsPrev = NULL;
Vec_WecForEachLevel( p->vObjCuts, vLits, i )
{
assert( Vec_IntSize(vLits) >= 2 );
value = sat_solver_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) );
assert( value );
/*
// for each cut, add implied nodes
Lits[0] = Abc_LitNot( Vec_IntEntry(vLits, 0) );
assert( Lits[0] < 2*p->FirstVar );
Vec_IntForEachEntryStart( vLits, Lit, k, 1 )
{
assert( Lit >= 2*p->FirstVar );
Lits[1] = Abc_LitNot( Lit );
value = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
assert( value );
//printf( "Adding clause %d + %d.\n", Lits[0], Lits[1]-2*p->FirstVar );
}
*/
//printf( "\n" );
// create invertor exclusivity clause
if ( i & 1 )
{
Lits[0] = Abc_LitNot( Vec_IntEntryLast(vLits) );
Lits[1] = Abc_LitNot( Vec_IntEntryLast(vLitsPrev) );
value = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
assert( value );
//printf( "Adding exclusivity clause %d + %d.\n", Lits[0]-2*p->FirstVar, Lits[1]-2*p->FirstVar );
}
vLitsPrev = vLits;
}
// add inverters
Vec_WecForEachLevel( p->vCuts, vCutOne, i )
Vec_IntForEachEntry( vCutOne, Lit, k )
if ( Abc_Lit2Var(Lit)-1 < p->nInputs ) // input
{
assert( k > 0 );
Lits[0] = Abc_Var2Lit( Vec_WecSize(p->vObjCuts) + Abc_Lit2Var(Lit)-1, 0 );
Lits[1] = Abc_Var2Lit( p->FirstVar + i, 1 );
value = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
assert( value );
}
else // internal node
{
Lits[0] = Abc_Var2Lit( Lit-p->LitShift, 0 );
Lits[1] = Abc_Var2Lit( p->FirstVar + i, 1 );
value = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
assert( value );
}
sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolar), Vec_IntSize(p->vPolar) );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int sat_solver_add_and1( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
{
lit Lits[3];
int Cid;
Lits[0] = toLitCond( iVar, !fCompl );
Lits[1] = toLitCond( iVar0, fCompl0 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( Cid );
Lits[0] = toLitCond( iVar, !fCompl );
Lits[1] = toLitCond( iVar1, fCompl1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( Cid );
/*
Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar0, !fCompl0 );
Lits[2] = toLitCond( iVar1, !fCompl1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
*/
return 3;
}
static inline int sat_solver_add_and2( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
{
lit Lits[3];
int Cid;
/*
Lits[0] = toLitCond( iVar, !fCompl );
Lits[1] = toLitCond( iVar0, fCompl0 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( Cid );
Lits[0] = toLitCond( iVar, !fCompl );
Lits[1] = toLitCond( iVar1, fCompl1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
assert( Cid );
*/
Lits[0] = toLitCond( iVar, fCompl );
Lits[1] = toLitCond( iVar0, !fCompl0 );
Lits[2] = toLitCond( iVar1, !fCompl1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
return 3;
}
/**Function*************************************************************
Synopsis [Adds a general cardinality constraint in terms of vVars.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Sbm_AddSorter( sat_solver * p, int * pVars, int i, int k, int * pnVars )
{
int iVar1 = (*pnVars)++;
int iVar2 = (*pnVars)++;
int fVerbose = 0;
if ( fVerbose )
{
int v;
for ( v = 0; v < i; v++ )
printf( " " );
printf( "<" );
for ( v = i+1; v < k; v++ )
printf( "-" );
printf( ">" );
for ( v = k+1; v < 8; v++ )
printf( " " );
printf( " " );
printf( "[%3d :%3d ] -> [%3d :%3d ]\n", pVars[i], pVars[k], iVar1, iVar2 );
}
// sat_solver_add_and1( p, iVar1, pVars[i], pVars[k], 1, 1, 1 );
// sat_solver_add_and2( p, iVar2, pVars[i], pVars[k], 0, 0, 0 );
sat_solver_add_half_sorter( p, iVar1, iVar2, pVars[i], pVars[k] );
pVars[i] = iVar1;
pVars[k] = iVar2;
}
static inline void Sbm_AddCardinConstrMerge( sat_solver * p, int * pVars, int lo, int hi, int r, int * pnVars )
{
int i, step = r * 2;
if ( step < hi - lo )
{
Sbm_AddCardinConstrMerge( p, pVars, lo, hi-r, step, pnVars );
Sbm_AddCardinConstrMerge( p, pVars, lo+r, hi, step, pnVars );
for ( i = lo+r; i < hi-r; i += step )
Sbm_AddSorter( p, pVars, i, i+r, pnVars );
for ( i = lo+r; i < hi-r-1; i += r )
{
lit Lits[2] = { Abc_Var2Lit(pVars[i], 0), Abc_Var2Lit(pVars[i+r], 1) };
int Cid = sat_solver_addclause( p, Lits, Lits + 2 );
assert( Cid );
}
}
}
static inline void Sbm_AddCardinConstrRange( sat_solver * p, int * pVars, int lo, int hi, int * pnVars )
{
if ( hi - lo >= 1 )
{
int i, mid = lo + (hi - lo) / 2;
for ( i = lo; i <= mid; i++ )
Sbm_AddSorter( p, pVars, i, i + (hi - lo + 1) / 2, pnVars );
Sbm_AddCardinConstrRange( p, pVars, lo, mid, pnVars );
Sbm_AddCardinConstrRange( p, pVars, mid+1, hi, pnVars );
Sbm_AddCardinConstrMerge( p, pVars, lo, hi, 1, pnVars );
}
}
int Sbm_AddCardinConstrPairWise( sat_solver * p, Vec_Int_t * vVars, int K )
{
int nVars = Vec_IntSize(vVars);
Sbm_AddCardinConstrRange( p, Vec_IntArray(vVars), 0, nVars - 1, &nVars );
sat_solver_bookmark( p );
return nVars;
}
sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars )
{
int nVars = 1 << LogN;
int nVarsAlloc = nVars + 2 * (nVars * LogN * (LogN-1) / 4 + nVars - 1), nVarsReal;
Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
sat_solver * pSat = sat_solver_new();
sat_solver_setnvars( pSat, nVarsAlloc );
nVarsReal = Sbm_AddCardinConstrPairWise( pSat, vVars, 2 );
assert( nVarsReal == nVarsAlloc );
*pvVars = vVars;
return pSat;
}
void Sbm_AddCardinConstrTest()
{
int LogN = 3, nVars = 1 << LogN, K = 2, Count = 1;
Vec_Int_t * vVars, * vLits = Vec_IntAlloc( nVars );
sat_solver * pSat = Sbm_AddCardinSolver( LogN, &vVars );
int nVarsReal = sat_solver_nvars( pSat );
int Lit = Abc_Var2Lit( Vec_IntEntry(vVars, K), 1 );
printf( "LogN = %d. N = %3d. Vars = %5d. Clauses = %6d. Comb = %d.\n", LogN, nVars, nVarsReal, sat_solver_nclauses(pSat), nVars * (nVars-1)/2 + nVars + 1 );
while ( 1 )
{
int i, status = sat_solver_solve( pSat, &Lit, &Lit+1, 0, 0, 0, 0 );
if ( status != l_True )
break;
Vec_IntClear( vLits );
printf( "%3d : ", Count++ );
for ( i = 0; i < nVars; i++ )
{
Vec_IntPush( vLits, Abc_Var2Lit(i, sat_solver_var_value(pSat, i)) );
printf( "%d", sat_solver_var_value(pSat, i) );
}
printf( "\n" );
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + nVars );
if ( status == 0 )
break;
}
sat_solver_delete( pSat );
Vec_IntFree( vVars );
Vec_IntFree( vLits );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Sbm_Man_t * Sbm_ManAlloc( int LogN )
{
Sbm_Man_t * p = ABC_CALLOC( Sbm_Man_t, 1 );
p->pSat = Sbm_AddCardinSolver( LogN, &p->vCardVars );
p->LogN = LogN;
p->FirstVar = sat_solver_nvars( p->pSat );
// window
p->vRoots = Vec_IntAlloc( 100 );
p->vCuts = Vec_WecAlloc( 1000 );
p->vObjCuts = Vec_WecAlloc( 1000 );
p->vSolCuts = Vec_IntAlloc( 100 );
p->vCutGates = Vec_IntAlloc( 100 );
p->vCutAreas = Vec_WrdAlloc( 100 );
// solver
p->vAssump = Vec_IntAlloc( 100 );
p->vPolar = Vec_IntAlloc( 100 );
// timing
p->vArrs = Vec_IntAlloc( 100 );
p->vReqs = Vec_IntAlloc( 100 );
// internal
p->vLit2Used = Vec_IntAlloc( 100 );
p->vDelays = Vec_IntAlloc( 100 );
p->vReason = Vec_IntAlloc( 100 );
return p;
}
void Sbm_ManStop( Sbm_Man_t * p )
{
sat_solver_delete( p->pSat );
Vec_IntFree( p->vCardVars );
// internal
Vec_IntFree( p->vRoots );
Vec_WecFree( p->vCuts );
Vec_WecFree( p->vObjCuts );
Vec_IntFree( p->vSolCuts );
Vec_IntFree( p->vCutGates );
Vec_WrdFree( p->vCutAreas );
// internal
Vec_IntFree( p->vAssump );
Vec_IntFree( p->vPolar );
// internal
Vec_IntFree( p->vArrs );
Vec_IntFree( p->vReqs );
// internal
Vec_IntFree( p->vLit2Used );
Vec_IntFree( p->vDelays );
Vec_IntFree( p->vReason );
ABC_FREE( p );
}
int Sbm_ManTestSat( void * pMan )
{
abctime clk = Abc_Clock(), clk2;
int i, k, Lit, LogN = 7, nVars = 1 << LogN, status, Root;
Sbm_Man_t * p = Sbm_ManAlloc( LogN );
word InvArea = 0;
int fKeepTrying = 1;
int StartSol;
// derive window
extern int Nf_ManExtractWindow( void * pMan, Vec_Int_t * vRoots, Vec_Wec_t * vCuts, Vec_Wec_t * vObjCuts, Vec_Int_t * vSolCuts, Vec_Int_t * vCutGates, Vec_Wrd_t * vCutAreas, word * pInvArea, int StartVar, int nVars );
p->nInputs = Nf_ManExtractWindow( pMan, p->vRoots, p->vCuts, p->vObjCuts, p->vSolCuts, p->vCutGates, p->vCutAreas, &InvArea, p->FirstVar, nVars );
p->LitShift = 2*p->nInputs+2;
assert( Vec_WecSize(p->vObjCuts) + p->nInputs <= nVars );
// print-out
// Vec_WecPrint( p->vCuts, 0 );
// printf( "\n" );
// Vec_WecPrint( p->vObjCuts, 0 );
// printf( "\n" );
Vec_IntPrint( p->vSolCuts );
printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n",
sat_solver_nclauses(p->pSat), Vec_WecSize(p->vObjCuts), Vec_WecSizeSize(p->vCuts),
sat_solver_nclauses(p->pSat) - Vec_WecSize(p->vObjCuts) - Vec_WecSizeSize(p->vCuts) );
// creating CNF
if ( !Sbm_ManCreateCnf(p) )
return 0;
// create assumptions
// cardinality
Vec_IntClear( p->vAssump );
Vec_IntPush( p->vAssump, -1 );
// unused variables
for ( i = Vec_WecSize(p->vObjCuts) + p->nInputs; i < nVars; i++ )
Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) );
// root variables
Vec_IntForEachEntry( p->vRoots, Root, i )
Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) );
// Vec_IntPrint( p->vAssump );
StartSol = Vec_IntSize(p->vSolCuts);
// StartSol = 30;
while ( fKeepTrying && StartSol-fKeepTrying > 0 )
{
printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
// for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ )
// Vec_IntPush( p->vAssump, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, i), 1) );
Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) );
// solve the problem
clk2 = Abc_Clock();
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 );
if ( status == l_True )
{
word AreaNew = 0;
int Count = 0;
printf( "AND Lits = %d. Inputs = %d. Vars = %d. All vars = %d.\n", Vec_WecSize(p->vObjCuts), p->nInputs, Vec_WecSize(p->vObjCuts) + p->nInputs, nVars );
// for ( i = 0; i < nVars; i++ )
// printf( "%d", sat_solver_var_value(p->pSat, i) );
// printf( "\n" );
for ( i = 0; i < nVars; i++ )
if ( sat_solver_var_value(p->pSat, i) )
{
printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
Count++;
if ( i >= Vec_WecSize(p->vObjCuts) )
AreaNew += InvArea;
}
printf( "Count = %d\n", Count );
// for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
// printf( "%d", sat_solver_var_value(p->pSat, i) );
// printf( "\n" );
Count = 1;
for ( i = p->FirstVar; i < sat_solver_nvars(p->pSat); i++ )
if ( sat_solver_var_value(p->pSat, i) )
{
Vec_Int_t * vCutOne = Vec_WecEntry(p->vCuts, i-p->FirstVar);
printf( "%2d : Cut %3d (Gate %2d) ", Count, i-p->FirstVar, Vec_IntEntry(p->vCutGates, i-p->FirstVar) );
Vec_IntForEachEntry( vCutOne, Lit, k )
printf( "%d(%d) ", Lit - 2*(p->nInputs+1), Abc_Lit2Var(Lit) );
printf( "\n" );
Count++;
AreaNew += Vec_WrdEntry(p->vCutAreas, i-p->FirstVar);
}
printf( "Area = %7.2f\n", Scl_Int2Flt((int)AreaNew) );
}
if ( status == l_False )
printf( "UNSAT " ), fKeepTrying = 0;
else if ( status == l_True )
printf( "SAT " ), fKeepTrying++;
Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
printf( "\n" );
}
Sbm_ManStop( p );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END