giaQbf.c File Reference

#include "gia.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "misc/extra/extra.h"

Go to the source code of this file.

Data Structures
struct	Qbf_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Qbf_Man_t_	Qbf_Man_t
	DECLARATIONS ///. More...

Functions
Cnf_Dat_t *	Mf_ManGenerateCnf (Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose)
int	Gia_ManSatEnum (Gia_Man_t *pGia, int nConfLimit, int nTimeOut, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
void	Gia_QbfDumpFile (Gia_Man_t *pGia, int nPars)
Qbf_Man_t *	Gia_QbfAlloc (Gia_Man_t *pGia, int nPars, int fVerbose)
void	Gia_QbfFree (Qbf_Man_t *p)
Gia_Man_t *	Gia_QbfQuantify (Gia_Man_t *p, int nPars)
Gia_Man_t *	Gia_QbfCofactor (Gia_Man_t *p, int nPars, Vec_Int_t *vValues, Vec_Int_t *vParMap)
int	Gia_QbfAddCofactor (Qbf_Man_t *p, Gia_Man_t *pCof)
void	Gia_QbfOnePattern (Qbf_Man_t *p, Vec_Int_t *vValues)
void	Gia_QbfPrint (Qbf_Man_t *p, Vec_Int_t *vValues, int Iter)
int	Gia_QbfVerify (Qbf_Man_t *p, Vec_Int_t *vValues)
void	Gia_QbfAddSpecialConstr (Qbf_Man_t *p)
void	Gia_QbfLearnConstraint (Qbf_Man_t *p, Vec_Int_t *vValues)
int	Gia_QbfSolve (Gia_Man_t *pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fVerbose)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Qbf_Man_t_ Qbf_Man_t

DECLARATIONS ///.

CFile****************************************************************

FileName [giaQbf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [QBF solver.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 18, 2014.]

Revision [

Id:

giaQbf.c,v 1.00 2014/10/18 00:00:00 alanmi Exp

]

Definition at line 33 of file giaQbf.c.

Function Documentation

int Gia_ManSatEnum	(	Gia_Man_t *	pGia,
		int	nConfLimit,
		int	nTimeOut,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Naive way to enumerate SAT assignments.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file giaQbf.c.

{
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    Vec_Int_t * vLits;
    int i, iLit, iParVarBeg, Iter;
    int nSolutions = 0, RetValue = 0;
    abctime clkStart = Abc_Clock();
    pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1;
    Cnf_DataFree( pCnf );
    // iterate through the SAT assignment
    vLits = Vec_IntAlloc( Gia_ManPiNum(pGia) );
    for ( Iter = 1 ; ; Iter++ )
    {
        int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
        if ( status == l_False ) { RetValue =  1; break; }
        if ( status == l_Undef ) { RetValue =  0; break; }
        nSolutions++;
        // extract SAT assignment
        Vec_IntClear( vLits );
        for ( i = 0; i < Gia_ManPiNum(pGia); i++ )
            Vec_IntPush( vLits, Abc_Var2Lit(iParVarBeg+i, sat_solver_var_value(pSat, iParVarBeg+i)) );
        if ( fVerbose )
        {
            printf( "%5d : ", Iter );
            Vec_IntForEachEntry( vLits, iLit, i )
                printf( "%d", !Abc_LitIsCompl(iLit) );
            printf( "\n" );
        }
        // add clause
        if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) )
            { RetValue =  1; break; }
        if ( nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= nTimeOut ) { RetValue = 0; break; }
    }
    sat_solver_delete( pSat );
    Vec_IntFree( vLits );
    if ( nTimeOut && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= nTimeOut )
        printf( "Enumerated %d assignments when timeout (%d sec) was reached.  ", nSolutions, nTimeOut );
    else if ( nConfLimit && !RetValue )
        printf( "Enumerated %d assignments when conflict limit (%d) was reached.  ", nSolutions, nConfLimit );
    else 
        printf( "Enumerated the complete set of %d assignments.  ", nSolutions );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
    return RetValue;
}

int Gia_QbfAddCofactor	(	Qbf_Man_t *	p,
		Gia_Man_t *	pCof
	)

Definition at line 280 of file giaQbf.c.

{
    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 );
    int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) - 1;
    pCnf->pMan = NULL;
    Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) );
    for ( i = 0; i < pCnf->nClauses; i++ )
        if ( !sat_solver_addclause( p->pSatSyn, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
        {
            Cnf_DataFree( pCnf );
            return 0;
        }
    Cnf_DataFree( pCnf );
    // add connection clauses
    for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ )
        if ( !sat_solver_add_buffer( p->pSatSyn, i, iFirstVar+i, 0 ) )
            return 0;
    return 1;
}

void Gia_QbfAddSpecialConstr

(

Qbf_Man_t *

p

)

