diff options
Diffstat (limited to 'src/sat/satoko/solver.c')
| -rw-r--r-- | src/sat/satoko/solver.c | 704 |
1 files changed, 704 insertions, 0 deletions
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c new file mode 100644 index 00000000..b2861bad --- /dev/null +++ b/src/sat/satoko/solver.c @@ -0,0 +1,704 @@ +//===--- solver.c -----------------------------------------------------------=== +// +// satoko: Satisfiability solver +// +// This file is distributed under the BSD 2-Clause License. +// See LICENSE for details. +// +//===------------------------------------------------------------------------=== +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <math.h> + +#include "act_clause.h" +#include "act_var.h" +#include "solver.h" +#include "utils/heap.h" +#include "utils/mem.h" +#include "utils/sort.h" + +#include "misc/util/abc_global.h" +ABC_NAMESPACE_IMPL_START + +//===------------------------------------------------------------------------=== +// Lit funtions +//===------------------------------------------------------------------------=== +/** + * A literal is said to be redundant in a given clause if and only if all + * variables in its reason are either present in that clause or (recursevely) + * redundant. + */ +static inline int lit_is_removable(solver_t* s, unsigned lit, unsigned min_level) +{ + unsigned top = vec_uint_size(s->tagged); + + assert(lit_reason(s, lit) != UNDEF); + vec_uint_clear(s->stack); + vec_uint_push_back(s->stack, lit2var(lit)); + while (vec_uint_size(s->stack)) { + unsigned i; + unsigned var = vec_uint_pop_back(s->stack); + struct clause *c = clause_read(s, var_reason(s, var)); + unsigned *lits = &(c->data[0].lit); + + assert(var_reason(s, var) != UNDEF); + if (c->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) { + assert(lit_value(s, lits[1]) == LIT_TRUE); + mkt_swap(unsigned, lits[0], lits[1]); + } + + /* Check scan the literals of the reason clause. + * The first literal is skiped because is the literal itself. */ + for (i = 1; i < c->size; i++) { + var = lit2var(lits[i]); + + /* Check if the variable has already been seen or if it + * was assinged a value at the decision level 0. In a + * positive case, there is no need to look any further */ + if (vec_char_at(s->seen, var) || var_dlevel(s, var) == 0) + continue; + + /* If the variable has a reason clause and if it was + * assingned at a 'possible' level, then we need to + * check if it is recursively redundant, otherwise the + * literal being checked is not redundant */ + if (var_reason(s, var) != UNDEF && ((1 << (var_dlevel(s, var) & 31)) & min_level)) { + vec_uint_push_back(s->stack, var); + vec_uint_push_back(s->tagged, var); + vec_char_assign(s->seen, var, 1); + } else { + vec_uint_foreach_start(s->tagged, var, i, top) + vec_char_assign(s->seen, var, 0); + vec_uint_shrink(s->tagged, top); + return 0; + } + } + } + return 1; +} + +//===------------------------------------------------------------------------=== +// Clause functions +//===------------------------------------------------------------------------=== +/* Calculate clause LBD (Literal Block Distance): + * - It's the number of variables in the final conflict clause that come from + * different decision levels + */ +static inline unsigned clause_clac_lbd(solver_t *s, unsigned *lits, unsigned size) +{ + unsigned i; + unsigned lbd = 0; + + s->cur_stamp++; + for (i = 0; i < size; i++) { + unsigned level = lit_dlevel(s, lits[i]); + if (vec_uint_at(s->stamps, level) != s->cur_stamp) { + vec_uint_assign(s->stamps, level, s->cur_stamp); + lbd++; + } + } + return lbd; +} + +static inline void clause_bin_resolution(solver_t *s, vec_uint_t *clause_lits) +{ + unsigned *lits = vec_uint_data(clause_lits); + unsigned counter, sz, i; + unsigned lit; + unsigned neg_lit = lit_neg(lits[0]); + struct watcher *w; + + s->cur_stamp++; + vec_uint_foreach(clause_lits, lit, i) + vec_uint_assign(s->stamps, lit2var(lit), s->cur_stamp); + + counter = 0; + watch_list_foreach(s->bin_watches, w, neg_lit) { + unsigned imp_lit = w->blocker; + if (vec_uint_at(s->stamps, lit2var(imp_lit)) == s->cur_stamp && + lit_value(s, imp_lit) == LIT_TRUE) { + counter++; + vec_uint_assign(s->stamps, lit2var(imp_lit), (s->cur_stamp - 1)); + } + } + if (counter > 0) { + sz = vec_uint_size(clause_lits) - 1; + for (i = 1; i < vec_uint_size(clause_lits) - counter; i++) + if (vec_uint_at(s->stamps, lit2var(lits[i])) != s->cur_stamp) { + mkt_swap(unsigned, lits[i], lits[sz]); + i--; + sz--; + } + vec_uint_shrink(clause_lits, vec_uint_size(clause_lits) - counter); + } +} + +static inline void clause_minimize(solver_t *s, vec_uint_t *clause_lits) +{ + unsigned i, j; + unsigned *lits = vec_uint_data(clause_lits); + unsigned min_level = 0; + unsigned clause_size; + + for (i = 1; i < vec_uint_size(clause_lits); i++) { + unsigned level = lit_dlevel(s, lits[i]); + min_level |= 1 << (level & 31); + } + + /* Remove reduntant literals */ + vec_uint_foreach(clause_lits, i, j) + vec_uint_push_back(s->tagged, lit2var(i)); + for (i = j = 1; i < vec_uint_size(clause_lits); i++) + if (lit_reason(s, lits[i]) == UNDEF || !lit_is_removable(s, lits[i], min_level)) + lits[j++] = lits[i]; + vec_uint_shrink(clause_lits, j); + + /* Binary Resolution */ + clause_size = vec_uint_size(clause_lits); + if (clause_size <= s->opts.clause_max_sz_bin_resol && + clause_clac_lbd(s, lits, clause_size) <= s->opts.clause_min_lbd_bin_resol) + clause_bin_resolution(s, clause_lits); +} + +static inline void clause_realloc(struct cdb *dest, struct cdb *src, unsigned *cref) +{ + unsigned new_cref; + struct clause *new_clause; + struct clause *old_clause = cdb_handler(src, *cref); + + if (old_clause->f_reallocd) { + *cref = (unsigned) old_clause->size; + return; + } + new_cref = cdb_append(dest, 3 + old_clause->f_learnt + old_clause->size); + new_clause = cdb_handler(dest, new_cref); + memcpy(new_clause, old_clause, (3 + old_clause->f_learnt + old_clause->size) * 4); + old_clause->f_reallocd = 1; + old_clause->size = (unsigned) new_cref; + *cref = new_cref; +} + +//===------------------------------------------------------------------------=== +// Solver internal functions +//===------------------------------------------------------------------------=== +static inline unsigned solver_decide(solver_t *s) +{ + unsigned next_var = UNDEF; + + while (next_var == UNDEF || var_value(s, next_var) != VAR_UNASSING) { + if (heap_size(s->var_order) == 0) { + next_var = UNDEF; + return UNDEF; + } else + next_var = heap_remove_min(s->var_order); + } + return var2lit(next_var, vec_char_at(s->polarity, next_var)); +} + +static inline void solver_new_decision(solver_t *s, unsigned lit) +{ + assert(var_value(s, lit2var(lit)) == VAR_UNASSING); + vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail)); + solver_enqueue(s, lit, UNDEF); +} + +/* Calculate Backtrack Level from the learnt clause */ +static inline unsigned solver_calc_bt_level(solver_t *s, vec_uint_t *learnt) +{ + unsigned i, tmp; + unsigned i_max = 1; + unsigned *lits = vec_uint_data(learnt); + unsigned max = lit_dlevel(s, lits[1]); + + if (vec_uint_size(learnt) == 1) + return 0; + for (i = 2; i < vec_uint_size(learnt); i++) { + if (lit_dlevel(s, lits[i]) > max) { + max = lit_dlevel(s, lits[i]); + i_max = i; + } + } + tmp = lits[1]; + lits[1] = lits[i_max]; + lits[i_max] = tmp; + return lit_dlevel(s, lits[1]); +} + +/** + * Most books and papers explain conflict analysis and the calculation of the + * 1UIP (first Unique Implication Point) using an implication graph. This + * function, however, do not explicity constructs the graph! It inspects the + * trail in reverse and figure out which literals should be added to the + * to-be-learnt clause using the reasons of each assignment. + * + * cur_lit: current literal being analyzed. + * n_paths: number of unprocessed paths from conlfict node to the current + * literal being analyzed (cur_lit). + * + * This functions performs a backward BFS (breadth-first search) for 1UIP node. + * The trail works as the BFS queue. The counter of unprocessed but seen + * variables (n_paths) allows us to identify when 'cur_lit' is the closest + * cause of conflict. + * + * When 'n_paths' reaches zero it means there are no unprocessed reverse paths + * back from the conflict node to 'cur_lit' - meaning it is the 1UIP decision + * variable. + * + */ +static inline void solver_analyze(solver_t *s, unsigned cref, vec_uint_t *learnt, + unsigned *bt_level, unsigned *lbd) +{ + unsigned i; + unsigned *trail = vec_uint_data(s->trail); + unsigned idx = vec_uint_size(s->trail) - 1; + unsigned n_paths = 0; + unsigned p = UNDEF; + unsigned var; + + vec_uint_push_back(learnt, UNDEF); + do { + struct clause *clause; + unsigned *lits; + unsigned j; + + assert(cref != UNDEF); + clause = clause_read(s, cref); + lits = &(clause->data[0].lit); + + if (p != UNDEF && clause->size == 2 && lit_value(s, lits[0]) == LIT_FALSE) { + assert(lit_value(s, lits[1]) == LIT_TRUE); + mkt_swap(unsigned, lits[0], lits[1] ); + } + + if (clause->f_learnt) + clause_act_bump(s, clause); + + if (clause->f_learnt && clause->lbd > 2) { + unsigned n_levels = clause_clac_lbd(s, lits, clause->size); + if (n_levels + 1 < clause->lbd) { + if (clause->lbd <= s->opts.lbd_freeze_clause) + clause->f_deletable = 0; + clause->lbd = n_levels; + } + } + + for (j = (p == UNDEF ? 0 : 1); j < clause->size; j++) { + var = lit2var(lits[j]); + if (vec_char_at(s->seen, var) || var_dlevel(s, var) == 0) + continue; + vec_char_assign(s->seen, var, 1); + var_act_bump(s, var); + if (var_dlevel(s, var) == solver_dlevel(s)) { + n_paths++; + if (var_reason(s, var) != UNDEF && clause_read(s, var_reason(s, var))->f_learnt) + vec_uint_push_back(s->last_dlevel, var); + } else + vec_uint_push_back(learnt, lits[j]); + } + + while (!vec_char_at(s->seen, lit2var(trail[idx--]))); + + p = trail[idx + 1]; + cref = lit_reason(s, p); + vec_char_assign(s->seen, lit2var(p), 0); + n_paths--; + } while (n_paths > 0); + + vec_uint_data(learnt)[0] = lit_neg(p); + clause_minimize(s, learnt); + *bt_level = solver_calc_bt_level(s, learnt); + *lbd = clause_clac_lbd(s, vec_uint_data(learnt), vec_uint_size(learnt)); + + if (vec_uint_size( s->last_dlevel) > 0) { + vec_uint_foreach(s->last_dlevel, var, i) { + if (clause_read(s, var_reason(s, var))->lbd < *lbd) + var_act_bump(s, var); + } + vec_uint_clear(s->last_dlevel); + } + vec_uint_foreach(s->tagged, var, i) + vec_char_assign(s->seen, var, 0); + vec_uint_clear(s->tagged); +} + +static inline int solver_rst(solver_t *s) +{ + return b_queue_is_valid(s->bq_lbd) && + (((long long)b_queue_avg(s->bq_lbd) * s->opts.f_rst) > (s->sum_lbd / s->stats.n_conflicts)); +} + +static inline int solver_block_rst(solver_t *s) +{ + return s->stats.n_conflicts > s->opts.fst_block_rst && + b_queue_is_valid(s->bq_lbd) && + (vec_uint_size(s->trail) > (s->opts.b_rst * (long long)b_queue_avg(s->bq_trail))); +} + +static inline void solver_handle_conflict(solver_t *s, unsigned confl_cref) +{ + unsigned bt_level; + unsigned lbd; + unsigned cref; + + vec_uint_clear(s->temp_lits); + solver_analyze(s, confl_cref, s->temp_lits, &bt_level, &lbd); + s->sum_lbd += lbd; + b_queue_push(s->bq_lbd, lbd); + solver_cancel_until(s, bt_level); + cref = UNDEF; + if (vec_uint_size(s->temp_lits) > 1) { + cref = solver_clause_create(s, s->temp_lits, 1); + clause_watch(s, cref); + } + solver_enqueue(s, vec_uint_at(s->temp_lits, 0), cref); + var_act_decay(s); + clause_act_decay(s); +} + +static inline void solver_analyze_final(solver_t *s, unsigned lit) +{ + unsigned i; + + vec_uint_push_back(s->final_conflict, lit); + if (solver_dlevel(s) == 0) + return; + vec_char_assign(s->seen, lit2var(lit), 1); + for (i = vec_uint_size(s->trail) - 1; i <= vec_uint_at(s->trail_lim, 0); i--) { + unsigned var = lit2var(vec_uint_at(s->trail, i)); + + if (vec_char_at(s->seen, var)) { + unsigned reason = var_reason(s, var); + if (reason == UNDEF) { + assert(var_dlevel(s, var) > 0); + vec_uint_push_back(s->final_conflict, lit_neg(vec_uint_at(s->trail, i))); + } else { + unsigned j; + struct clause *clause = clause_read(s, reason); + for (j = (clause->size == 2 ? 0 : 1); j < clause->size; j++) { + if (lit_dlevel(s, clause->data[j].lit) > 0) + vec_char_assign(s->seen, lit2var(clause->data[j].lit), 1); + } + } + vec_char_assign(s->seen, var, 0); + } + } + vec_char_assign(s->seen, lit2var(lit), 0); +} + +static inline void solver_garbage_collect(solver_t *s) +{ + unsigned i; + unsigned *array; + struct cdb *new_cdb = cdb_alloc(cdb_capacity(s->all_clauses) - cdb_wasted(s->all_clauses)); + + for (i = 0; i < 2 * vec_char_size(s->assigns); i++) { + struct watcher *w; + watch_list_foreach(s->watches, w, i) + clause_realloc(new_cdb, s->all_clauses, &(w->cref)); + watch_list_foreach(s->bin_watches, w, i) + clause_realloc(new_cdb, s->all_clauses, &(w->cref)); + } + + for (i = 0; i < vec_uint_size(s->trail); i++) + if (lit_reason(s, vec_uint_at(s->trail, i)) != UNDEF) + clause_realloc(new_cdb, s->all_clauses, &(vec_uint_data(s->reasons)[lit2var(vec_uint_at(s->trail, i))])); + + array = vec_uint_data(s->learnts); + for (i = 0; i < vec_uint_size(s->learnts); i++) + clause_realloc(new_cdb, s->all_clauses, &(array[i])); + + array = vec_uint_data(s->originals); + for (i = 0; i < vec_uint_size(s->originals); i++) + clause_realloc(new_cdb, s->all_clauses, &(array[i])); + + cdb_free(s->all_clauses); + s->all_clauses = new_cdb; +} + +static inline void solver_reduce_cdb(solver_t *s) +{ + unsigned i, limit; + unsigned n_learnts = vec_uint_size(s->learnts); + unsigned cref; + struct clause *clause; + struct clause **learnts_cls; + + learnts_cls = satoko_alloc(struct clause *, n_learnts); + vec_uint_foreach(s->learnts, cref, i) + learnts_cls[i] = clause_read(s, cref); + + limit = n_learnts / 2; + + satoko_sort((void *)learnts_cls, n_learnts, + (int (*)(const void *, const void *)) clause_compare); + + if (learnts_cls[n_learnts / 2]->lbd <= 3) + s->RC2 += s->opts.inc_special_reduce; + if (learnts_cls[n_learnts - 1]->lbd <= 6) + s->RC2 += s->opts.inc_special_reduce; + + vec_uint_clear(s->learnts); + for (i = 0; i < n_learnts; i++) { + clause = learnts_cls[i]; + cref = cdb_cref(s->all_clauses, (unsigned *)clause); + assert(clause->f_mark == 0); + if (clause->f_deletable && clause->lbd > 2 && clause->size > 2 && lit_reason(s, clause->data[0].lit) != cref && (i < limit)) { + clause->f_mark = 1; + s->stats.n_learnt_lits -= clause->size; + clause_unwatch(s, cref); + cdb_remove(s->all_clauses, clause); + } else { + if (!clause->f_deletable) + limit++; + clause->f_deletable = 1; + vec_uint_push_back(s->learnts, cref); + } + } + satoko_free(learnts_cls); + + if (s->opts.verbose) { + printf("reduceDB: Keeping %7d out of %7d clauses (%5.2f %%) \n", + vec_uint_size(s->learnts), n_learnts, + 100.0 * vec_uint_size(s->learnts) / n_learnts); + fflush(stdout); + } + if (cdb_wasted(s->all_clauses) > cdb_size(s->all_clauses) * s->opts.garbage_max_ratio) + solver_garbage_collect(s); +} + +//===------------------------------------------------------------------------=== +// Solver external functions +//===------------------------------------------------------------------------=== +unsigned solver_clause_create(solver_t *s, vec_uint_t *lits, unsigned f_learnt) +{ + struct clause *clause; + unsigned cref; + unsigned n_words; + + assert(vec_uint_size(lits) > 1); + assert(f_learnt == 0 || f_learnt == 1); + + n_words = 3 + f_learnt + vec_uint_size(lits); + cref = cdb_append(s->all_clauses, n_words); + clause = clause_read(s, cref); + clause->f_learnt = f_learnt; + clause->f_mark = 0; + clause->f_reallocd = 0; + clause->f_deletable = f_learnt; + clause->size = vec_uint_size(lits); + memcpy(&(clause->data[0].lit), vec_uint_data(lits), sizeof(unsigned) * vec_uint_size(lits)); + + if (f_learnt) { + vec_uint_push_back(s->learnts, cref); + clause->lbd = clause_clac_lbd(s, vec_uint_data(lits), vec_uint_size(lits)); + clause->data[clause->size].act = 0; + s->stats.n_learnt_lits += vec_uint_size(lits); + clause_act_bump(s, clause); + } else { + vec_uint_push_back(s->originals, cref); + s->stats.n_original_lits += vec_uint_size(lits); + } + return cref; +} + +void solver_cancel_until(solver_t * s, unsigned level) +{ + int 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)); + + vec_char_assign(s->assigns, var, VAR_UNASSING); + vec_uint_assign(s->reasons, var, UNDEF); + vec_char_assign(s->polarity, var, lit_polarity(vec_uint_at(s->trail, (unsigned) i))); + if (!heap_in_heap(s->var_order, var)) + heap_insert(s->var_order, var); + } + s->i_qhead = vec_uint_at(s->trail_lim, level); + vec_uint_shrink(s->trail, vec_uint_at(s->trail_lim, level)); + vec_uint_shrink(s->trail_lim, level); +} + +unsigned solver_propagate(solver_t *s) +{ + unsigned conf_cref = UNDEF; + unsigned *lits; + unsigned neg_lit; + unsigned n_propagations = 0; + + while (s->i_qhead < vec_uint_size(s->trail)) { + unsigned p = vec_uint_at(s->trail, s->i_qhead++); + struct watch_list *ws; + struct watcher *begin; + struct watcher *end; + struct watcher *i, *j; + + n_propagations++; + watch_list_foreach(s->bin_watches, i, p) { + if (var_value(s, lit2var(i->blocker)) == VAR_UNASSING) + solver_enqueue(s, i->blocker, i->cref); + else if (lit_value(s, i->blocker) == LIT_FALSE) + return i->cref; + } + + ws = vec_wl_at(s->watches, p); + begin = watch_list_array(ws); + end = begin + watch_list_size(ws); + for (i = j = begin; i < end;) { + struct clause *clause; + struct watcher w; + + if (lit_value(s, i->blocker) == LIT_TRUE) { + *j++ = *i++; + continue; + } + + clause = clause_read(s, i->cref); + lits = &(clause->data[0].lit); + + // Make sure the false literal is data[1]: + neg_lit = lit_neg(p); + if (lits[0] == neg_lit) + mkt_swap(unsigned, lits[0], lits[1]); + assert(lits[1] == neg_lit); + + w.cref = i->cref; + w.blocker = lits[0]; + + /* If 0th watch is true, then clause is already satisfied. */ + if (lits[0] != i->blocker && lit_value(s, lits[0]) == LIT_TRUE) + *j++ = w; + else { + /* Look for new watch */ + unsigned k; + for (k = 2; k < clause->size; k++) { + if (lit_value(s, lits[k]) != LIT_FALSE) { + lits[1] = lits[k]; + lits[k] = neg_lit; + watch_list_push(vec_wl_at(s->watches, lit_neg(lits[1])), w); + goto next; + } + } + + *j++ = w; + + /* Clause becomes unit under this assignment */ + if (lit_value(s, lits[0]) == LIT_FALSE) { + conf_cref = i->cref; + s->i_qhead = vec_uint_size(s->trail); + i++; + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } else + solver_enqueue(s, lits[0], i->cref); + } + next: + i++; + } + + s->stats.n_inspects += j - watch_list_array(ws); + watch_list_shrink(ws, j - watch_list_array(ws)); + } + s->stats.n_propagations += n_propagations; + s->n_props_simplify -= n_propagations; + return conf_cref; +} + +char solver_search(solver_t *s) +{ + s->stats.n_starts++; + while (1) { + unsigned confl_cref = solver_propagate(s); + if (confl_cref != UNDEF) { + s->stats.n_conflicts++; + if (solver_dlevel(s) == 0) + return SATOKO_UNSAT; + /* Restart heuristic */ + b_queue_push(s->bq_trail, vec_uint_size(s->trail)); + if (solver_block_rst(s)) + b_queue_clean(s->bq_lbd); + solver_handle_conflict(s, confl_cref); + } else { + /* No conflict */ + unsigned next_lit; + + if (solver_rst(s)) { + b_queue_clean(s->bq_lbd); + solver_cancel_until(s, 0); + return SATOKO_UNDEC; + } + if (solver_dlevel(s) == 0) + satoko_simplify(s); + + /* Reduce the set of learnt clauses */ + if (s->stats.n_conflicts >= s->n_confl_bfr_reduce) { + s->RC1 = (s->stats.n_conflicts / s->RC2) + 1; + solver_reduce_cdb(s); + s->RC2 += s->opts.inc_reduce; + s->n_confl_bfr_reduce = s->RC1 * s->RC2; + } + + /* Make decisions based on user assumptions */ + next_lit = UNDEF; + while (solver_dlevel(s) < vec_uint_size(s->assumptions)) { + unsigned lit = vec_uint_at(s->assumptions, solver_dlevel(s)); + if (lit_value(s, lit) == LIT_TRUE) { + vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail)); + } else if (lit_value(s, lit) == LIT_FALSE) { + solver_analyze_final(s, lit_neg(lit)); + return SATOKO_UNSAT; + } else { + next_lit = lit; + break; + } + + } + if (next_lit == UNDEF) { + s->stats.n_decisions++; + next_lit = solver_decide(s); + if (next_lit == UNDEF) + return SATOKO_SAT; + } + solver_new_decision(s, next_lit); + } + } +} + +//===------------------------------------------------------------------------=== +// Debug procedure +//===------------------------------------------------------------------------=== +void solver_debug_check(solver_t *s, int result) +{ + unsigned cref, 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++) + if (array[i - 1] == lit_neg(array[i])) { + printf("Inconsistent trail: %u %u\n", array[i - 1], array[i]); + return; + } + printf(" TRAIL OK\n"); + + printf("Checking clauses... \n"); + vec_uint_foreach(s->originals, cref, i) { + unsigned j; + struct clause *clause = clause_read(s, cref); + for (j = 0; j < clause->size; j++) { + if (vec_uint_find(s->trail, clause->data[j].lit)) { + break; + } + } + if (result == SATOKO_SAT && j == clause->size) { + printf("FOUND UNSAT CLAUSE!!!!\n"); + clause_print(clause); + } + } +} + +ABC_NAMESPACE_IMPL_END |