summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/proof/pdr/pdrCore.c58
-rw-r--r--src/sat/bsat/satSolver.c94
-rw-r--r--src/sat/bsat/satSolver.h1
3 files changed, 132 insertions, 21 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 9d42417b..60454752 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -288,7 +288,7 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
best_i = i;
for ( j = i+1; j < nSize; j++ )
// if ( pArray[j] < pArray[best_i] )
- if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] )
+ if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] ) // list lower priority first (these will be removed first)
best_i = j;
temp = pArray[i];
pArray[i] = pArray[best_i];
@@ -488,7 +488,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
/**Function*************************************************************
- Synopsis [Specialized sorting of flops based on cost.]
+ Synopsis [Specialized sorting of flops based on priority.]
Description []
@@ -497,14 +497,14 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
SeeAlso []
***********************************************************************/
-static inline int Vec_IntSelectSortCostReverseLit( int * pArray, int nSize, Vec_Int_t * vCosts )
+static inline int Vec_IntSelectSortPrioReverseLit( int * pArray, int nSize, Vec_Int_t * vPrios )
{
int i, j, best_i;
for ( i = 0; i < nSize-1; i++ )
{
best_i = i;
for ( j = i+1; j < nSize; j++ )
- if ( Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vCosts, Abc_Lit2Var(pArray[best_i])) )
+ if ( Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[j])) > Vec_IntEntry(vPrios, Abc_Lit2Var(pArray[best_i])) ) // prefer higher priority
best_i = j;
ABC_SWAP( int, pArray[i], pArray[best_i] );
}
@@ -526,7 +526,7 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp
{
int fUseMinAss = 0;
sat_solver * pSat = Pdr_ManFetchSolver( p, k );
- int Order = Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
+ int Order = Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
Vec_Int_t * vLits1 = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
int RetValue, Count = 0, iLit, Lits[2], nLits = Vec_IntSize( vLits1 );
// create free variables
@@ -541,7 +541,7 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp
// if there is only one positive literal, put it in front and always assume
if ( fUseMinAss )
{
- for ( i = 0; i < pCube->nLits; i++ )
+ for ( i = 0; i < pCube->nLits && Count < 2; i++ )
Count += !Abc_LitIsCompl(pCube->Lits[i]);
if ( Count == 1 )
{
@@ -549,7 +549,10 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp
if ( !Abc_LitIsCompl(pCube->Lits[i]) )
break;
assert( i < pCube->nLits );
- ABC_SWAP( int, pCube->Lits[0], pCube->Lits[i] );
+ iLit = pCube->Lits[i];
+ for ( ; i > 0; i-- )
+ pCube->Lits[i] = pCube->Lits[i-1];
+ pCube->Lits[0] = iLit;
}
}
// add clauses for the additional AND-gates
@@ -576,35 +579,51 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp
// perform minimization
if ( fUseMinAss )
{
- if ( Count == 1 )
+ if ( Count == 1 ) // always assume the only positive literal
{
- if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT after assuming the first (mandatory) literal
+ if ( !sat_solver_push(pSat, Vec_IntEntry(vLits1, 0)) ) // UNSAT with the first (mandatory) literal
nLits = 1;
else
- nLits = 1 + sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit );
+ nLits = 1 + sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1)+1, nLits-1, p->pPars->nConfLimit );
sat_solver_pop(pSat); // unassume the first literal
}
else
- nLits = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit );
+ nLits = sat_solver_minimize_assumptions2( pSat, Vec_IntArray(vLits1), nLits, p->pPars->nConfLimit );
Vec_IntShrink( vLits1, nLits );
}
else
{
- int k, Entry;
// try removing one literal at a time in the old-fashioned way
+ int k, Entry;
Vec_Int_t * vTemp = Vec_IntAlloc( nLits );
- for ( i = 0; i < nLits; i++ )
+ for ( i = nLits - 1; i >= 0; i-- )
{
- // check init state
- if ( Pdr_SetIsInit(pCube, i) )
- continue;
+ // if we are about to remove a positive lit, make sure at least one positive lit remains
+ if ( !Abc_LitIsCompl(Vec_IntEntry(vLits1, i)) )
+ {
+ Vec_IntForEachEntry( vLits1, iLit, k )
+ if ( iLit != -1 && k != i && !Abc_LitIsCompl(iLit) )
+ break;
+ if ( k == Vec_IntSize(vLits1) ) // no other positive literals, except the i-th one
+ continue;
+ }
// load remaining literals
Vec_IntClear( vTemp );
Vec_IntForEachEntry( vLits1, Entry, k )
if ( Entry != -1 && k != i )
Vec_IntPush( vTemp, Entry );
+ else if ( Entry != -1 ) // assume opposite literal
+ Vec_IntPush( vTemp, Abc_LitNot(Entry) );
// solve with assumptions
RetValue = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), p->pPars->nConfLimit, 0, 0, 0 );
+ // commit the literal
+ if ( RetValue == l_False )
+ {
+ int LitNot = Abc_LitNot(Vec_IntEntry(vLits1, i));
+ int RetValue = sat_solver_addclause( pSat, &LitNot, &LitNot+1 );
+ assert( RetValue );
+ }
+ // update the clause
if ( RetValue == l_False )
Vec_IntWriteEntry( vLits1, i, -1 );
}
@@ -625,7 +644,7 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp
Vec_IntForEachEntry( vLits1, iLit, i )
if ( !Abc_LitIsCompl(iLit) )
break;
- if ( i == Vec_IntSize(vLits1) )
+ if ( i == Vec_IntSize(vLits1) ) // has no positive literals
{
// find positive lit in the cube
for ( i = 0; i < pCube->nLits; i++ )
@@ -633,7 +652,10 @@ int Pdr_ManGeneralize2( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** pp
break;
assert( i < pCube->nLits );
Vec_IntPush( vLits1, pCube->Lits[i] );
+// printf( "-" );
}
+// else
+// printf( "+" );
}
// create a subset cube
*ppCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits1), Vec_IntSize(vLits1) );
@@ -664,7 +686,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
// if there is no induction, return
*ppCubeMin = NULL;
if ( p->pPars->fFlopOrder )
- Vec_IntSelectSortCostReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
+ Vec_IntSelectSortPrioReverseLit( pCube->Lits, pCube->nLits, p->vPrio );
RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0, 1 );
if ( p->pPars->fFlopOrder )
Vec_IntSelectSort( pCube->Lits, pCube->nLits );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index aad0df51..fe7e65fe 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -2187,8 +2187,8 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int
return (int)(status != l_False); // return 1 if the problem is not UNSAT
}
assert( nLits >= 2 );
- nLitsR = nLits / 2;
- nLitsL = nLits - nLitsR;
+ nLitsL = nLits / 2;
+ nLitsR = nLits - nLitsL;
// assume the left lits
for ( i = 0; i < nLitsL; i++ )
if ( !sat_solver_push(s, pLits[i]) )
@@ -2202,7 +2202,7 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int
for ( i = 0; i < nLitsL; i++ )
sat_solver_pop(s);
// swap literals
- assert( nResL <= nLitsL );
+// assert( nResL <= nLitsL );
// for ( i = 0; i < nResL; i++ )
// ABC_SWAP( int, pLits[i], pLits[nLitsL+i] );
veci_resize( &s->temp_clause, 0 );
@@ -2227,6 +2227,94 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int
return nResL + nResR;
}
+// This is a specialized version of the above procedure with several custom changes:
+// - makes sure that at least one of the marked literals is preserved in the clause
+// - sets literals to zero when they do not have to be used
+// - sets literals to zero for disproved variables
+int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit )
+{
+ int i, k, nLitsL, nLitsR, nResL, nResR;
+ if ( nLits == 1 )
+ {
+ // since the problem is UNSAT, we will try to solve it without assuming the last literal
+ // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+ int RetValue = 1, LitNot = Abc_LitNot(pLits[0]);
+ int status = l_False;
+ int Temp = s->nConfLimit;
+ s->nConfLimit = nConfLimit;
+
+ RetValue = sat_solver_push( s, LitNot ); assert( RetValue );
+ status = sat_solver_solve_internal( s );
+ sat_solver_pop( s );
+
+ // if the problem is UNSAT, add clause
+ if ( status == l_False )
+ {
+ RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+ assert( RetValue );
+ }
+
+ s->nConfLimit = Temp;
+ return (int)(status != l_False); // return 1 if the problem is not UNSAT
+ }
+ assert( nLits >= 2 );
+ nLitsL = nLits / 2;
+ nLitsR = nLits - nLitsL;
+ // assume the left lits
+ for ( i = 0; i < nLitsL; i++ )
+ if ( !sat_solver_push(s, pLits[i]) )
+ {
+ for ( k = i; k >= 0; k-- )
+ sat_solver_pop(s);
+
+ // add clauses for these literal
+ for ( k = i+1; k > nLitsL; k++ )
+ {
+ int LitNot = Abc_LitNot(pLits[i]);
+ int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+ assert( RetValue );
+ }
+
+ return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
+ }
+ // solve for the right lits
+ nResL = sat_solver_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit );
+ for ( i = 0; i < nLitsL; i++ )
+ sat_solver_pop(s);
+ // swap literals
+// assert( nResL <= nLitsL );
+ veci_resize( &s->temp_clause, 0 );
+ for ( i = 0; i < nLitsL; i++ )
+ veci_push( &s->temp_clause, pLits[i] );
+ for ( i = 0; i < nResL; i++ )
+ pLits[i] = pLits[nLitsL+i];
+ for ( i = 0; i < nLitsL; i++ )
+ pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
+ // assume the right lits
+ for ( i = 0; i < nResL; i++ )
+ if ( !sat_solver_push(s, pLits[i]) )
+ {
+ for ( k = i; k >= 0; k-- )
+ sat_solver_pop(s);
+
+ // add clauses for these literal
+ for ( k = i+1; k > nResL; k++ )
+ {
+ int LitNot = Abc_LitNot(pLits[i]);
+ int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
+ assert( RetValue );
+ }
+
+ return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
+ }
+ // solve for the left lits
+ nResR = sat_solver_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit );
+ for ( i = 0; i < nResL; i++ )
+ sat_solver_pop(s);
+ return nResL + nResR;
+}
+
+
int sat_solver_nvars(sat_solver* s)
{
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index ac0b6e8d..5191b2cd 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -51,6 +51,7 @@ extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT
extern int sat_solver_solve_internal(sat_solver* s);
extern int sat_solver_solve_lexsat(sat_solver* s, int * pLits, int nLits);
extern int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int nConfLimit );
+extern int sat_solver_minimize_assumptions2( sat_solver* s, int * pLits, int nLits, int nConfLimit );
extern int sat_solver_push(sat_solver* s, int p);
extern void sat_solver_pop(sat_solver* s);
extern void sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 17:59:56 +0000