Function*************************************************************

Synopsis [Constraint learning.]

Description []

SideEffects []

SeeAlso []

Definition at line 368 of file giaQbf.c.

{
    int i, status, Lits[2];
    for ( i = 0; i < 4*11; i++ )
        if ( i % 4 == 0 )
        {
            assert( Vec_IntEntry(p->vParMap, i) == -1 );
            Vec_IntWriteEntry( p->vParMap, i, (i % 4) == 3 );
            Lits[0] = Abc_Var2Lit( i, (i % 4) != 3 );
            status = sat_solver_addclause( p->pSatSyn, Lits, Lits+1 );
            assert( status );
        }
}

Qbf_Man_t* Gia_QbfAlloc	(	Gia_Man_t *	pGia,
		int	nPars,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Generate one SAT assignment of the problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file giaQbf.c.

{
    Qbf_Man_t * p;
    Cnf_Dat_t * pCnf;
    Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) );
    pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
    Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) );
    p = ABC_CALLOC( Qbf_Man_t, 1 );
    p->clkStart   = Abc_Clock();
    p->pGia       = pGia;
    p->nPars      = nPars;
    p->nVars      = Gia_ManPiNum(pGia) - nPars;
    p->fVerbose   = fVerbose;
    p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia) - 1;
    p->pSatVer    = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    p->pSatSyn    = sat_solver_new();
    p->vValues    = Vec_IntAlloc( Gia_ManPiNum(pGia) );
    p->vParMap    = Vec_IntStartFull( nPars );
    p->vLits      = Vec_IntAlloc( nPars );
    sat_solver_setnvars( p->pSatSyn, nPars );
    Cnf_DataFree( pCnf );
    return p;
}

Gia_Man_t* Gia_QbfCofactor	(	Gia_Man_t *	p,
		int	nPars,
		Vec_Int_t *	vValues,
		Vec_Int_t *	vParMap
	)

Function*************************************************************

Synopsis [Create and add one cofactor.]

Description []

SideEffects []

SeeAlso []

Definition at line 253 of file giaQbf.c.

{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj; int i;
    assert( Gia_ManPiNum(p) == nPars + Vec_IntSize(vValues) );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    Gia_ManHashAlloc( pNew );
    Gia_ManConst0(p)->Value = 0;
    Gia_ManForEachPi( p, pObj, i )
        if ( i < nPars )
        {
            pObj->Value = Gia_ManAppendCi(pNew);
            if ( Vec_IntEntry(vParMap, i) != -1 )
                pObj->Value = Vec_IntEntry(vParMap, i);
        }
        else
            pObj->Value = Vec_IntEntry(vValues, i - nPars);
    Gia_ManForEachAnd( p, pObj, i )
        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
    Gia_ManForEachCo( p, pObj, i )
        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    assert( Gia_ManPiNum(pNew) == nPars );
    return pNew;
}

void Gia_QbfDumpFile	(	Gia_Man_t *	pGia,
		int	nPars
	)

Function*************************************************************

Synopsis [Dumps the original problem in QDIMACS format.]

Description []

SideEffects []

SeeAlso []

Definition at line 127 of file giaQbf.c.

{
    // original problem: \exists p \forall x \exists y.  M(p,x,y)
    // negated problem:  \forall p \exists x \exists y. !M(p,x,y)
    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
    Vec_Int_t * vVarMap, * vForAlls, * vExists;
    Gia_Obj_t * pObj;
    char * pFileName;
    int i, Entry;
    // create var map
    vVarMap = Vec_IntStart( pCnf->nVars );
    Gia_ManForEachCi( pGia, pObj, i )
        if ( i < nPars )
            Vec_IntWriteEntry( vVarMap, pCnf->pVarNums[Gia_ManCiIdToId(pGia, i)], 1 );
    // create various maps
    vForAlls = Vec_IntAlloc( nPars );
    vExists = Vec_IntAlloc( Gia_ManCiNum(pGia) - nPars );
    Vec_IntForEachEntry( vVarMap, Entry, i )
        if ( Entry )
            Vec_IntPush( vForAlls, i );
        else
            Vec_IntPush( vExists, i );
    // generate CNF
    pFileName = Extra_FileNameGenericAppend( pGia->pSpec, ".qdimacs" );
    Cnf_DataWriteIntoFile( pCnf, pFileName, 0, vForAlls, vExists );
    Cnf_DataFree( pCnf );
    Vec_IntFree( vForAlls );
    Vec_IntFree( vExists );
    Vec_IntFree( vVarMap );
    printf( "The 2QBF formula was written into file \"%s\".\n", pFileName );
}

void Gia_QbfFree

(

Qbf_Man_t *

p

)

Definition at line 193 of file giaQbf.c.

