From d9f6af51afa7b84f8fb6d7c9d5cceef289b6f195 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 24 Jul 2023 16:21:42 -0700
Subject: [PATCH] Experiment with CNF cofactoring.

---
 src/sat/cnf/cnf.h     |  1 +
 src/sat/cnf/cnfMan.c  | 32 +++++++++++++++++++++-----------
 src/sat/cnf/cnfUtil.c | 41 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 63 insertions(+), 11 deletions(-)

diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h
index 35c0fa2f7..f79c67798 100644
--- a/src/sat/cnf/cnf.h
+++ b/src/sat/cnf/cnf.h
@@ -154,6 +154,7 @@ extern void            Cnf_ManStop( Cnf_Man_t * p );
 extern Vec_Int_t *     Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
 extern Cnf_Dat_t *     Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals );
 extern Cnf_Dat_t *     Cnf_DataDup( Cnf_Dat_t * p );
+extern Cnf_Dat_t *     Cnf_DataDupCof( Cnf_Dat_t * p, int Lit );
 extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
 extern void            Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips );
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c
index f63cc6335..518a066be 100644
--- a/src/sat/cnf/cnfMan.c
+++ b/src/sat/cnf/cnfMan.c
@@ -103,10 +103,8 @@ void Cnf_ManStop( Cnf_Man_t * p )
 ***********************************************************************/
 Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
 {
-    Vec_Int_t * vCiIds;
-    Aig_Obj_t * pObj;
-    int i;
-    vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
+    Aig_Obj_t * pObj; int i;
+    Vec_Int_t * vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
     Aig_ManForEachCi( p, pObj, i )
         Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
     return vCiIds;
@@ -126,9 +124,7 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
 Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals )
 {
     Cnf_Dat_t * pCnf;
-    int i;
-    pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
-    memset( pCnf, 0, sizeof(Cnf_Dat_t) );
+    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
     pCnf->pMan = pAig;
     pCnf->nVars = nVars;
     pCnf->nClauses = nClauses;
@@ -136,10 +132,8 @@ Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiter
     pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
     pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
     pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
-    pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(pAig) );
-//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
-    for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
-        pCnf->pVarNums[i] = -1;
+    if ( pCnf->pVarNums )
+    pCnf->pVarNums = ABC_FALLOC( int, Aig_ManObjNumMax(pAig) );
     return pCnf;
 }
 
@@ -160,11 +154,27 @@ Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p )
     int i;
     pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals );
     memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
+    if ( p->pVarNums )
     memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
     for ( i = 1; i < p->nClauses; i++ )
         pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
     return pCnf;
 }
+Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit )
+{
+    Cnf_Dat_t * pCnf;
+    int i;
+    pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+1, p->nLiterals+1 );
+    memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
+    if ( pCnf->pVarNums )
+    memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
+    for ( i = 1; i < p->nClauses; i++ )
+        pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
+    pCnf->pClauses[p->nClauses] = pCnf->pClauses[0] + p->nLiterals;
+    pCnf->pClauses[p->nClauses][0] = Lit;
+    assert( pCnf->pClauses[p->nClauses+1] == pCnf->pClauses[0] + p->nLiterals+1 );
+    return pCnf;
+}
 
 /**Function*************************************************************
 
diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c
index 5ccbeb0dd..d15e83665 100644
--- a/src/sat/cnf/cnfUtil.c
+++ b/src/sat/cnf/cnfUtil.c
@@ -469,6 +469,47 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cnf_DataBestVar( Cnf_Dat_t * p, int * pSkip )
+{
+    int * pNums = ABC_CALLOC( int, p->nVars );
+    int i, * pLit, NumMax = -1, iVarMax = -1;
+    for ( i = 0; i < p->nClauses; i++ )
+        for ( pLit = p->pClauses[i]; pLit < p->pClauses[i+1]; pLit++ )
+            pNums[Abc_Lit2Var(*pLit)]++;
+    for ( i = 0; i < p->nVars; i++ )
+        if ( (!pSkip || !pSkip[i]) && NumMax < pNums[i] )
+            NumMax = pNums[i], iVarMax = i;
+    ABC_FREE( pNums );
+    return iVarMax;
+}
+void Cnf_Experiment1()
+{
+    Cnf_Dat_t * pTemp, * p = Cnf_DataReadFromFile( "../166b.cnf" ); int i;
+    int * pSkip = ABC_CALLOC( int, p->nVars );
+    for ( i = 0; i < 100; i++ )
+    {
+        int iVar = Cnf_DataBestVar( p, pSkip );
+        char FileName[100]; sprintf( FileName, "cnf/%03d.cnf", i );
+        Cnf_DataWriteIntoFile( p, FileName, 0, NULL, NULL );
+        printf( "Dumped file \"%s\".\n", FileName );
+        p = Cnf_DataDupCof( pTemp = p, Abc_Var2Lit(iVar, 0) );
+        Cnf_DataFree( pTemp );
+        pSkip[iVar] = 1;
+    }
+    Cnf_DataFree( p );
+    ABC_FREE( pSkip );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///