From bd9b7d64e1131f45699a5a4b20b4bf44795da857 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 1 Mar 2017 13:59:23 -0800 Subject: Adding efficient procedure to minimize the set of assumptions. --- src/sat/bsat/satSolver.c | 52 ++++++++++++++++++++++++++++++++++++++++++++++++ src/sat/bsat/satSolver.h | 1 + 2 files changed, 53 insertions(+) (limited to 'src/sat/bsat') diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index df9ada8e..3d24161e 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2168,6 +2168,58 @@ int sat_solver_solve_lexsat( sat_solver* s, int * pLits, int nLits ) return status; } +// This procedure is called on a set of assumptions to minimize their number. +// The procedure relies on the fact that the current set of assumptions is UNSAT. +// It receives and returns SAT solver without assumptions. It returns the number +// of assumptions after minimization. The set of assumptions is returned in pLits. +int sat_solver_minimize_assumptions( 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 + // the result is UNSAT, the last literal can be dropped; otherwise, it is needed + int status = l_False; + int Temp = s->nConfLimit; + s->nConfLimit = nConfLimit; + status = sat_solver_solve_internal( s ); + s->nConfLimit = Temp; + return (int)(status != l_False); // return 1 if the problem is not UNSAT + } + assert( nLits >= 2 ); + nLitsR = nLits / 2; + nLitsL = nLits - nLitsR; + // 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); + return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit ); + } + // solve for the right lits + nResL = sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit ); + for ( i = 0; i < nLitsL; i++ ) + sat_solver_pop(s); + // swap literals + assert( nResL <= nLitsL ); + for ( i = 0; i < nResL; i++ ) + ABC_SWAP( int, pLits[i], pLits[nLitsL+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); + return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit ); + } + // solve for the left lits + nResR = sat_solver_minimize_assumptions( 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 5a8483c1..ac0b6e8d 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -50,6 +50,7 @@ extern int sat_solver_simplify(sat_solver* s); extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal); 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_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); -- cgit v1.2.3 From 7747d89c905a85c8ab6c03e987ad9747032d919d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 1 Mar 2017 20:29:09 -0800 Subject: Adding alternative generalization procedure. --- src/sat/bsat/satSolver.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/sat/bsat') diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 3d24161e..47fba5e3 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2178,7 +2178,7 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int if ( nLits == 1 ) { // since the problem is UNSAT, we will try to solve it without assuming the last literal - // the result is UNSAT, the last literal can be dropped; otherwise, it is needed + // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed int status = l_False; int Temp = s->nConfLimit; s->nConfLimit = nConfLimit; -- cgit v1.2.3 From 160d1311c9ca687cffe0d9ee6752afdc3f43864c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 11:10:16 -0800 Subject: Adding efficient procedure to minimize the set of assumptions (improved literal reordering). --- src/sat/bsat/satSolver.c | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'src/sat/bsat') diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 47fba5e3..aad0df51 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2203,8 +2203,15 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int sat_solver_pop(s); // swap literals assert( nResL <= nLitsL ); +// for ( i = 0; i < nResL; i++ ) +// ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); + 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++ ) - ABC_SWAP( int, pLits[i], pLits[nLitsL+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]) ) -- cgit v1.2.3 From ff88edd6645bebeb2cbe63b02e5db62b3e140d53 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Mar 2017 13:01:32 -0800 Subject: Adding alternative generalization procedure. --- src/sat/bsat/satSolver.c | 94 ++++++++++++++++++++++++++++++++++++++++++++++-- src/sat/bsat/satSolver.h | 1 + 2 files changed, 92 insertions(+), 3 deletions(-) (limited to 'src/sat/bsat') 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); -- cgit v1.2.3