{
    sat_solver_delete( p->pSatVer );
    sat_solver_delete( p->pSatSyn );
    Vec_IntFree( p->vLits );
    Vec_IntFree( p->vValues );
    Vec_IntFree( p->vParMap );
    ABC_FREE( p );
}

void Gia_QbfLearnConstraint	(	Qbf_Man_t *	p,
		Vec_Int_t *	vValues
	)

Definition at line 381 of file giaQbf.c.

{
    int i, status, Entry, Lits[2];
    assert( Vec_IntSize(vValues) == p->nPars );
    printf( "  Pattern   " );
    Vec_IntPrintBinary( vValues );
    printf( "\n" );
    Vec_IntForEachEntry( vValues, Entry, i )
    {
        Lits[0] = Abc_Var2Lit( i, Entry );
        status = sat_solver_solve( p->pSatSyn, Lits, Lits+1, 0, 0, 0, 0 );
        printf( "  Var =%4d ", i );
        if ( status != l_True )
        {
            printf( "UNSAT\n" );
            Lits[0] = Abc_LitNot(Lits[0]);
            status = sat_solver_addclause( p->pSatSyn, Lits, Lits+1 );
            assert( status );
            continue;
        }
        Gia_QbfOnePattern( p, p->vLits );
        Vec_IntPrintBinary( p->vLits );
        printf( "\n" );
    }
    assert( Vec_IntSize(vValues) == p->nPars );
}

void Gia_QbfOnePattern	(	Qbf_Man_t *	p,
		Vec_Int_t *	vValues
	)

Function*************************************************************

