luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/sat/satoko/solver.c

719 lines
24 KiB
C
Raw Blame History

//===--- 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);
stk_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_bin(s->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) {
stk_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;
}
next_var = heap_remove_min(s->var_order);
if (solver_has_marks(s) && !var_mark(s, next_var))
next_var = UNDEF;
}
return var2lit(next_var, var_polarity(s, next_var));
}
static inline void solver_new_decision(solver_t *s, unsigned lit)
{
if (solver_has_marks(s) && !var_mark(s, lit2var(lit)))
return;
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);
stk_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)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 > (int)s->opts.fst_block_rst &&
b_queue_is_valid(s->bq_lbd) &&
((long)vec_uint_size(s->trail) > (s->opts.b_rst * (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)
{
int i;
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--) {
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));
if (s->book_cdb)
s->book_cdb = 0;
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));
}
/* Update CREFS */
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_start(s->learnts, cref, i, s->book_cl_lrnt)
learnts_cls[i] = clause_read(s, cref);
limit = (unsigned)(n_learnts * s->opts.learnt_ratio);
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->polarity, var, vec_char_at(s->assigns, var));
vec_char_assign(s->assigns, var, VAR_UNASSING);
vec_uint_assign(s->reasons, var, UNDEF);
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_bin(s->watches, i, p) {
if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker)))
continue;
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 + ws->n_bin; i < end;) {
struct clause *clause;
struct watcher w;
if (solver_has_marks(s) && !var_mark(s, lit2var(i->blocker))) {
*j++ = *i++;
continue;
}
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)
stk_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, 0);
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 (!s->opts.no_simplify && solver_dlevel(s) == 0)
satoko_simplify(s);
/* Reduce the set of learnt clauses */
if (s->opts.learnt_ratio &&
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
Reference in New Issue View Git Blame Copy Permalink