From 4f09348367d03e5dae158a5232297f7507742b64 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 23 Apr 2014 09:52:35 -0700 Subject: Experiments with permutations. --- src/misc/extra/extraUtilPerm.c | 163 +++++++++++++++++++++++++++-------------- 1 file changed, 110 insertions(+), 53 deletions(-) (limited to 'src/misc/extra') diff --git a/src/misc/extra/extraUtilPerm.c b/src/misc/extra/extraUtilPerm.c index d5b8e080..752a7d0b 100644 --- a/src/misc/extra/extraUtilPerm.c +++ b/src/misc/extra/extraUtilPerm.c @@ -128,6 +128,7 @@ static inline int Abc_ZddCacheInsert( Abc_ZddMan * p, int Arg0, int Arg1, int Ar Abc_ZddEnt * pEnt = p->pCache + (Abc_ZddHash(Arg0, Arg1, Arg2) & p->nCacheMask); pEnt->Arg0 = Arg0; pEnt->Arg1 = Arg1; pEnt->Arg2 = Arg2; pEnt->Res = Res; p->nCacheMisses++; + assert( Res >= 0 ); return Res; } static inline int Abc_ZddUniqueLookup( Abc_ZddMan * p, int Var, int True, int False ) @@ -394,12 +395,11 @@ int Abc_ZddMultiply( Abc_ZddMan * p, int a, int Var ) if ( (int)A->Var > Var ) r = Abc_ZddUniqueCreate( p, Var, a, 0 ); else if ( (int)A->Var < Var ) - { r0 = Abc_ZddMultiply( p, A->False, Var ), - r1 = Abc_ZddMultiply( p, A->True, Var ); + r1 = Abc_ZddMultiply( p, A->True, Var ), r = Abc_ZddUniqueCreate( p, A->Var, r1, r0 ); - } - else assert( 0 ); + else + r = Abc_ZddUniqueCreate( p, A->Var, A->False, A->True ); return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_MULTIPLY, r ); } int Abc_ZddCountPaths( Abc_ZddMan * p, int a ) @@ -555,55 +555,54 @@ int Abc_ZddDotMinProduct6( Abc_ZddMan * p, int a, int b ) int Abc_ZddPerm( Abc_ZddMan * p, int a, int Var ) { Abc_ZddObj * A; - int r; + int r0, r1, r; assert( Var < p->nVars ); if ( a == 0 ) return 0; if ( a == 1 ) return Abc_ZddIthVar(Var); if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_PERM)) >= 0 ) return r; A = Abc_ZddNode( p, a ); - if ( (int)A->Var == Var ) - r = Abc_ZddUniqueCreate( p, A->Var, A->False, A->True ); - else if ( p->pV2TI[A->Var] > p->pV2TJ[Var] ) + if ( p->pV2TI[A->Var] > p->pV2TI[Var] ) // Ai > Bi r = Abc_ZddUniqueCreate( p, Var, a, 0 ); + else if ( (int)A->Var == Var ) // Ai == Bi && Aj == Bj + r0 = Abc_ZddPerm( p, A->False, Var ), + r = Abc_ZddUnion( p, r0, A->True ); else { - int r0, r1, VarTop, VarPerm; + int VarPerm, VarTop; int Ai = p->pV2TI[A->Var]; int Aj = p->pV2TJ[A->Var]; int Bi = p->pV2TI[Var]; int Bj = p->pV2TJ[Var]; - assert( Ai < Aj && Bi < Bj ); - if ( Ai == Bj || (Ai == Bi && Aj > Bj) || (Aj == Bj && Ai > Bi) ) - VarTop = Var, - VarPerm = A->Var; - else if ( Ai == Bi ) - VarTop = A->Var, - VarPerm = Abc_ZddVarIJ(p, Aj, Bj); + assert( Ai < Aj && Bi < Bj && Ai <= Bi ); + if ( Aj == Bi ) + VarPerm = Var, + VarTop = Abc_ZddVarIJ(p, Ai, Bj); else if ( Aj == Bj ) - VarTop = Abc_ZddVarIJ(p, Ai, Bi), - VarPerm = Abc_ZddVarIJ(p, Bi, Bj); - else if ( Aj == Bi ) - VarTop = A->Var, - VarPerm = Abc_ZddVarIJ(p, Ai, Bj); + VarPerm = Var, + VarTop = Abc_ZddVarIJ(p, Ai, Bi); + else if ( Ai == Bi ) + VarPerm = Abc_ZddVarIJ(p, Abc_MinInt(Aj, Bj), Abc_MaxInt(Aj, Bj)), + VarTop = A->Var; else // no clash - VarTop = A->Var, - VarPerm = Var; + VarPerm = Var, + VarTop = A->Var; + assert( p->pV2TI[VarPerm] > p->pV2TI[VarTop] ); r0 = Abc_ZddPerm( p, A->False, Var ); r1 = Abc_ZddPerm( p, A->True, VarPerm ); - if ( VarTop < Abc_ZddObjVar(p, r0) && VarTop < Abc_ZddObjVar(p, r1) ) + assert( Abc_ZddObjVar(p, r1) > VarTop ); + if ( Abc_ZddObjVar(p, r0) > VarTop ) r = Abc_ZddUniqueCreate( p, VarTop, r1, r0 ); else - { - r1 = Abc_ZddMultiply( p, r1, VarTop ); + r1 = Abc_ZddUniqueCreate( p, VarTop, r1, 0 ), r = Abc_ZddUnion( p, r0, r1 ); - } } return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_PERM, r ); } + int Abc_ZddPermProduct( Abc_ZddMan * p, int a, int b ) { - Abc_ZddObj * A, * B; + Abc_ZddObj * B; int r0, r1, r; if ( a == 0 ) return 0; if ( a == 1 ) return b; @@ -611,27 +610,11 @@ int Abc_ZddPermProduct( Abc_ZddMan * p, int a, int b ) if ( b == 1 ) return a; if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_PERM_PROD)) >= 0 ) return r; - A = Abc_ZddNode( p, a ); - B = Abc_ZddNode( p, b ); - if ( Abc_ZddVarsClash(p, A->Var, B->Var) ) - { - r0 = Abc_ZddPermProduct( p, a, B->False ); - r1 = Abc_ZddPermProduct( p, a, B->True ); - r1 = Abc_ZddPerm( p, r1, B->Var ); - r = Abc_ZddUnion( p, r1, r0 ); - assert( Abc_MinInt(A->Var, B->Var) <= (int)Abc_ZddObjVar(p, r) ); - } - else - { - if ( A->Var < B->Var ) - r0 = Abc_ZddPermProduct( p, A->False, b ), - r1 = Abc_ZddPermProduct( p, A->True, b ); - else if ( A->Var > B->Var ) - r0 = Abc_ZddPermProduct( p, a, B->False ), - r1 = Abc_ZddPermProduct( p, a, B->True ); - else assert( 0 ); - r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 ); - } + B = Abc_ZddNode( p, b ); + r0 = Abc_ZddPermProduct( p, a, B->False ); + r1 = Abc_ZddPermProduct( p, a, B->True ); + r1 = Abc_ZddPerm( p, r1, B->Var ); + r = Abc_ZddUnion( p, r0, r1 ); return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_PERM_PROD, r ); } @@ -651,12 +634,14 @@ void Abc_ZddPermPrint( int * pPerm, int Size ) int i; printf( "{" ); for ( i = 0; i < Size; i++ ) - printf( " %d", pPerm[i] ); + printf( " %2d", pPerm[i] ); printf( " }\n" ); } void Abc_ZddCombPrint( int * pComb, int nTrans ) { int i; + if ( nTrans == 0 ) + printf( "Empty set" ); for ( i = 0; i < nTrans; i++ ) printf( "(%d %d)", pComb[i] >> 16, pComb[i] & 0xffff ); printf( "\n" ); @@ -715,11 +700,11 @@ void Abc_ZddPrint_rec( Abc_ZddMan * p, int a, int * pPath, int Size ) // if ( a == 1 ) { Abc_ZddPermPrint( pPath, Size ); return; } if ( a == 1 ) { - int pPerm[10], pComb[10], i; - assert( p->nPermSize <= 10 ); + int pPerm[24], pComb[24], i; + assert( p->nPermSize <= 24 ); for ( i = 0; i < Size; i++ ) pComb[i] = (p->pV2TI[pPath[i]] << 16) | p->pV2TJ[pPath[i]]; -// Abc_ZddCombPrint( pComb, Size ); + Abc_ZddCombPrint( pComb, Size ); Abc_ZddComb2Perm( pComb, Size, pPerm, p->nPermSize ); Abc_ZddPermPrint( pPerm, p->nPermSize ); return; @@ -858,6 +843,78 @@ void Abc_ZddPermTest() Abc_ZddManFree( p ); } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_EnumerateCubeStatesZdd() +{ + int pXYZ[3][9][2] = { + { {3, 5}, {3,17}, {3,15}, {1, 6}, {1,16}, {1,14}, {2, 4}, {2,18}, {2,13} }, + { {2,14}, {2,24}, {2,12}, {3,13}, {3,23}, {3,10}, {1,15}, {1,22}, {1,11} }, + { {1,10}, {1, 7}, {1, 4}, {3,12}, {3, 9}, {3, 6}, {2,11}, {2, 8}, {2, 5} } }; + Abc_ZddMan * p; + int i, k, pComb[9], pPerm[24], nSize; + int ZddTurn1, ZddTurn2, ZddTurn3, ZddTurns9, ZddAll, ZddReached, ZddNew; + abctime clk = Abc_Clock(); + printf( "Enumerating states of 2x2x2 cube.\n" ); + p = Abc_ZddManAlloc( 24 * 23 / 2, 1 << 28 ); + Abc_ZddManCreatePerms( p, 24 ); + // init state + printf( "Iter %2d -> %8d ", 0, 1 ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + // first 9 states + ZddTurns9 = 0; + for ( i = 0; i < 3; i++ ) + { + for ( k = 0; k < 24; k++ ) + pPerm[k] = k; + for ( k = 0; k < 9; k++ ) + ABC_SWAP( int, pPerm[pXYZ[i][k][0]-1], pPerm[pXYZ[i][k][1]-1] ); + nSize = Abc_ZddPerm2Comb( pPerm, 24, pComb ); + assert( nSize == 9 ); + for ( k = 0; k < 9; k++ ) + pComb[k] = Abc_ZddVarIJ( p, pComb[k] >> 16, pComb[k] & 0xffff ); + // add first turn + ZddTurn1 = Abc_ZddBuildSet( p, pComb, 9 ); + ZddTurns9 = Abc_ZddUnion( p, ZddTurns9, ZddTurn1 ); + //Abc_ZddPrint( p, ZddTurn1 ); + // add second turn + ZddTurn2 = Abc_ZddPermProduct( p, ZddTurn1, ZddTurn1 ); + ZddTurns9 = Abc_ZddUnion( p, ZddTurns9, ZddTurn2 ); + //Abc_ZddPrint( p, ZddTurn2 ); + // add third turn + ZddTurn3 = Abc_ZddPermProduct( p, ZddTurn2, ZddTurn1 ); + ZddTurns9 = Abc_ZddUnion( p, ZddTurns9, ZddTurn3 ); + //Abc_ZddPrint( p, ZddTurn3 ); + //printf( "\n" ); + } + //Abc_ZddPrint( p, ZddTurns9 ); + printf( "Iter %2d -> %8d ", 1, Abc_ZddCountPaths(p, ZddTurns9) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + // other states + ZddNew = ZddTurns9; + ZddAll = Abc_ZddUnion( p, 1, ZddTurns9 ); + for ( i = 2; i <= 100; i++ ) + { + ZddReached = Abc_ZddPermProduct( p, ZddNew, ZddTurns9 ); + ZddNew = Abc_ZddDiff( p, ZddReached, ZddAll ); + ZddAll = Abc_ZddUnion( p, ZddAll, ZddNew ); + printf( "Iter %2d -> %8d ", i, Abc_ZddCountPaths(p, ZddNew) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + if ( ZddNew == 0 ) + break; + } + Abc_ZddManFree( p ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3