Synopsis [Extract SAT assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file giaQbf.c.

{
    int i;
    Vec_IntClear( vValues );
    for ( i = 0; i < p->nPars; i++ )
        Vec_IntPush( vValues, sat_solver_var_value(p->pSatSyn, i) );
}

void Gia_QbfPrint	(	Qbf_Man_t *	p,
		Vec_Int_t *	vValues,
		int	Iter
	)

Definition at line 318 of file giaQbf.c.

{
    printf( "%5d : ", Iter );
    assert( Vec_IntSize(vValues) == p->nVars );
    Vec_IntPrintBinary( vValues ); printf( "  " );
    printf( "Var = %6d  ", sat_solver_nvars(p->pSatSyn) );
    printf( "Cla = %6d  ", sat_solver_nclauses(p->pSatSyn) );
    printf( "Conf = %6d  ", sat_solver_nconflicts(p->pSatSyn) );
    Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}

Gia_Man_t* Gia_QbfQuantify	(	Gia_Man_t *	p,
		int	nPars
	)

Function*************************************************************

Synopsis [Create and add one cofactor.]

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file giaQbf.c.

{
    Gia_Man_t * pNew, * pTemp;
    Gia_Obj_t * pObj; 
    int i, m, nMints = (1 << (Gia_ManPiNum(p) - nPars));
    assert( Gia_ManPoNum(p) == 1 );
    pNew = Gia_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    Gia_ManHashAlloc( pNew );
    Gia_ManConst0(p)->Value = 0;
    for ( i = 0; i < nPars; i++ )
        Gia_ManAppendCi(pNew);
    for ( m = 0; m < nMints; m++ )
    {
        Gia_ManForEachPi( p, pObj, i )
            pObj->Value = (i < nPars) ? Gia_Obj2Lit(pNew, Gia_ManPi(pNew, i)) : ((m >> (i - nPars)) & 1);
        Gia_ManForEachAnd( p, pObj, i )
            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
        Gia_ManForEachCo( p, pObj, i )
            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
    }
    pNew = Gia_ManCleanup( pTemp = pNew );
    Gia_ManStop( pTemp );
    assert( Gia_ManPiNum(pNew) == nPars );
    assert( Gia_ManPoNum(pNew) == nMints );
    return pNew;
}

int Gia_QbfSolve	(	Gia_Man_t *	pGia,
		int	nPars,
		int	nIterLimit,
		int	nConfLimit,
		int	nTimeOut,
		int	fVerbose
	)

Function*************************************************************

Synopsis [Performs QBF solving using an improved algorithm.]

Description []

SideEffects []

SeeAlso []

Definition at line 419 of file giaQbf.c.

{
    Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fVerbose );
    Gia_Man_t * pCof;
    int i, status, RetValue = 0;
    abctime clk;
//    Gia_QbfAddSpecialConstr( p );
    if ( fVerbose )
        printf( "Solving QBF for \"%s\" with %d parameters, %d variables and %d AIG nodes.\n", 
            Gia_ManName(pGia), p->nPars, p->nVars, Gia_ManAndNum(pGia) );
    assert( Gia_ManRegNum(pGia) == 0 );
    Vec_IntFill( p->vValues, nPars, 0 );
    for ( i = 0; Gia_QbfVerify(p, p->vValues); i++ )
    {
        // generate next constraint
        assert( Vec_IntSize(p->vValues) == p->nVars );
        pCof = Gia_QbfCofactor( pGia, nPars, p->vValues, p->vParMap );
        status = Gia_QbfAddCofactor( p, pCof );
        Gia_ManStop( pCof );
        if ( status == 0 )       { RetValue =  1; break; }
        // synthesize next assignment
        clk = Abc_Clock();
        status = sat_solver_solve( p->pSatSyn, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
        p->clkSat += Abc_Clock() - clk;
        if ( fVerbose )
            Gia_QbfPrint( p, p->vValues, i );
        if ( status == l_False ) { RetValue =  1; break; }
        if ( status == l_Undef ) { RetValue = -1; break; }
        // extract SAT assignment
        Gia_QbfOnePattern( p, p->vValues );
        assert( Vec_IntSize(p->vValues) == p->nPars );
        // examine variables
//        Gia_QbfLearnConstraint( p, p->vValues );
//        Vec_IntPrintBinary( p->vValues ); printf( "\n" );
        if ( nIterLimit && i+1 == nIterLimit ) { RetValue = -1; break; }
        if ( nTimeOut && (Abc_Clock() - p->clkStart)/CLOCKS_PER_SEC >= nTimeOut ) { RetValue = -1; break; }
    }
    if ( RetValue == 0 )
    {
        printf( "Parameters: " );
        assert( Vec_IntSize(p->vValues) == nPars );
        Vec_IntPrintBinary( p->vValues );
        printf( "\n" );
    }
    if ( RetValue == -1 && nTimeOut && (Abc_Clock() - p->clkStart)/CLOCKS_PER_SEC >= nTimeOut )
        printf( "The problem timed out after %d sec.  ", nTimeOut );
    else if ( RetValue == -1 && nConfLimit )
        printf( "The problem aborted after %d conflicts.  ", nConfLimit );
    else if ( RetValue == -1 && nIterLimit )
        printf( "The problem aborted after %d iterations.  ", nIterLimit );
    else if ( RetValue == 1 )
        printf( "The problem is UNSAT after %d iterations.  ", i );
    else 
        printf( "The problem is SAT after %d iterations.  ", i );
    if ( fVerbose )
    {
        printf( "\n" );
        Abc_PrintTime( 1, "SAT  ", p->clkSat );
        Abc_PrintTime( 1, "Other", Abc_Clock() - p->clkStart - p->clkSat );
        Abc_PrintTime( 1, "TOTAL", Abc_Clock() - p->clkStart );
    }
    else
        Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
    Gia_QbfFree( p );
    return RetValue;
}

int Gia_QbfVerify	(	Qbf_Man_t *	p,
		Vec_Int_t *	vValues
	)

Function*************************************************************

Synopsis [Generate one SAT assignment in terms of functional vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 340 of file giaQbf.c.

{
    int i, Entry, RetValue;
    assert( Vec_IntSize(vValues) == p->nPars );
    Vec_IntClear( p->vLits );
    Vec_IntForEachEntry( vValues, Entry, i )
        Vec_IntPush( p->vLits, Abc_Var2Lit(p->iParVarBeg+i, !Entry) );
    RetValue = sat_solver_solve( p->pSatVer, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits), 0, 0, 0, 0 );
    if ( RetValue == l_True )
    {
        Vec_IntClear( vValues );
        for ( i = 0; i < p->nVars; i++ )
            Vec_IntPush( vValues, sat_solver_var_value(p->pSatVer, p->iParVarBeg+p->nPars+i) );
    }
    return RetValue == l_True ? 1 : 0;
}

Cnf_Dat_t* Mf_ManGenerateCnf	(	Gia_Man_t *	pGia,
		int	nLutSize,
		int	fCnfObjIds,
		int	fAddOrCla,
		int	fVerbose
	)

Function*************************************************************

Synopsis [CNF generation]

Description []

SideEffects []

SeeAlso []

Definition at line 1629 of file giaMf.c.

{
    Gia_Man_t * pNew;
    Jf_Par_t Pars, * pPars = &Pars;
    assert( nLutSize >= 3 && nLutSize <= 8 );
    Mf_ManSetDefaultPars( pPars );
    pPars->fGenCnf    = 1;
    pPars->fCoarsen   = !fCnfObjIds;
    pPars->nLutSize   = nLutSize;
    pPars->fCnfObjIds = fCnfObjIds;
    pPars->fAddOrCla  = fAddOrCla;
    pPars->fVerbose   = fVerbose;
    pNew = Mf_ManPerformMapping( pGia, pPars );
    Gia_ManStopP( &pNew );
//    Cnf_DataPrint( (Cnf_Dat_t *)pGia->pData, 1 );
    return pGia->pData;
}