mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Cuber fixes. Added March_CU heuristics

Browse source
This commit is contained in:
Miguel Neves 2017-10-06 16:10:05 -07:00
parent 133f376172
commit 4d91169118
6 changed files with 130 additions and 59 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -120,7 +120,7 @@ def _get_args(args):
try: try:
if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
return args[0] return args[0]
elif len(args) == 1 and isinstance(args[0], set): elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
return [arg for arg in args[0]] return [arg for arg in args[0]]
else: else:
return args return args

3
src/sat/sat_config.cpp
View file

@ -100,6 +100,9 @@ namespace sat {
else if (p.lookahead_reward() == symbol("unit")) { else if (p.lookahead_reward() == symbol("unit")) {
m_lookahead_reward = unit_literal_reward; m_lookahead_reward = unit_literal_reward;
} }
else if (p.lookahead_reward() == symbol("march_cu")) {
m_lookahead_reward = march_cu_reward;
}
else { else {
throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'"); throw sat_param_exception("invalid reward type supplied: accepted heuristics are 'ternary', 'heuleu', 'unit' or 'heule_schur'");
} }

3
src/sat/sat_config.h
View file

@ -61,7 +61,8 @@ namespace sat {
ternary_reward, ternary_reward,
unit_literal_reward, unit_literal_reward,
heule_schur_reward, heule_schur_reward,
heule_unit_reward heule_unit_reward,
march_cu_reward
}; };
struct config { struct config {

160
src/sat/sat_lookahead.cpp
View file

@ -217,7 +217,7 @@ namespace sat {
bool lookahead::select(unsigned level) { bool lookahead::select(unsigned level) {
init_pre_selection(level); init_pre_selection(level);
unsigned level_cand = std::max(m_config.m_level_cand, m_freevars.size() / 50); unsigned level_cand = std::max(m_config.m_level_cand, m_freevars.size() / 50);
unsigned max_num_cand = level == 0 ? m_freevars.size() : level_cand / level; unsigned max_num_cand = (level > 0 && m_config.m_preselect) ? level_cand / level : m_freevars.size();
max_num_cand = std::max(m_config.m_min_cutoff, max_num_cand); max_num_cand = std::max(m_config.m_min_cutoff, max_num_cand);
double sum = 0; double sum = 0;
@ -251,30 +251,40 @@ namespace sat {
} }
TRACE("sat", display_candidates(tout);); TRACE("sat", display_candidates(tout););
SASSERT(!m_candidates.empty()); SASSERT(!m_candidates.empty());
if (m_candidates.size() > max_num_cand) { heap_sort();
unsigned j = m_candidates.size()/2; while (m_candidates.size() > max_num_cand) {
while (j > 0) { m_candidates.pop_back();
--j;
sift_up(j);
}
while (true) {
m_candidates[0] = m_candidates.back();
m_candidates.pop_back();
if (m_candidates.size() == max_num_cand) break;
sift_up(0);
}
} }
SASSERT(!m_candidates.empty() && m_candidates.size() <= max_num_cand); SASSERT(!m_candidates.empty() && m_candidates.size() <= max_num_cand);
TRACE("sat", display_candidates(tout);); TRACE("sat", display_candidates(tout););
return true; return true;
} }
void lookahead::sift_up(unsigned j) { void lookahead::heap_sort() {
if (m_candidates.size() > 1) {
heapify();
for (unsigned i = m_candidates.size() - 1; i > 0; --i) {
candidate c = m_candidates[i];
m_candidates[i] = m_candidates[0];
m_candidates[0] = c;
sift_down(0, i);
}
}
}
void lookahead::heapify() {
unsigned i = 1 + (m_candidates.size() - 2) / 2;
while(i > 0) {
sift_down(--i, m_candidates.size());
}
}
void lookahead::sift_down(unsigned j, unsigned sz) {
unsigned i = j; unsigned i = j;
candidate c = m_candidates[j]; candidate c = m_candidates[j];
for (unsigned k = 2*j + 1; k < m_candidates.size(); i = k, k = 2*k + 1) { for (unsigned k = 2 * j + 1; k < sz; i = k, k = 2 * k + 1) {
// pick largest parent // pick smallest child
if (k + 1 < m_candidates.size() && m_candidates[k].m_rating < m_candidates[k+1].m_rating) { if (k + 1 < sz && m_candidates[k].m_rating > m_candidates[k + 1].m_rating) {
++k; ++k;
} }
if (c.m_rating <= m_candidates[k].m_rating) break; if (c.m_rating <= m_candidates[k].m_rating) break;
@ -432,6 +442,9 @@ namespace sat {
case heule_unit_reward: case heule_unit_reward:
heule_unit_scores(); heule_unit_scores();
break; break;
case march_cu_reward:
march_cu_scores();
break;
case unit_literal_reward: case unit_literal_reward:
heule_schur_scores(); heule_schur_scores();
break; break;
@ -478,7 +491,7 @@ namespace sat {
for (bool_var x : m_freevars) { for (bool_var x : m_freevars) {
literal l(x, false); literal l(x, false);
m_rating[l.var()] = heule_unit_score(l) * heule_unit_score(~l); m_rating[l.var()] = heule_unit_score(l) * heule_unit_score(~l);
} }
} }
double lookahead::heule_unit_score(literal l) { double lookahead::heule_unit_score(literal l) {
@ -493,7 +506,23 @@ namespace sat {
sum += pow(0.5, m_nary_literals[cls_idx]); sum += pow(0.5, m_nary_literals[cls_idx]);
} }
return sum; return sum;
} }
void lookahead::march_cu_scores() {
for (bool_var x : m_freevars) {
literal l(x, false);
double pos = march_cu_score(l), neg = march_cu_score(~l);
m_rating[l.var()] = 1024 * pos * neg + pos + neg + 1;
}
}
double lookahead::march_cu_score(literal l) {
double sum = 1.0 + literal_big_occs(~l);
for (literal lit : m_binary[l.index()]) {
if (is_undef(lit)) sum += literal_big_occs(lit);
}
return sum;
}
void lookahead::ensure_H(unsigned level) { void lookahead::ensure_H(unsigned level) {
while (m_H.size() <= level) { while (m_H.size() <= level) {
@ -884,7 +913,7 @@ namespace sat {
} }
void lookahead::init() { void lookahead::init() {
m_delta_trigger = m_num_vars/10; m_delta_trigger = 0.0;
m_config.m_dl_success = 0.8; m_config.m_dl_success = 0.8;
m_inconsistent = false; m_inconsistent = false;
m_qhead = 0; m_qhead = 0;
@ -1068,6 +1097,7 @@ namespace sat {
m_lookahead_reward += num_units; m_lookahead_reward += num_units;
break; break;
case heule_unit_reward: case heule_unit_reward:
case march_cu_reward:
case heule_schur_reward: case heule_schur_reward:
break; break;
default: default:
@ -1391,6 +1421,9 @@ namespace sat {
case heule_unit_reward: case heule_unit_reward:
m_lookahead_reward += pow(0.5, nonfixed); m_lookahead_reward += pow(0.5, nonfixed);
break; break;
case march_cu_reward:
m_lookahead_reward += 3.3 * pow(0.5, nonfixed - 2);
break;
case ternary_reward: case ternary_reward:
if (nonfixed == 2) { if (nonfixed == 2) {
m_lookahead_reward += (*m_heur)[l1.index()] * (*m_heur)[l2.index()]; m_lookahead_reward += (*m_heur)[l1.index()] * (*m_heur)[l2.index()];
@ -1486,6 +1519,9 @@ namespace sat {
case heule_unit_reward: case heule_unit_reward:
m_lookahead_reward += 0.25; m_lookahead_reward += 0.25;
break; break;
case march_cu_reward:
m_lookahead_reward += 3.3;
break;
case unit_literal_reward: case unit_literal_reward:
break; break;
} }
@ -1516,6 +1552,9 @@ namespace sat {
case heule_unit_reward: case heule_unit_reward:
m_lookahead_reward += pow(0.5, sz); m_lookahead_reward += pow(0.5, sz);
break; break;
case march_cu_reward:
m_lookahead_reward += 3.3 * pow(0.5, sz - 2);
break;
case ternary_reward: case ternary_reward:
m_lookahead_reward = (double)0.001; m_lookahead_reward = (double)0.001;
break; break;
@ -1525,10 +1564,18 @@ namespace sat {
} }
// Sum_{ clause C that contains ~l } 1 // Sum_{ clause C that contains ~l } 1
// FIXME: counts occurences of ~l; misleading
double lookahead::literal_occs(literal l) { double lookahead::literal_occs(literal l) {
double result = m_binary[l.index()].size(); double result = m_binary[l.index()].size();
unsigned_vector const& nclauses = m_nary[(~l).index()]; //unsigned_vector const& nclauses = m_nary[(~l).index()];
result += m_nary_count[(~l).index()]; result += literal_big_occs(l);
return result;
}
// Sum_{ clause C that contains ~l such that |C| > 2} 1
// FIXME: counts occurences of ~l; misleading
double lookahead::literal_big_occs(literal l) {
double result = m_nary_count[(~l).index()];
result += m_ternary_count[(~l).index()]; result += m_ternary_count[(~l).index()];
return result; return result;
} }
@ -1542,22 +1589,19 @@ namespace sat {
} }
} }
void lookahead::propagate() { void lookahead::propagate() {
while (!inconsistent() && m_qhead < m_trail.size()) { while (!inconsistent() && m_qhead < m_trail.size()) {
unsigned i = m_qhead; unsigned i = m_qhead;
unsigned sz = m_trail.size(); for (; i < m_trail.size() && !inconsistent(); ++i) {
for (; i < sz && !inconsistent(); ++i) {
literal l = m_trail[i]; literal l = m_trail[i];
TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";); TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
propagate_binary(l); propagate_binary(l);
} }
while (m_qhead < sz && !inconsistent()) { while (m_qhead < m_trail.size() && !inconsistent()) {
propagate_clauses(m_trail[m_qhead++]); propagate_clauses(m_trail[m_qhead++]);
} }
SASSERT(m_qhead == sz || (inconsistent() && m_qhead < sz)); SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
} }
TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
} }
@ -1566,12 +1610,15 @@ namespace sat {
TRACE("sat", display_lookahead(tout); ); TRACE("sat", display_lookahead(tout); );
unsigned base = 2; unsigned base = 2;
bool change = true; bool change = true;
bool first = true; literal last_changed = null_literal;
while (change && !inconsistent()) { while (change && !inconsistent()) {
change = false; change = false;
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
checkpoint(); checkpoint();
literal lit = m_lookahead[i].m_lit; literal lit = m_lookahead[i].m_lit;
if (lit == last_changed) {
break;
}
if (is_fixed_at(lit, c_fixed_truth)) continue; if (is_fixed_at(lit, c_fixed_truth)) continue;
unsigned level = base + m_lookahead[i].m_offset; unsigned level = base + m_lookahead[i].m_offset;
if (m_stamp[lit.var()] >= level) { if (m_stamp[lit.var()] >= level) {
@ -1584,7 +1631,7 @@ namespace sat {
unsigned old_trail_sz = m_trail.size(); unsigned old_trail_sz = m_trail.size();
reset_lookahead_reward(lit); reset_lookahead_reward(lit);
push_lookahead1(lit, level); push_lookahead1(lit, level);
if (!first) do_double(lit, base); do_double(lit, base);
bool unsat = inconsistent(); bool unsat = inconsistent();
unsigned num_units = m_trail.size() - old_trail_sz; unsigned num_units = m_trail.size() - old_trail_sz;
pop_lookahead1(lit, num_units); pop_lookahead1(lit, num_units);
@ -1595,6 +1642,7 @@ namespace sat {
propagate(); propagate();
init_lookahead_reward(); init_lookahead_reward();
change = true; change = true;
last_changed = lit;
} }
else { else {
update_lookahead_reward(lit, level); update_lookahead_reward(lit, level);
@ -1604,13 +1652,9 @@ namespace sat {
if (c_fixed_truth - 2 * m_lookahead.size() < base) { if (c_fixed_truth - 2 * m_lookahead.size() < base) {
break; break;
} }
if (first && !change) {
first = false;
change = true;
}
reset_lookahead_reward(); reset_lookahead_reward();
init_lookahead_reward(); init_lookahead_reward();
// base += 2 * m_lookahead.size(); base += 2 * m_lookahead.size();
} }
reset_lookahead_reward(); reset_lookahead_reward();
TRACE("sat", display_lookahead(tout); ); TRACE("sat", display_lookahead(tout); );
@ -1664,6 +1708,7 @@ namespace sat {
case ternary_reward: return l + r + (1 << 10) * l * r; case ternary_reward: return l + r + (1 << 10) * l * r;
case heule_schur_reward: return l * r; case heule_schur_reward: return l * r;
case heule_unit_reward: return l * r; case heule_unit_reward: return l * r;
case march_cu_reward: return 1024 * (1024 * l * r + l + r);
case unit_literal_reward: return l * r; case unit_literal_reward: return l * r;
default: UNREACHABLE(); return l * r; default: UNREACHABLE(); return l * r;
} }
@ -1753,14 +1798,16 @@ namespace sat {
} }
} }
void lookahead::do_double(literal l, unsigned& base) { void lookahead::do_double(literal l, unsigned& base) {
if (!inconsistent() && scope_lvl() > 1 && dl_enabled(l)) { if (!inconsistent() && dl_enabled(l)) {
if (get_lookahead_reward(l) > m_delta_trigger) { if (get_lookahead_reward(l) > m_delta_trigger) {
if (dl_no_overflow(base)) { if (dl_no_overflow(base)) {
++m_stats.m_double_lookahead_rounds; ++m_stats.m_double_lookahead_rounds;
double_look(l, base); double_look(l, base);
m_delta_trigger = get_lookahead_reward(l); if (!inconsistent()) {
dl_disable(l); m_delta_trigger = get_lookahead_reward(l);
dl_disable(l);
}
} }
} }
else { else {
@ -1772,21 +1819,30 @@ namespace sat {
void lookahead::double_look(literal l, unsigned& base) { void lookahead::double_look(literal l, unsigned& base) {
SASSERT(!inconsistent()); SASSERT(!inconsistent());
SASSERT(dl_no_overflow(base)); SASSERT(dl_no_overflow(base));
unsigned dl_truth = base + 2 * m_lookahead.size() * (m_config.m_dl_max_iterations + 1); base += m_lookahead.size();
unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations;
scoped_level _sl(*this, dl_truth); scoped_level _sl(*this, dl_truth);
IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";); IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";);
init_lookahead_reward(); init_lookahead_reward();
assign(l); assign(l);
propagate(); propagate();
bool change = true; bool change = true;
literal last_changed = null_literal;
unsigned num_iterations = 0; unsigned num_iterations = 0;
while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) { while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) {
change = false; change = false;
num_iterations++; num_iterations++;
base += 2*m_lookahead.size();
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
literal lit = m_lookahead[i].m_lit; literal lit = m_lookahead[i].m_lit;
if (is_fixed_at(lit, dl_truth)) continue; if (lit == last_changed) {
SASSERT(change == false);
break;
}
if (is_fixed_at(lit, dl_truth)) continue;
if (base + m_lookahead.size() + m_lookahead[i].m_offset >= dl_truth) {
change = false;
break;
}
if (push_lookahead2(lit, base + m_lookahead[i].m_offset)) { if (push_lookahead2(lit, base + m_lookahead[i].m_offset)) {
TRACE("sat", tout << "unit: " << ~lit << "\n";); TRACE("sat", tout << "unit: " << ~lit << "\n";);
++m_stats.m_double_lookahead_propagations; ++m_stats.m_double_lookahead_propagations;
@ -1795,10 +1851,12 @@ namespace sat {
assign(~lit); assign(~lit);
propagate(); propagate();
change = true; change = true;
last_changed = lit;
init_lookahead_reward(); init_lookahead_reward();
} }
} }
SASSERT(dl_truth - 2 * m_lookahead.size() > base); base += 2 * m_lookahead.size();
SASSERT(dl_truth >= base);
} }
reset_lookahead_reward(); reset_lookahead_reward();
SASSERT(m_level == dl_truth); SASSERT(m_level == dl_truth);
@ -1838,14 +1896,13 @@ namespace sat {
void lookahead::propagated(literal l) { void lookahead::propagated(literal l) {
assign(l); assign(l);
switch (m_search_mode) { for (unsigned i = m_trail.size() - 1; i < m_trail.size() && !inconsistent(); ++i) {
case lookahead_mode::searching: literal l = m_trail[i];
break; TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
case lookahead_mode::lookahead1: propagate_binary(l);
}
if (m_search_mode == lookahead_mode::lookahead1) {
m_wstack.push_back(l); m_wstack.push_back(l);
break;
case lookahead_mode::lookahead2:
break;
} }
} }
@ -1953,10 +2010,11 @@ namespace sat {
backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
return l_undef; return l_undef;
} }
int prev_nfreevars = m_freevars.size();
literal lit = choose(); literal lit = choose();
if (inconsistent()) { if (inconsistent()) {
TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";); TRACE("sat", tout << "inconsistent: " << m_cube_state.m_cube << "\n";);
m_cube_state.m_freevars_threshold = m_freevars.size(); m_cube_state.m_freevars_threshold = prev_nfreevars;
if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false; if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return l_false;
continue; continue;
} }

17
src/sat/sat_lookahead.h
View file

@ -73,6 +73,7 @@ namespace sat {
double m_max_score; double m_max_score;
unsigned m_max_hlevel; unsigned m_max_hlevel;
unsigned m_min_cutoff; unsigned m_min_cutoff;
bool m_preselect;
unsigned m_level_cand; unsigned m_level_cand;
double m_delta_rho; double m_delta_rho;
unsigned m_dl_max_iterations; unsigned m_dl_max_iterations;
@ -86,9 +87,10 @@ namespace sat {
m_alpha = 3.5; m_alpha = 3.5;
m_max_score = 20.0; m_max_score = 20.0;
m_min_cutoff = 30; m_min_cutoff = 30;
m_preselect = false;
m_level_cand = 600; m_level_cand = 600;
m_delta_rho = (double)0.9995; m_delta_rho = (double)0.99995;
m_dl_max_iterations = 32; m_dl_max_iterations = 2;
m_tc1_limit = 10000000; m_tc1_limit = 10000000;
m_reward_type = ternary_reward; m_reward_type = ternary_reward;
m_cube_cutoff = 0; m_cube_cutoff = 0;
@ -289,7 +291,10 @@ namespace sat {
double get_rating(bool_var v) const { return m_rating[v]; } double get_rating(bool_var v) const { return m_rating[v]; }
double get_rating(literal l) const { return get_rating(l.var()); } double get_rating(literal l) const { return get_rating(l.var()); }
bool select(unsigned level); bool select(unsigned level);
void sift_up(unsigned j); //void sift_up(unsigned j);
void heap_sort();
void heapify();
void sift_down(unsigned j, unsigned sz);
double init_candidates(unsigned level, bool newbies); double init_candidates(unsigned level, bool newbies);
std::ostream& display_candidates(std::ostream& out) const; std::ostream& display_candidates(std::ostream& out) const;
bool is_unsat() const; bool is_unsat() const;
@ -301,6 +306,8 @@ namespace sat {
double heule_schur_score(literal l); double heule_schur_score(literal l);
void heule_unit_scores(); void heule_unit_scores();
double heule_unit_score(literal l); double heule_unit_score(literal l);
void march_cu_scores();
double march_cu_score(literal l);
double l_score(literal l, svector<double> const& h, double factor, double sqfactor, double afactor); double l_score(literal l, svector<double> const& h, double factor, double sqfactor, double afactor);
// ------------------------------------ // ------------------------------------
@ -460,6 +467,7 @@ namespace sat {
void do_double(literal l, unsigned& base); void do_double(literal l, unsigned& base);
void double_look(literal l, unsigned& base); void double_look(literal l, unsigned& base);
void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; } void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; }
//void set_conflict() { TRACE("sat", tout << "conflict\n";); printf("CONFLICT\n"); m_inconsistent = true; }
bool inconsistent() { return m_inconsistent; } bool inconsistent() { return m_inconsistent; }
unsigned scope_lvl() const { return m_trail_lim.size(); } unsigned scope_lvl() const { return m_trail_lim.size(); }
@ -544,7 +552,8 @@ namespace sat {
void collect_statistics(statistics& st) const; void collect_statistics(statistics& st) const;
double literal_occs(literal l); double literal_occs(literal l);
double literal_big_occs(literal l);
}; };
} }

4
src/sat/sat_params.pyg
View file

@ -31,7 +31,7 @@ def_module_params('sat',
('drat.check', BOOL, False, 'build up internal proof and check'), ('drat.check', BOOL, False, 'build up internal proof and check'),
('cardinality.solver', BOOL, False, 'use cardinality solver'), ('cardinality.solver', BOOL, False, 'use cardinality solver'),
('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'), ('pb.solver', SYMBOL, 'circuit', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use SMT solver)'),
('xor.solver', BOOL, False, 'use xor solver'), ('xor.solver', BOOL, False, 'use xor solver'),
('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'), ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search', BOOL, False, 'use local search instead of CDCL'),
@ -40,7 +40,7 @@ def_module_params('sat',
('lookahead.cube.cutoff', UINT, 0, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'), ('lookahead.cube.cutoff', UINT, 0, 'cut-off depth to create cubes. Only enabled when non-zero. Used when lookahead_cube is true.'),
('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead_search', BOOL, False, 'use lookahead solver'),
('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'),
('lookahead.reward', SYMBOL, 'heuleu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), or unit'), ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'),
('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'), ('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving'),
('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes'))) ('dimacs.inprocess.display', BOOL, False, 'display SAT instance in DIMACS format if unsolved after inprocess.max inprocessing passes')))