From 3df049f37df1f02feaf7585a04f2e07e5fd33fbc Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Mon, 28 Aug 2017 10:59:30 +0200 Subject: [Satoko] Correcting bug found when integrating with pdr. The head of the propagation queue was not begin properly reset. Adding some debugging functions. --- src/sat/satoko/cnf_reader.c | 3 +- src/sat/satoko/solver.c | 87 +++++++++++++++++++++++++++++++++++---------- src/sat/satoko/solver.h | 5 +++ src/sat/satoko/solver_api.c | 28 +++++++++++++-- 4 files changed, 102 insertions(+), 21 deletions(-) (limited to 'src/sat/satoko') diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c index 8223affd..48a0b068 100644 --- a/src/sat/satoko/cnf_reader.c +++ b/src/sat/satoko/cnf_reader.c @@ -142,8 +142,9 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver) } read_clause(&token, lits); if (!satoko_add_clause(p, (int*)vec_uint_data(lits), vec_uint_size(lits))) { + printf("Unable to add clause: "); vec_uint_print(lits); - return 0; + return SATOKO_ERR; } } } diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index 51befd16..b35574ab 100644 --- a/src/sat/satoko/solver.c +++ b/src/sat/satoko/solver.c @@ -362,14 +362,16 @@ static inline void solver_handle_conflict(solver_t *s, unsigned confl_cref) static inline void solver_analyze_final(solver_t *s, unsigned lit) { - int i; + unsigned i; + // printf("[Satoko] Analize final..\n"); + // printf("[Satoko] Conflicting lit: %d\n", lit); vec_uint_clear(s->final_conflict); vec_uint_push_back(s->final_conflict, lit); if (solver_dlevel(s) == 0) return; vec_char_assign(s->seen, lit2var(lit), 1); - for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, 0); i--) { + for (i = vec_uint_size(s->trail); i --> vec_uint_at(s->trail_lim, 0);) { unsigned var = lit2var(vec_uint_at(s->trail, i)); if (vec_char_at(s->seen, var)) { @@ -385,10 +387,11 @@ static inline void solver_analyze_final(solver_t *s, unsigned lit) vec_char_assign(s->seen, lit2var(clause->data[j].lit), 1); } } - vec_char_assign(s->seen, var, 0); + vec_char_assign(s->seen, var, 0); } } vec_char_assign(s->seen, lit2var(lit), 0); + // solver_debug_check_unsat(s); } static inline void solver_garbage_collect(solver_t *s) @@ -511,12 +514,12 @@ unsigned solver_clause_create(solver_t *s, vec_uint_t *lits, unsigned f_learnt) void solver_cancel_until(solver_t *s, unsigned level) { - int i; + unsigned i; if (solver_dlevel(s) <= level) return; - for (i = (int) vec_uint_size(s->trail) - 1; i >= (int) vec_uint_at(s->trail_lim, level); i--) { - unsigned var = lit2var(vec_uint_at(s->trail, (unsigned) i)); + for (i = vec_uint_size(s->trail); i --> vec_uint_at(s->trail_lim, level);) { + unsigned var = lit2var(vec_uint_at(s->trail, i)); vec_char_assign(s->polarity, var, vec_char_at(s->assigns, var)); vec_char_assign(s->assigns, var, VAR_UNASSING); @@ -636,6 +639,7 @@ char solver_search(solver_t *s) b_queue_clean(s->bq_lbd); solver_handle_conflict(s, confl_cref); } else { + // solver_debug_check_clauses(s); /* No conflict */ unsigned next_lit; @@ -675,8 +679,10 @@ char solver_search(solver_t *s) if (next_lit == UNDEF) { s->stats.n_decisions++; next_lit = solver_decide(s); - if (next_lit == UNDEF) + if (next_lit == UNDEF) { + // solver_debug_check(s, SATOKO_SAT); return SATOKO_SAT; + } } solver_new_decision(s, next_lit); } @@ -684,23 +690,66 @@ char solver_search(solver_t *s) } //===------------------------------------------------------------------------=== -// Debug procedure +// Debug procedures //===------------------------------------------------------------------------=== -void solver_debug_check(solver_t *s, int result) +void solver_debug_check_trail(solver_t *s) { - unsigned cref, i; + unsigned i; unsigned *array; - - printf("Checking for trail(%u) inconsistencies...", vec_uint_size(s->trail)); - array = vec_uint_data(s->trail); - for (i = 1; i < vec_uint_size(s->trail); i++) + vec_uint_t *trail_dup = vec_uint_alloc(0); + fprintf(stdout, "[Satoko] Checking for trail(%u) inconsistencies...\n", vec_uint_size(s->trail)); + vec_uint_duplicate(trail_dup, s->trail); + vec_uint_sort(trail_dup, 1); + array = vec_uint_data(trail_dup); + for (i = 1; i < vec_uint_size(trail_dup); i++) { if (array[i - 1] == lit_compl(array[i])) { - printf("Inconsistent trail: %u %u\n", array[i - 1], array[i]); + fprintf(stdout, "[Satoko] Inconsistent trail: %u %u\n", array[i - 1], array[i]); + assert(0); return; } - printf(" TRAIL OK\n"); + } + for (i = 0; i < vec_uint_size(trail_dup); i++) { + if (var_value(s, lit2var(array[i])) != lit_polarity(array[i])) { + fprintf(stdout, "[Satoko] Inconsistent trail assignment: %u, %u\n", vec_char_at(s->assigns, lit2var(array[i])), array[i]); + assert(0); + return; + } + } + fprintf(stdout, "[Satoko] Trail OK.\n"); + vec_uint_print(trail_dup); + vec_uint_free(trail_dup); - printf("Checking clauses... \n"); +} + +void solver_debug_check_clauses(solver_t *s) +{ + unsigned cref, i; + + fprintf(stdout, "[Satoko] Checking clauses (%d)...\n", vec_uint_size(s->originals)); + vec_uint_foreach(s->originals, cref, i) { + unsigned j; + struct clause *clause = clause_fetch(s, cref); + for (j = 0; j < clause->size; j++) { + if (vec_uint_find(s->trail, lit_compl(clause->data[j].lit))) { + continue; + } + break; + } + if (j == clause->size) { + vec_uint_print(s->trail); + fprintf(stdout, "[Satoko] FOUND UNSAT CLAUSE]: (%d) ", i); + clause_print(clause); + assert(0); + } + } + fprintf(stdout, "[Satoko] All SAT - OK\n"); +} + +void solver_debug_check(solver_t *s, int result) +{ + unsigned cref, i; + solver_debug_check_trail(s); + fprintf(stdout, "[Satoko] Checking clauses (%d)... \n", vec_uint_size(s->originals)); vec_uint_foreach(s->originals, cref, i) { unsigned j; struct clause *clause = clause_fetch(s, cref); @@ -710,10 +759,12 @@ void solver_debug_check(solver_t *s, int result) } } if (result == SATOKO_SAT && j == clause->size) { - printf("FOUND UNSAT CLAUSE!!!!\n"); + fprintf(stdout, "[Satoko] FOUND UNSAT CLAUSE: (%d) ", i); clause_print(clause); + assert(0); } } + fprintf(stdout, "[Satoko] All SAT - OK\n"); } ABC_NAMESPACE_IMPL_END diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index d6f7d75e..ee7b84e2 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -99,6 +99,7 @@ struct solver_t_ { unsigned book_cdb; /* Bookmark clause database size */ unsigned book_vars; /* Bookmark number of variables */ unsigned book_trail; /* Bookmark trail size */ + // unsigned book_qhead; /* Bookmark propagation queue head */ /* Temporary data used for solving cones */ vec_char_t *marks; @@ -118,7 +119,11 @@ extern unsigned solver_clause_create(solver_t *, vec_uint_t *, unsigned); extern char solver_search(solver_t *); extern void solver_cancel_until(solver_t *, unsigned); extern unsigned solver_propagate(solver_t *); + +/* Debuging */ extern void solver_debug_check(solver_t *, int); +extern void solver_debug_check_trail(solver_t *); +extern void solver_debug_check_clauses(solver_t *); //===------------------------------------------------------------------------=== // Inline var/lit functions diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 8784a761..d404992e 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -43,6 +43,11 @@ static inline int clause_is_satisfied(solver_t *s, struct clause *clause) return SATOKO_ERR; } +static inline void solver_clean_stats(solver_t *s) +{ + memset(&(s->stats), 0, sizeof(struct satoko_stats)); +} + static inline void print_opts(solver_t *s) { printf( "+-[ BLACK MAGIC - PARAMETERS ]-+\n"); @@ -282,12 +287,15 @@ int satoko_add_clause(solver_t *s, int *lits, int size) void satoko_assump_push(solver_t *s, int lit) { + assert(lit2var(lit) < solver_varnum(s)); + // printf("[Satoko] Push assumption: %d\n", lit); vec_uint_push_back(s->assumptions, lit); } void satoko_assump_pop(solver_t *s) { assert(vec_uint_size(s->assumptions) > 0); + // printf("[Satoko] Pop assumption: %d\n", vec_uint_pop_back(s->assumptions)); vec_uint_pop_back(s->assumptions); solver_cancel_until(s, vec_uint_size(s->assumptions)); } @@ -297,6 +305,7 @@ int satoko_solve(solver_t *s) int status = SATOKO_UNDEC; assert(s); + solver_clean_stats(s); //if (s->opts.verbose) // print_opts(s); if (s->status == SATOKO_ERR) { @@ -327,6 +336,12 @@ int satoko_solve(solver_t *s) int satoko_solve_assumptions(solver_t *s, int * plits, int nlits) { int i, status; + // printf("\n[Satoko] Solve with assumptions.. (%d)\n", vec_uint_size(s->assumptions)); + // printf("[Satoko] + Variables: %d\n", solver_varnum(s)); + // printf("[Satoko] + Clauses: %d\n", solver_clausenum(s)); + // printf("[Satoko] + Trail size: %d\n", vec_uint_size(s->trail)); + // printf("[Satoko] + Queue head: %d\n", s->i_qhead); + // solver_debug_check_trail(s); for ( i = 0; i < nlits; i++ ) satoko_assump_push( s, plits[i] ); status = satoko_solve( s ); @@ -357,28 +372,33 @@ satoko_stats_t satoko_stats(satoko_t *s) void satoko_bookmark(satoko_t *s) { + // printf("[Satoko] Bookmark.\n"); assert(s->status == SATOKO_OK); assert(solver_dlevel(s) == 0); s->book_cl_orig = vec_uint_size(s->originals); s->book_cl_lrnt = vec_uint_size(s->learnts); s->book_vars = vec_char_size(s->assigns); s->book_trail = vec_uint_size(s->trail); + // s->book_qhead = s->i_qhead; s->opts.no_simplify = 1; } void satoko_unbookmark(satoko_t *s) { + // printf("[Satoko] Unbookmark.\n"); assert(s->status == SATOKO_OK); s->book_cl_orig = 0; s->book_cl_lrnt = 0; s->book_cdb = 0; s->book_vars = 0; s->book_trail = 0; + // s->book_qhead = 0; s->opts.no_simplify = 0; } void satoko_reset(satoko_t *s) { + // printf("[Satoko] Reset.\n"); vec_uint_clear(s->assumptions); vec_uint_clear(s->final_conflict); cdb_clear(s->all_clauses); @@ -412,6 +432,7 @@ void satoko_reset(satoko_t *s) s->book_cdb = 0; s->book_vars = 0; s->book_trail = 0; + s->i_qhead = 0; } void satoko_rollback(satoko_t *s) @@ -421,13 +442,13 @@ void satoko_rollback(satoko_t *s) unsigned n_learnts = vec_uint_size(s->learnts) - s->book_cl_lrnt; struct clause **cl_to_remove; + // printf("[Satoko] rollback.\n"); assert(s->status == SATOKO_OK); assert(solver_dlevel(s) == 0); if (!s->book_vars) { satoko_reset(s); return; } - cl_to_remove = satoko_alloc(struct clause *, n_originals + n_learnts); /* Mark clauses */ vec_uint_foreach_start(s->originals, cref, i, s->book_cl_orig) @@ -446,6 +467,7 @@ void satoko_rollback(satoko_t *s) vec_wl_at(s->watches, i)->size = 0; vec_wl_at(s->watches, i)->n_bin = 0; } + // s->i_qhead = s->book_qhead; s->watches->size = s->book_vars; vec_act_shrink(s->activity, s->book_vars); vec_uint_shrink(s->levels, s->book_vars); @@ -464,6 +486,7 @@ void satoko_rollback(satoko_t *s) s->book_cl_lrnt = 0; s->book_vars = 0; s->book_trail = 0; + // s->book_qhead = 0; } void satoko_mark_cone(satoko_t *s, int * pvars, int n_vars) @@ -510,7 +533,7 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var) fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig); for (i = 0; i < vec_char_size(s->assigns); i++) if ( var_value(s, i) != VAR_UNASSING ) - fprintf(file, "%d\n", var_value(s, i) == LIT_FALSE ? -(int)(i + !zero_var) : i + !zero_var); + fprintf(file, "%d %d\n", var_value(s, i) == LIT_FALSE ? -(int)(i + !zero_var) : i + !zero_var, zero_var ? : 0); array = vec_uint_data(s->originals); for (i = 0; i < vec_uint_size(s->originals); i++) @@ -521,6 +544,7 @@ void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var) for (i = 0; i < n_lrnts; i++) clause_dump(file, clause_fetch(s, array[i]), !zero_var); } + fclose(file); } -- cgit v1.2.3