summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2017-09-03 08:07:28 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2017-09-03 08:07:28 -0700
commit5e2bfe36ff267e4407b2a6b8126de622d5892395 (patch)
treec1114089d70d9f003a20f3999d145b5d6d8c5558
parent1d44f420392d40a71c907a0ad7636983f2441f30 (diff)
downloadabc-5e2bfe36ff267e4407b2a6b8126de622d5892395.tar.gz
abc-5e2bfe36ff267e4407b2a6b8126de622d5892395.tar.bz2
abc-5e2bfe36ff267e4407b2a6b8126de622d5892395.zip
Adding minimize_assumptions to Satoko.
-rw-r--r--src/sat/satoko/satoko.h1
-rw-r--r--src/sat/satoko/solver_api.c58
2 files changed, 57 insertions, 2 deletions
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index 5c0de7ad..fb646c01 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -101,6 +101,7 @@ extern int satoko_simplify(satoko_t *);
extern int satoko_solve(satoko_t *);
extern int satoko_solve_assumptions(satoko_t *s, int * plits, int nlits);
extern int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim);
+extern int satoko_minimize_assumptions(satoko_t *s, int * plits, int nlits, int nconflim);
extern void satoko_mark_cone(satoko_t *, int *, int);
extern void satoko_unmark_cone(satoko_t *, int *, int);
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 20217e54..975066a4 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -287,7 +287,7 @@ int satoko_add_clause(solver_t *s, int *lits, int size)
void satoko_assump_push(solver_t *s, int lit)
{
- assert(lit2var(lit) < satoko_varnum(s));
+ assert(lit2var(lit) < (unsigned)satoko_varnum(s));
// printf("[Satoko] Push assumption: %d\n", lit);
vec_uint_push_back(s->assumptions, lit);
vec_char_assign(s->polarity, lit2var(lit), lit_polarity(lit));
@@ -354,11 +354,65 @@ int satoko_solve_assumptions(solver_t *s, int * plits, int nlits)
int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim)
{
int temp = s->opts.conf_limit, status;
- s->opts.conf_limit = nconflim;
+ s->opts.conf_limit = s->stats.n_conflicts + nconflim;
status = satoko_solve_assumptions(s, plits, nlits);
s->opts.conf_limit = temp;
return status;
}
+int satoko_minimize_assumptions(satoko_t * s, int * plits, int nlits, int nconflim)
+{
+ int i, nlitsL, nlitsR, nresL, nresR, status;
+ if ( nlits == 1 )
+ {
+ // since the problem is UNSAT, we try to solve it without assuming the last literal
+ // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
+ status = satoko_solve_assumptions_limit( s, NULL, 0, nconflim );
+ return (int)(status != SATOKO_UNSAT); // 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++ )
+ satoko_assump_push(s, plits[i]);
+ // solve with these assumptions
+ status = satoko_solve_assumptions_limit( s, NULL, 0, nconflim );
+ if ( status == SATOKO_UNSAT ) // these are enough
+ {
+ for ( i = 0; i < nlitsL; i++ )
+ satoko_assump_pop(s);
+ return satoko_minimize_assumptions( s, plits, nlitsL, nconflim );
+ }
+ // these are not enoguh
+ // solve for the right lits
+ nresL = nlitsR == 1 ? 1 : satoko_minimize_assumptions( s, plits + nlitsL, nlitsR, nconflim );
+ for ( i = 0; i < nlitsL; i++ )
+ satoko_assump_pop(s);
+ // swap literals
+ vec_uint_clear(s->temp_lits);
+ for ( i = 0; i < nlitsL; i++ )
+ vec_uint_push_back(s->temp_lits, plits[i]);
+ for ( i = 0; i < nresL; i++ )
+ plits[i] = plits[nlitsL+i];
+ for ( i = 0; i < nlitsL; i++ )
+ plits[nresL+i] = vec_uint_at(s->temp_lits, i);
+ // assume the right lits
+ for ( i = 0; i < nresL; i++ )
+ satoko_assump_push(s, plits[i]);
+ // solve with these assumptions
+ status = satoko_solve_assumptions_limit( s, NULL, 0, nconflim );
+ if ( status == SATOKO_UNSAT ) // these are enough
+ {
+ for ( i = 0; i < nresL; i++ )
+ satoko_assump_pop(s);
+ return nresL;
+ }
+ // solve for the left lits
+ nresR = nlitsL == 1 ? 1 : satoko_minimize_assumptions( s, plits + nresL, nlitsL, nconflim );
+ for ( i = 0; i < nresL; i++ )
+ satoko_assump_pop(s);
+ return nresL + nresR;
+}
int satoko_final_conflict(solver_t *s, int **out)
{