diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index 5f45f6c1c..a180d4ca9 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -828,7 +828,10 @@ class env { } else if (!strcmp(ch,"$to_real")) { check_arity(terms.size(), 1); - r = to_real(terms[0]); + r = terms[0]; + if (r.get_sort().is_int()) { + r = to_real(terms[0]); + } } else if (!strcmp(ch,"$is_int")) { check_arity(terms.size(), 1); diff --git a/src/opt/bcd2.cpp b/src/opt/bcd2.cpp deleted file mode 100644 index a373b652b..000000000 --- a/src/opt/bcd2.cpp +++ /dev/null @@ -1,405 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - bcd2.cpp - -Abstract: - - bcd2 based MaxSAT. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-4-17 - -Notes: - ---*/ -#include "bcd2.h" -#include "pb_decl_plugin.h" -#include "uint_set.h" -#include "ast_pp.h" - - -namespace opt { - // ------------------------------------------------------ - // Morgado, Heras, Marques-Silva 2013 - // (initial version without model-based optimizations) - // - class bcd2 : public maxsmt_solver_base { - struct wcore { - expr* m_r; - unsigned_vector m_R; - rational m_lower; - rational m_mid; - rational m_upper; - }; - typedef obj_hashtable expr_set; - - pb_util pb; - expr_ref_vector m_soft_aux; - obj_map m_relax2index; // expr |-> index - obj_map m_soft2index; // expr |-> index - expr_ref_vector m_trail; - expr_ref_vector m_soft_constraints; - expr_set m_asm_set; - vector m_cores; - vector m_sigmas; - rational m_den; // least common multiplier of original denominators - bool m_enable_lazy; // enable adding soft constraints lazily (called 'mgbcd2') - unsigned_vector m_lazy_soft; // soft constraints to add lazily. - - void set2asms(expr_set const& set, expr_ref_vector & es) const { - es.reset(); - expr_set::iterator it = set.begin(), end = set.end(); - for (; it != end; ++it) { - es.push_back(m.mk_not(*it)); - } - } - void bcd2_init_soft(weights_t& weights, expr_ref_vector const& soft) { - - // normalize weights to be integral: - m_den = rational::one(); - for (unsigned i = 0; i < m_weights.size(); ++i) { - m_den = lcm(m_den, denominator(m_weights[i])); - } - if (!m_den.is_one()) { - for (unsigned i = 0; i < m_weights.size(); ++i) { - m_weights[i] = m_den*m_weights[i]; - SASSERT(m_weights[i].is_int()); - } - } - } - void init_bcd() { - m_trail.reset(); - m_asm_set.reset(); - m_cores.reset(); - m_sigmas.reset(); - m_lazy_soft.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_sigmas.push_back(m_weights[i]); - m_soft_aux.push_back(mk_fresh()); - if (m_enable_lazy) { - m_lazy_soft.push_back(i); - } - else { - enable_soft_constraint(i); - } - } - m_upper += rational(1); - } - - void process_sat() { - svector assignment; - update_assignment(assignment); - if (check_lazy_soft(assignment)) { - update_sigmas(); - } - } - - public: - bcd2(maxsat_context& c, - weights_t& ws, expr_ref_vector const& soft): - maxsmt_solver_base(c, ws, soft), - pb(m), - m_soft_aux(m), - m_trail(m), - m_soft_constraints(m), - m_enable_lazy(true) { - bcd2_init_soft(ws, soft); - } - - virtual ~bcd2() {} - - virtual lbool operator()() { - expr_ref fml(m), r(m); - lbool is_sat = l_undef; - expr_ref_vector asms(m); - init(); - init_bcd(); - if (m.canceled()) { - normalize_bounds(); - return l_undef; - } - process_sat(); - while (m_lower < m_upper) { - trace_bounds("bcd2"); - assert_soft(); - solver::scoped_push _scope2(s()); - TRACE("opt", display(tout);); - assert_cores(); - set2asms(m_asm_set, asms); - if (m.canceled()) { - normalize_bounds(); - return l_undef; - } - is_sat = s().check_sat(asms.size(), asms.c_ptr()); - switch(is_sat) { - case l_undef: - normalize_bounds(); - return l_undef; - case l_true: - process_sat(); - break; - case l_false: { - ptr_vector unsat_core; - uint_set subC, soft; - s().get_unsat_core(unsat_core); - core2indices(unsat_core, subC, soft); - SASSERT(unsat_core.size() == subC.num_elems() + soft.num_elems()); - if (soft.num_elems() == 0 && subC.num_elems() == 1) { - unsigned s = *subC.begin(); - wcore& c_s = m_cores[s]; - c_s.m_lower = refine(c_s.m_R, c_s.m_mid); - c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2)); - } - else { - wcore c_s; - rational delta = min_of_delta(subC); - rational lower = sum_of_lower(subC); - union_Rs(subC, c_s.m_R); - r = mk_fresh(); - relax(subC, soft, c_s.m_R, delta); - c_s.m_lower = refine(c_s.m_R, lower + delta - rational(1)); - c_s.m_upper = rational::one(); - c_s.m_upper += sum_of_sigmas(c_s.m_R); - c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2)); - c_s.m_r = r; - m_asm_set.insert(r); - subtract(m_cores, subC); - m_relax2index.insert(r, m_cores.size()); - m_cores.push_back(c_s); - } - break; - } - } - m_lower = compute_lower(); - } - normalize_bounds(); - return l_true; - } - - - private: - - void enable_soft_constraint(unsigned i) { - expr_ref fml(m); - expr* r = m_soft_aux[i].get(); - m_soft2index.insert(r, i); - fml = m.mk_or(r, m_soft[i]); - m_soft_constraints.push_back(fml); - m_asm_set.insert(r); - SASSERT(m_weights[i].is_int()); - } - - void assert_soft() { - for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { - s().assert_expr(m_soft_constraints[i].get()); - } - m_soft_constraints.reset(); - } - - bool check_lazy_soft(svector const& assignment) { - bool all_satisfied = true; - for (unsigned i = 0; i < m_lazy_soft.size(); ++i) { - unsigned j = m_lazy_soft[i]; - if (!assignment[j]) { - enable_soft_constraint(j); - m_lazy_soft[i] = m_lazy_soft.back(); - m_lazy_soft.pop_back(); - --i; - all_satisfied = false; - } - } - return all_satisfied; - } - - void normalize_bounds() { - m_lower /= m_den; - m_upper /= m_den; - } - - expr* mk_fresh() { - expr* r = mk_fresh_bool("r"); - m_trail.push_back(r); - return r; - } - - void update_assignment(svector& new_assignment) { - expr_ref val(m); - rational new_upper(0); - model_ref model; - new_assignment.reset(); - s().get_model(model); - for (unsigned i = 0; i < m_soft.size(); ++i) { - new_assignment.push_back(model->eval(m_soft[i], val) && m.is_true(val)); - if (!new_assignment[i]) { - new_upper += m_weights[i]; - } - } - if (new_upper < m_upper) { - m_upper = new_upper; - m_model = model; - m_assignment.reset(); - m_assignment.append(new_assignment); - } - } - - void update_sigmas() { - for (unsigned i = 0; i < m_cores.size(); ++i) { - wcore& c_i = m_cores[i]; - unsigned_vector const& R = c_i.m_R; - c_i.m_upper.reset(); - for (unsigned j = 0; j < R.size(); ++j) { - unsigned r_j = R[j]; - if (!m_assignment[r_j]) { - c_i.m_upper += m_weights[r_j]; - m_sigmas[r_j] = m_weights[r_j]; - } - else { - m_sigmas[r_j].reset(); - } - } - c_i.m_mid = div(c_i.m_lower + c_i.m_upper, rational(2)); - } - } - - /** - * Minimum of two (positive) numbers. Zero is treated as +infinity. - */ - rational min_z(rational const& a, rational const& b) { - if (a.is_zero()) return b; - if (b.is_zero()) return a; - if (a < b) return a; - return b; - } - - rational min_of_delta(uint_set const& subC) { - rational delta(0); - for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { - unsigned j = *it; - wcore const& core = m_cores[j]; - rational new_delta = rational(1) + core.m_upper - core.m_mid; - SASSERT(new_delta.is_pos()); - delta = min_z(delta, new_delta); - } - return delta; - } - - rational sum_of_lower(uint_set const& subC) { - rational lower(0); - for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { - lower += m_cores[*it].m_lower; - } - return lower; - } - - rational sum_of_sigmas(unsigned_vector const& R) { - rational sum(0); - for (unsigned i = 0; i < R.size(); ++i) { - sum += m_sigmas[R[i]]; - } - return sum; - } - void union_Rs(uint_set const& subC, unsigned_vector& R) { - for (uint_set::iterator it = subC.begin(); it != subC.end(); ++it) { - R.append(m_cores[*it].m_R); - } - } - rational compute_lower() { - rational result(0); - for (unsigned i = 0; i < m_cores.size(); ++i) { - result += m_cores[i].m_lower; - } - return result; - } - void subtract(vector& cores, uint_set const& subC) { - unsigned j = 0; - for (unsigned i = 0; i < cores.size(); ++i) { - if (subC.contains(i)) { - m_asm_set.remove(cores[i].m_r); - } - else { - if (j != i) { - cores[j] = cores[i]; - } - ++j; - } - } - cores.resize(j); - for (unsigned i = 0; i < cores.size(); ++i) { - m_relax2index.insert(cores[i].m_r, i); - } - } - void core2indices(ptr_vector const& core, uint_set& subC, uint_set& soft) { - for (unsigned i = 0; i < core.size(); ++i) { - unsigned j; - expr* a; - VERIFY(m.is_not(core[i], a)); - if (m_relax2index.find(a, j)) { - subC.insert(j); - } - else { - VERIFY(m_soft2index.find(a, j)); - soft.insert(j); - } - } - } - rational refine(unsigned_vector const& idx, rational v) { - return v + rational(1); - } - void relax(uint_set& subC, uint_set& soft, unsigned_vector& R, rational& delta) { - for (uint_set::iterator it = soft.begin(); it != soft.end(); ++it) { - R.push_back(*it); - delta = min_z(delta, m_weights[*it]); - m_asm_set.remove(m_soft_aux[*it].get()); - } - } - void assert_cores() { - for (unsigned i = 0; i < m_cores.size(); ++i) { - assert_core(m_cores[i]); - } - } - void assert_core(wcore const& core) { - expr_ref fml(m); - vector ws; - ptr_vector rs; - rational w(0); - for (unsigned j = 0; j < core.m_R.size(); ++j) { - unsigned idx = core.m_R[j]; - ws.push_back(m_weights[idx]); - w += ws.back(); - rs.push_back(m_soft_aux[idx].get()); - } - w.neg(); - w += core.m_mid; - ws.push_back(w); - rs.push_back(core.m_r); - fml = pb.mk_le(ws.size(), ws.c_ptr(), rs.c_ptr(), core.m_mid); - s().assert_expr(fml); - } - void display(std::ostream& out) { - out << "[" << m_lower << ":" << m_upper << "]\n"; - s().display(out); - out << "\n"; - for (unsigned i = 0; i < m_cores.size(); ++i) { - wcore const& c = m_cores[i]; - out << mk_pp(c.m_r, m) << ": "; - for (unsigned j = 0; j < c.m_R.size(); ++j) { - out << c.m_R[j] << " (" << m_sigmas[c.m_R[j]] << ") "; - } - out << "[" << c.m_lower << ":" << c.m_mid << ":" << c.m_upper << "]\n"; - } - for (unsigned i = 0; i < m_soft.size(); ++i) { - out << mk_pp(m_soft[i], m) << " " << m_weights[i] << "\n"; - } - } - }; - - maxsmt_solver_base* mk_bcd2( - maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) { - return alloc(bcd2, c, ws, soft); - } - -} diff --git a/src/opt/bcd2.h b/src/opt/bcd2.h deleted file mode 100644 index 50b7215e3..000000000 --- a/src/opt/bcd2.h +++ /dev/null @@ -1,28 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - bcd2.h - -Abstract: - - Bcd2 based MaxSAT. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-4-17 - -Notes: - ---*/ - -#ifndef BCD2_H_ -#define BCD2_H_ - -#include "maxsmt.h" - -namespace opt { - maxsmt_solver_base* mk_bcd2(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft); -} -#endif diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp deleted file mode 100644 index 48ef50cbc..000000000 --- a/src/opt/fu_malik.cpp +++ /dev/null @@ -1,237 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - fu_malik.cpp - -Abstract: - Fu & Malik built-in optimization method. - Adapted from sample code in C. - -Author: - - Anh-Dung Phan (t-anphan) 2013-10-15 - -Notes: - ---*/ - -#include "fu_malik.h" -#include "qfbv_tactic.h" -#include "tactic2solver.h" -#include "goal.h" -#include "probe.h" -#include "tactic.h" -#include "ast_pp.h" -#include "model_smt2_pp.h" -#include "opt_context.h" - -/** - \brief Fu & Malik procedure for MaxSAT. This procedure is based on - unsat core extraction and the at-most-one constraint. - - Return the number of soft-constraints that can be - satisfied. Return -1 if the hard-constraints cannot be - satisfied. That is, the formula cannot be satisfied even if all - soft-constraints are ignored. - - For more information on the Fu & Malik procedure: - - Z. Fu and S. Malik, On solving the partial MAX-SAT problem, in International - Conference on Theory and Applications of Satisfiability Testing, 2006. -*/ -namespace opt { - - class fu_malik : public maxsmt_solver_base { - filter_model_converter& m_fm; - expr_ref_vector m_aux_soft; - expr_ref_vector m_aux; - model_ref m_model; - - public: - fu_malik(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): - maxsmt_solver_base(c, ws, soft), - m_fm(c.fm()), - m_aux_soft(soft), - m_aux(m) - { - m_upper = rational(m_aux_soft.size() + 1); - m_lower.reset(); - m_assignment.resize(m_aux_soft.size(), false); - } - - /** - \brief One step of the Fu&Malik algorithm. - - Input: soft constraints + aux-vars (aka answer literals) - Output: done/not-done when not done return updated set of soft-constraints and aux-vars. - - if SAT --> terminates - - if UNSAT - * compute unsat core - * add blocking variable to soft-constraints in the core - - replace soft-constraint with the one with the blocking variable - - we should also add an aux-var - - replace aux-var with a new one - * add at-most-one constraint with blocking - */ - - typedef obj_hashtable expr_set; - - void set2vector(expr_set const& set, expr_ref_vector & es) const { - es.reset(); - expr_set::iterator it = set.begin(), end = set.end(); - for (; it != end; ++it) { - es.push_back(*it); - } - } - - void collect_statistics(statistics& st) const { - st.update("opt-fm-num-steps", m_aux_soft.size() + 2 - m_upper.get_unsigned()); - } - - void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const { - set.reset(); - expr_set::iterator it = set1.begin(), end = set1.end(); - for (; it != end; ++it) { - set.insert(*it); - } - it = set2.begin(); - end = set2.end(); - for (; it != end; ++it) { - set.insert(*it); - } - } - - lbool step() { - IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_aux_soft.size() + 2 - m_upper.get_unsigned() << ")\n";); - expr_ref_vector assumptions(m), block_vars(m); - for (unsigned i = 0; i < m_aux_soft.size(); ++i) { - assumptions.push_back(m.mk_not(m_aux[i].get())); - } - lbool is_sat = s().check_sat(assumptions.size(), assumptions.c_ptr()); - if (is_sat != l_false) { - return is_sat; - } - - ptr_vector core; - s().get_unsat_core(core); - - SASSERT(!core.empty()); - - // Update soft-constraints and aux_vars - for (unsigned i = 0; i < m_aux_soft.size(); ++i) { - - bool found = false; - for (unsigned j = 0; !found && j < core.size(); ++j) { - found = assumptions[i].get() == core[j]; - } - if (!found) { - continue; - } - app_ref block_var(m), tmp(m); - block_var = m.mk_fresh_const("block_var", m.mk_bool_sort()); - m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort()); - m_fm.insert(block_var->get_decl()); - m_fm.insert(to_app(m_aux[i].get())->get_decl()); - m_aux_soft[i] = m.mk_or(m_aux_soft[i].get(), block_var); - block_vars.push_back(block_var); - tmp = m.mk_or(m_aux_soft[i].get(), m_aux[i].get()); - s().assert_expr(tmp); - } - SASSERT (!block_vars.empty()); - assert_at_most_one(block_vars); - IF_VERBOSE(1, verbose_stream() << "(opt.max_sat # of non-blocked soft constraints: " << m_aux_soft.size() - block_vars.size() << ")\n";); - return l_false; - } - - void assert_at_most_one(expr_ref_vector const& block_vars) { - expr_ref has_one(m), has_zero(m), at_most_one(m); - mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, has_zero); - at_most_one = m.mk_or(has_one, has_zero); - s().assert_expr(at_most_one); - } - - void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& has_zero) { - SASSERT(n != 0); - if (n == 1) { - has_one = vars[0]; - has_zero = m.mk_not(vars[0]); - } - else { - unsigned mid = n/2; - expr_ref has_one1(m), has_one2(m), has_zero1(m), has_zero2(m); - mk_at_most_one(mid, vars, has_one1, has_zero1); - mk_at_most_one(n-mid, vars+mid, has_one2, has_zero2); - has_one = m.mk_or(m.mk_and(has_one1, has_zero2), m.mk_and(has_one2, has_zero1)); - has_zero = m.mk_and(has_zero1, has_zero2); - } - } - - - // TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef - virtual lbool operator()() { - lbool is_sat = l_true; - if (m_aux_soft.empty()) { - return is_sat; - } - solver::scoped_push _sp(s()); - expr_ref tmp(m); - - TRACE("opt", - tout << "soft constraints:\n"; - for (unsigned i = 0; i < m_aux_soft.size(); ++i) { - tout << mk_pp(m_aux_soft[i].get(), m) << "\n"; - }); - - for (unsigned i = 0; i < m_aux_soft.size(); ++i) { - m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort())); - m_fm.insert(to_app(m_aux.back())->get_decl()); - tmp = m.mk_or(m_aux_soft[i].get(), m_aux[i].get()); - s().assert_expr(tmp); - } - - do { - is_sat = step(); - --m_upper; - } - while (is_sat == l_false); - - if (is_sat == l_true) { - // Get a list satisfying m_aux_soft - s().get_model(m_model); - m_lower = m_upper; - m_assignment.reset(); - for (unsigned i = 0; i < m_soft.size(); ++i) { - expr_ref val(m); - if (!m_model->eval(m_soft[i], val)) return l_undef; - TRACE("opt", tout << val << "\n";); - m_assignment.push_back(m.is_true(val)); - } - TRACE("opt", tout << "maxsat cost: " << m_upper << "\n"; - model_smt2_pp(tout, m, *m_model, 0);); - } - // We are done and soft_constraints has - // been updated with the max-sat assignment. - return is_sat; - } - - virtual void get_model(model_ref& mdl) { - mdl = m_model.get(); - } - - virtual rational get_lower() const { - return rational(m_aux_soft.size())-m_upper; - } - - virtual rational get_upper() const { - return rational(m_aux_soft.size())-m_lower; - } - }; - - maxsmt_solver_base* mk_fu_malik(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft) { - return alloc(fu_malik, c, ws, soft); - } - -}; - diff --git a/src/opt/fu_malik.h b/src/opt/fu_malik.h deleted file mode 100644 index 52e960b5e..000000000 --- a/src/opt/fu_malik.h +++ /dev/null @@ -1,37 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - fu_malik.h - -Abstract: - - Fu&Malik built-in optimization method. - Adapted from sample code in C. - -Author: - - Anh-Dung Phan (t-anphan) 2013-10-15 - -Notes: - - Takes solver with hard constraints added. - Returns a maximal satisfying subset of soft_constraints - that are still consistent with the solver state. - ---*/ -#ifndef OPT_FU_MALIK_H_ -#define OPT_FU_MALIK_H_ - -#include "opt_solver.h" -#include "maxsmt.h" - -namespace opt { - - maxsmt_solver_base* mk_fu_malik(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft); - - -}; - -#endif diff --git a/src/opt/hitting_sets.cpp b/src/opt/hitting_sets.cpp deleted file mode 100644 index 678d7924e..000000000 --- a/src/opt/hitting_sets.cpp +++ /dev/null @@ -1,1088 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - hitting_sets.h - -Abstract: - - Hitting set approximations. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-06-06 - -Notes: - ---*/ -#include "vector.h" -#include "util.h" -#include "hitting_sets.h" -#include "simplex.h" -#include "sparse_matrix_def.h" -#include "simplex_def.h" - -typedef simplex::simplex Simplex; -typedef simplex::sparse_matrix sparse_matrix; - - -namespace opt { - - struct hitting_sets::imp { - class justification { - public: - enum kind_t { AXIOM, DECISION, CLAUSE }; - private: - kind_t m_kind; - unsigned m_value; - bool m_pos; - public: - explicit justification(kind_t k):m_kind(k), m_value(0), m_pos(false) {} - explicit justification(unsigned v, bool pos):m_kind(CLAUSE), m_value(v), m_pos(pos) {} - justification(justification const& other): - m_kind(other.m_kind), m_value(other.m_value), m_pos(other.m_pos) {} - justification& operator=(justification const& other) { - m_kind = other.m_kind; - m_value = other.m_value; - m_pos = other.m_pos; - return *this; - } - unsigned clause() const { return m_value; } - bool is_axiom() const { return m_kind == AXIOM; } - bool is_decision() const { return m_kind == DECISION; } - bool is_clause() const { return m_kind == CLAUSE; } - kind_t kind() const { return m_kind; } - bool pos() const { return m_pos; } - }; - - class set { - unsigned m_num_elems; - unsigned m_elems[0]; - set(): m_num_elems(0) {} - public: - - static set* mk(small_object_allocator& alloc, unsigned sz, unsigned const* elems) { - unsigned size = (sz+1)*sizeof(unsigned); - void * mem = alloc.allocate(size); - set* result = new (mem) set(); - result->m_num_elems = sz; - memcpy(result->m_elems, elems, sizeof(unsigned)*sz); - return result; - } - - inline unsigned operator[](unsigned idx) const { - SASSERT(idx < m_num_elems); - return m_elems[idx]; - } - - inline unsigned& operator[](unsigned idx) { - SASSERT(idx < m_num_elems); - return m_elems[idx]; - } - - unsigned size() const { return m_num_elems; } - - unsigned alloc_size() const { return (m_num_elems + 1)*sizeof(unsigned); } - - bool empty() const { return 0 == size(); } - }; - - reslimit& m_limit; - rational m_lower; - rational m_upper; - vector m_weights; - vector m_weights_inv; - rational m_max_weight; - rational m_denominator; - small_object_allocator m_alloc; - ptr_vector m_T; - ptr_vector m_F; - svector m_value; - svector m_model; - vector m_tuse_list; - vector m_fuse_list; - - // Custom CDCL solver. - svector m_justification; - vector m_twatch; - vector m_fwatch; - unsigned_vector m_level; - unsigned_vector m_trail; // trail of assigned literals - unsigned m_qhead; // queue head - justification m_conflict_j; // conflict justification - unsigned m_conflict_l; // conflict literal - bool m_inconsistent; - unsigned m_scope_lvl; - rational m_weight; // current weight of assignment. - unsigned_vector m_indices; - unsigned_vector m_scores; - vector m_scored_weights; - svector m_score_updated; - bool m_enable_simplex; - struct compare_scores { - imp* m_imp; - compare_scores():m_imp(0) {} - bool operator()(int v1, int v2) const { - return m_imp->m_scored_weights[v1] > m_imp->m_scored_weights[v2]; - } - }; - compare_scores m_compare_scores; - heap m_heap; - svector m_mark; - struct scope { - unsigned m_trail_lim; - }; - vector m_scopes; - unsigned_vector m_lemma; - unsigned m_conflict_lvl; - - // simplex - unsynch_mpz_manager m; - Simplex m_simplex; - unsigned m_weights_var; - - static unsigned const null_idx = UINT_MAX; - - imp(reslimit& lim): - m_limit(lim), - m_max_weight(0), - m_denominator(1), - m_alloc("hitting-sets"), - m_qhead(0), - m_conflict_j(justification(justification::AXIOM)), - m_inconsistent(false), - m_scope_lvl(0), - m_compare_scores(), - m_heap(0, m_compare_scores), - m_simplex(lim), - m_weights_var(0) { - m_enable_simplex = true; - m_compare_scores.m_imp = this; - } - ~imp() { - for (unsigned i = 0; i < m_T.size(); ++i) { - m_alloc.deallocate(m_T[i]->alloc_size(), m_T[i]); - } - for (unsigned i = 0; i < m_F.size(); ++i) { - m_alloc.deallocate(m_F[i]->alloc_size(), m_F[i]); - } - } - - void add_weight(rational const& w) { - SASSERT(w.is_pos()); - unsigned var = m_weights.size(); - m_simplex.ensure_var(var); - m_simplex.set_lower(var, mpq_inf(mpq(0),mpq(0))); - m_simplex.set_upper(var, mpq_inf(mpq(1),mpq(0))); - m_weights.push_back(w); - m_weights_inv.push_back(rational::one()); - m_value.push_back(l_undef); - m_justification.push_back(justification(justification::DECISION)); - m_tuse_list.push_back(unsigned_vector()); - m_fuse_list.push_back(unsigned_vector()); - m_twatch.push_back(unsigned_vector()); - m_fwatch.push_back(unsigned_vector()); - m_level.push_back(0); - m_indices.push_back(var); - m_model.push_back(l_undef); - m_mark.push_back(false); - m_scores.push_back(0); - m_scored_weights.push_back(rational(0)); - m_score_updated.push_back(true); - m_max_weight += w; - } - - justification add_exists_false(unsigned sz, unsigned const* S) { - return add_exists(sz, S, true); - } - - justification add_exists_true(unsigned sz, unsigned const* S) { - return add_exists(sz, S, false); - } - - justification add_exists(unsigned sz, unsigned const* S, bool sign) { - vector& use_list = sign?m_fuse_list:m_tuse_list; - lbool val = sign?l_false:l_true; - justification j(justification::AXIOM); - ptr_vector& Sets = sign?m_F:m_T; - vector& watch = sign?m_fwatch:m_twatch; - init_weights(); - if (sz == 0) { - set_conflict(0, justification(justification::AXIOM)); - } - else if (sz == 1) { - IF_VERBOSE(2, verbose_stream() << "unit literal : " << S[0] << " " << val << "\n";); - assign(S[0], val, justification(justification::AXIOM)); - } - else { - unsigned clause_id = Sets.size(); - for (unsigned i = 0; i < sz; ++i) { - use_list[S[i]].push_back(clause_id); - } - j = justification(clause_id, !sign); - watch[S[0]].push_back(clause_id); - watch[S[1]].push_back(clause_id); - Sets.push_back(set::mk(m_alloc, sz, S)); - if (!sign) { - pop(scope_lvl()); - inc_score(clause_id); - } - TRACE("opt", display(tout, j);); - IF_VERBOSE(2, if (!sign) display(verbose_stream(), j);); - if (!sign && m_enable_simplex) { - add_simplex_row(!sign, sz, S); - } - } - return j; - } - - lbool compute_lower() { - m_lower.reset(); - rational w1 = L1(); - rational w2 = L2(); - rational w3 = L3(); - if (w1 > m_lower) m_lower = w1; - if (w2 > m_lower) m_lower = w2; - if (w3 > m_lower) m_lower = w3; - return l_true; - } - - lbool compute_upper() { - m_upper = m_max_weight; - unsigned fsz = m_F.size(); - lbool r = search(); - pop(scope_lvl()); - - - IF_VERBOSE(1, verbose_stream() << "(hsmax.negated-size: " << fsz << ")\n";); -#if 0 - // garbage collect agressively on exit. - // all learned clases for negative branches are - // pruned. - for (unsigned i = fsz; i < m_F.size(); ++i) { - m_alloc.deallocate(m_F[i]->alloc_size(), m_F[i]); - } - m_F.resize(fsz); - for (unsigned i = 0; i < m_fuse_list.size(); ++i) { - unsigned_vector & uses = m_fuse_list[i]; - while (!uses.empty() && uses.back() >= fsz) uses.pop_back(); - unsigned_vector & watch = m_fwatch[i]; - unsigned j = 0, k = 0; - for (; j < watch.size(); ++j) { - if (watch[j] < fsz) { - watch[k] = watch[j]; - ++k; - } - } - watch.resize(k); - } -#endif - return r; - } - - rational get_lower() { - return m_lower/m_denominator; - } - - rational get_upper() { - return m_upper/m_denominator; - } - - void set_upper(rational const& r) { - m_max_weight = r*m_denominator; - } - - bool get_value(unsigned idx) { - return - idx < m_model.size() && - m_model[idx] == l_true; - } - - void collect_statistics(::statistics& st) const { - m_simplex.collect_statistics(st); - } - - void reset() { - m_lower.reset(); - m_upper = m_max_weight; - } - - void init_weights() { - if (m_weights_var != 0) { - return; - } - m_weights_var = m_weights.size(); - unsigned_vector vars; - scoped_mpz_vector coeffs(m); - - // normalize weights to integral. - rational d(1); - for (unsigned i = 0; i < m_weights.size(); ++i) { - d = lcm(d, denominator(m_weights[i])); - } - m_denominator = d; - if (!d.is_one()) { - for (unsigned i = 0; i < m_weights.size(); ++i) { - m_weights[i] *= d; - } - } - rational lc(1); - for (unsigned i = 0; i < m_weights.size(); ++i) { - lc = lcm(lc, m_weights[i]); - } - for (unsigned i = 0; i < m_weights.size(); ++i) { - m_weights_inv[i] = lc/m_weights[i]; - } - - m_heap.set_bounds(m_weights.size()); - for (unsigned i = 0; i < m_weights.size(); ++i) { - m_heap.insert(i); - } - update_heap(); - - // set up Simplex objective function. - for (unsigned i = 0; i < m_weights.size(); ++i) { - vars.push_back(i); - coeffs.push_back(m_weights[i].to_mpq().numerator()); - } - m_simplex.ensure_var(m_weights_var); - vars.push_back(m_weights_var); - coeffs.push_back(mpz(-1)); - m_simplex.add_row(m_weights_var, coeffs.size(), vars.c_ptr(), coeffs.c_ptr()); - - } - - void display(std::ostream& out) const { - out << "inconsistent: " << m_inconsistent << "\n"; - out << "weight: " << m_weight << "\n"; - for (unsigned i = 0; i < m_weights.size(); ++i) { - out << i << ": " << value(i) << " w: " << m_weights[i] << " s: " << m_scores[i] << "\n"; - } - for (unsigned i = 0; i < m_T.size(); ++i) { - display(out << "+" << i << ": ", *m_T[i]); - } - for (unsigned i = 0; i < m_F.size(); ++i) { - display(out << "-" << i << ": ", *m_F[i]); - } - out << "watch lists:\n"; - for (unsigned i = 0; i < m_fwatch.size(); ++i) { - out << i << ": "; - for (unsigned j = 0; j < m_twatch[i].size(); ++j) { - out << "+" << m_twatch[i][j] << " "; - } - for (unsigned j = 0; j < m_fwatch[i].size(); ++j) { - out << "-" << m_fwatch[i][j] << " "; - } - out << "\n"; - } - out << "trail\n"; - for (unsigned i = 0; i < m_trail.size(); ++i) { - unsigned idx = m_trail[i]; - out << (m_justification[idx].is_decision()?"d":"") << idx << " "; - } - out << "\n"; - } - - void display(std::ostream& out, set const& S) const { - for (unsigned i = 0; i < S.size(); ++i) { - out << S[i] << " "; - } - out << "\n"; - } - - void display(std::ostream& out, justification const& j) const { - switch(j.kind()) { - case justification::AXIOM: - out << "axiom\n"; - break; - case justification::DECISION: - out << "decision\n"; - break; - case justification::CLAUSE: { - out << "clause: "; - set const& S = j.pos()?(*m_T[j.clause()]):(*m_F[j.clause()]); - for (unsigned i = 0; i < S.size(); ++i) { - out << S[i] << " "; - } - out << "\n"; - } - } - } - - void display_lemma(std::ostream& out) { - out << "lemma: "; - for (unsigned i = 0; i < m_lemma.size(); ++i) { - out << m_lemma[i] << " "; - } - out << "\n"; - } - - struct scoped_push { - imp& s; - scoped_push(imp& s):s(s) { s.push(); } - ~scoped_push() { s.pop(1); } - }; - - struct value_lt { - vector const& weights; - value_lt(vector const& weights): - weights(weights) {} - bool operator()(int v1, int v2) const { - return weights[v1] > weights[v2]; - } - }; - - void inc_score(unsigned clause_id) { - set const& S = *m_T[clause_id]; - if (!has_selected(S)) { - for (unsigned j = 0; j < S.size(); ++j) { - ++m_scores[S[j]]; - m_score_updated[S[j]] = true; - } - } - } - - void dec_score(unsigned clause_id) { - set const& S = *m_T[clause_id]; - if (!has_selected(S)) { - for (unsigned j = 0; j < S.size(); ++j) { - SASSERT(m_scores[S[j]] > 0); - --m_scores[S[j]]; - m_score_updated[S[j]] = true; - } - } - } - - void update_score(unsigned idx, bool inc) { - unsigned_vector const& uses = m_tuse_list[idx]; - for (unsigned i = 0; i < uses.size(); ++i) { - if (inc) { - inc_score(uses[i]); - } - else { - dec_score(uses[i]); - } - } - } - - rational L1() { - rational w(m_weight); - scoped_push _sc(*this); - for (unsigned i = 0; !canceled() && i < m_T.size(); ++i) { - set const& S = *m_T[i]; - SASSERT(!S.empty()); - if (!has_selected(S)) { - w += m_weights[select_min(S)]; - for (unsigned j = 0; j < S.size(); ++j) { - assign(S[j], l_true, justification(justification::DECISION)); - } - } - } - return w; - } - - void update_heap() { - for (unsigned i = 0; i < m_scored_weights.size(); ++i) { - if (m_score_updated[i]) { - rational const& old_w = m_scored_weights[i]; - rational new_w = rational(m_scores[i])*m_weights_inv[i]; - if (new_w > old_w) { - m_scored_weights[i] = new_w; - //m_heap.decreased(i); - } - else if (new_w < old_w) { - m_scored_weights[i] = new_w; - //m_heap.increased(i); - } - m_score_updated[i] = false; - } - } - } - - rational L2() { - rational w(m_weight); - scoped_push _sc(*this); - int n = 0; - for (unsigned i = 0; i < m_T.size(); ++i) { - if (!has_selected(*m_T[i])) ++n; - } - - update_heap(); - value_lt lt(m_scored_weights); - std::sort(m_indices.begin(), m_indices.end(), lt); - for(unsigned i = 0; i < m_indices.size() && n > 0; ++i) { - // deg(c) = score(c) - // wt(c) = m_weights[c] - - unsigned idx = m_indices[i]; - if (m_scores[idx] == 0) { - break; - } - if (m_scores[idx] < static_cast(n) || m_weights[idx].is_one()) { - w += m_weights[idx]; - } - else { - w += div((rational(n)*m_weights[idx]), rational(m_scores[idx])); - } - n -= m_scores[idx]; - } - return w; - } - - rational L3() { - TRACE("simplex", m_simplex.display(tout);); - VERIFY(l_true == m_simplex.make_feasible()); - TRACE("simplex", m_simplex.display(tout);); - VERIFY(l_true == m_simplex.minimize(m_weights_var)); - mpq_inf const& val = m_simplex.get_value(m_weights_var); - unsynch_mpq_inf_manager mg; - unsynch_mpq_manager& mq = mg.get_mpq_manager(); - scoped_mpq c(mq); - mg.ceil(val, c); - rational w(c); - CTRACE("simplex", - w >= m_weight, tout << w << " " << m_weight << " !!!!\n"; - display(tout);); - SASSERT(w >= m_weight); - return w; - } - - void add_simplex_row(bool is_some_true, unsigned sz, unsigned const* S) { - unsigned_vector vars; - scoped_mpz_vector coeffs(m); - for (unsigned i = 0; i < sz; ++i) { - vars.push_back(S[i]); - coeffs.push_back(mpz(1)); - } - unsigned base_var = m_F.size() + m_T.size() + m_weights.size(); - m_simplex.ensure_var(base_var); - vars.push_back(base_var); - coeffs.push_back(mpz(-1)); - // S - base_var = 0 - if (is_some_true) { - // base_var >= 1 - m_simplex.set_lower(base_var, mpq_inf(mpq(1),mpq(0))); - } - else { - // base_var <= sz-1 - m_simplex.set_upper(base_var, mpq_inf(mpq(sz-1),mpq(0))); - } - m_simplex.add_row(base_var, coeffs.size(), vars.c_ptr(), coeffs.c_ptr()); - } - - unsigned select_min(set const& S) { - unsigned result = S[0]; - for (unsigned i = 1; i < S.size(); ++i) { - if (m_weights[result] > m_weights[S[i]]) { - result = S[i]; - } - } - return result; - } - - bool have_selected(lbool val, ptr_vector const& Sets, unsigned& i) { - for (i = 0; i < Sets.size(); ++i) { - if (!has_selected(val, *Sets[i])) return false; - } - return true; - } - - void set_undef_to_false() { - for (unsigned i = 0; i < m_model.size(); ++i) { - if (m_model[i] == l_undef) { - m_model[i] = l_false; - } - } - } - - bool values_satisfy_Fs(unsigned& i) { - unsigned j = 0; - for (i = 0; i < m_F.size(); ++i) { - set const& F = *m_F[i]; - for (j = 0; j < F.size(); ++j) { - if (m_model[F[j]] == l_false) { - break; - } - } - if (F.size() == j) { - break; - } - } - return i == m_F.size(); - } - - bool has_selected(set const& S) { - return has_selected(l_true, S); - } - - bool has_unselected(set const& S) { - return has_selected(l_false, S); - } - - bool has_unset(set const& S) { - return has_selected(l_undef, S); - } - - bool has_selected(lbool val, set const& S) { - for (unsigned i = 0; i < S.size(); ++i) { - if (val == value(S[i])) { - return true; - } - } - return false; - } - - // (greedy) CDCL learner for hitting sets. - - inline unsigned scope_lvl() const { return m_scope_lvl; } - inline bool inconsistent() const { return m_inconsistent; } - inline bool canceled() const { return !m_limit.inc(); } - inline unsigned lvl(unsigned idx) const { return m_level[idx]; } - inline lbool value(unsigned idx) const { return m_value[idx]; } - - inline bool is_marked(unsigned v) const { return m_mark[v] != 0; } - inline void mark(unsigned v) { SASSERT(!is_marked(v)); m_mark[v] = true; } - inline void reset_mark(unsigned v) { SASSERT(is_marked(v)); m_mark[v] = false; } - - void push() { - SASSERT(!inconsistent()); - ++m_scope_lvl; - m_scopes.push_back(scope()); - scope& s = m_scopes.back(); - s.m_trail_lim = m_trail.size(); - } - - void pop(unsigned n) { - if (n > 0) { - m_inconsistent = false; - m_scope_lvl = scope_lvl() - n; - unassign(m_scopes[scope_lvl()].m_trail_lim); - m_scopes.shrink(scope_lvl()); - } - } - - void assign(unsigned idx, lbool val, justification const& justification) { - if (val == l_true) { - m_weight += m_weights[idx]; - update_score(idx, false); - if (m_enable_simplex) { - m_simplex.set_lower(idx, mpq_inf(mpq(1),mpq(0))); - } - } - SASSERT(val != l_true || m_scores[idx] == 0); - m_value[idx] = val; - m_justification[idx] = justification; - m_trail.push_back(idx); - m_level[idx] = scope_lvl(); - TRACE("opt", tout << idx << " := " << val << " scope: " << scope_lvl() << " w: " << m_weight << "\n";); - } - - - svector m_replay_idx; - svector m_replay_val; - void unassign(unsigned sz) { - for (unsigned j = sz; j < m_trail.size(); ++j) { - unsigned idx = m_trail[j]; - lbool val = value(idx); - m_value[idx] = l_undef; - if (val == l_true) { - m_weight -= m_weights[idx]; - update_score(idx, true); - if (m_enable_simplex) { - m_simplex.set_lower(idx, mpq_inf(mpq(0),mpq(0))); - } - } - if (m_justification[idx].is_axiom()) { - m_replay_idx.push_back(idx); - m_replay_val.push_back(val); - } - } - TRACE("opt", tout << m_weight << "\n";); - m_trail.shrink(sz); - m_qhead = sz; - for (unsigned i = m_replay_idx.size(); i > 0; ) { - --i; - unsigned idx = m_replay_idx[i]; - lbool val = m_replay_val[i]; - assign(idx, val, justification(justification::AXIOM)); - } - m_replay_idx.reset(); - m_replay_val.reset(); - } - - - lbool search() { - TRACE("opt", display(tout);); - pop(scope_lvl()); - while (true) { - while (true) { - propagate(); - if (canceled()) return l_undef; - if (!inconsistent()) break; - if (!resolve_conflict()) return l_false; - SASSERT(!inconsistent()); - } - if (!decide()) { - SASSERT(validate_model()); - m_model.reset(); - m_model.append(m_value); - m_upper = m_weight; - // SASSERT(m_weight < m_max_weight); - return l_true; - } - } - } - - bool validate_model() { - for (unsigned i = 0; i < m_T.size(); ++i) { - set const& S = *m_T[i]; - bool found = false; - for (unsigned j = 0; !found && j < S.size(); ++j) { - found = value(S[j]) == l_true; - } - CTRACE("opt", !found, - display(tout << "not found: " << i << "\n", S); - display(tout);); - SASSERT(found); - } - for (unsigned i = 0; i < m_F.size(); ++i) { - set const& S = *m_F[i]; - bool found = false; - for (unsigned j = 0; !found && j < S.size(); ++j) { - found = value(S[j]) != l_true; - } - CTRACE("opt", !found, - display(tout << "not found: " << i << "\n", S); - display(tout);); - SASSERT(found); - } - - return true; - } - - bool invariant() { - DEBUG_CODE( - for (unsigned i = 0; i < m_fwatch.size(); ++i) { - for (unsigned j = 0; j < m_fwatch[i].size(); ++j) { - set const& S = *m_F[m_fwatch[i][j]]; - SASSERT(S[0] == i || S[1] == i); - } - } - for (unsigned i = 0; i < m_twatch.size(); ++i) { - for (unsigned j = 0; j < m_twatch[i].size(); ++j) { - set const& S = *m_T[m_twatch[i][j]]; - SASSERT(S[0] == i || S[1] == i); - } - }); - return true; - } - - bool resolve_conflict() { - while (true) { - if (!resolve_conflict_core()) return false; - if (!inconsistent()) return true; - } - } - - unsigned get_max_lvl(unsigned conflict_l, justification const& conflict_j) { - if (scope_lvl() == 0) return 0; - unsigned r = lvl(conflict_l); - if (conflict_j.is_clause()) { - unsigned clause = conflict_j.clause(); - ptr_vector const& S = conflict_j.pos()?m_T:m_F; - r = std::max(r, lvl((*S[clause])[0])); - r = std::max(r, lvl((*S[clause])[1])); - } - return r; - } - - bool resolve_conflict_core() { - SASSERT(inconsistent()); - TRACE("opt", display(tout);); - unsigned conflict_l = m_conflict_l; - justification conflict_j(m_conflict_j); - if (conflict_j.is_axiom()) { - return false; - } - m_conflict_lvl = get_max_lvl(conflict_l, conflict_j); - if (m_conflict_lvl == 0) { - return false; - } - unsigned idx = skip_above_conflict_level(); - unsigned num_marks = 0; - m_lemma.reset(); - m_lemma.push_back(0); - process_antecedent(conflict_l, num_marks); - do { - TRACE("opt", tout << "conflict literal: " << conflict_l << "\n"; - display(tout, conflict_j);); - if (conflict_j.is_clause()) { - unsigned cl = conflict_j.clause(); - unsigned i = 0; - SASSERT(value(conflict_l) != l_undef); - set const& T = conflict_j.pos()?(*m_T[cl]):(*m_F[cl]); - if (T[0] == conflict_l) { - i = 1; - } - else { - SASSERT(T[1] == conflict_l); - process_antecedent(T[0], num_marks); - i = 2; - } - unsigned sz = T.size(); - for (; i < sz; ++i) { - process_antecedent(T[i], num_marks); - } - } - else if (conflict_j.is_decision()) { - --num_marks; - SASSERT(num_marks == 0); - break; - } - else if (conflict_j.is_axiom()) { - IF_VERBOSE(0, verbose_stream() << "axiom " << conflict_l << " " << value(conflict_l) << " " << num_marks << "\n";); - --num_marks; - SASSERT(num_marks == 0); - break; - } - while (true) { - unsigned l = m_trail[idx]; - if (is_marked(l)) break; - SASSERT(idx > 0); - --idx; - } - conflict_l = m_trail[idx]; - conflict_j = m_justification[conflict_l]; - --idx; - --num_marks; - if (num_marks == 0 && value(conflict_l) == l_false) { - ++num_marks; - } - reset_mark(conflict_l); - } - while (num_marks > 0); - m_lemma[0] = conflict_l; - TRACE("opt", display_lemma(tout);); - SASSERT(value(conflict_l) == l_true); - unsigned new_scope_lvl = 0; - for (unsigned i = 1; i < m_lemma.size(); ++i) { - SASSERT(l_true == value(m_lemma[i])); - new_scope_lvl = std::max(new_scope_lvl, lvl(m_lemma[i])); - reset_mark(m_lemma[i]); - } - pop(scope_lvl() - new_scope_lvl); - SASSERT(l_undef == value(conflict_l)); - justification j = add_exists_false(m_lemma.size(), m_lemma.c_ptr()); - if (!j.is_axiom()) assign(conflict_l, l_false, j); - return true; - } - - - void process_antecedent(unsigned antecedent, unsigned& num_marks) { - unsigned alvl = lvl(antecedent); - SASSERT(alvl <= m_conflict_lvl); - if (!is_marked(antecedent) && alvl > 0 && !m_justification[antecedent].is_axiom()) { - mark(antecedent); - if (alvl == m_conflict_lvl || value(antecedent) == l_false) { - ++num_marks; - } - else { - m_lemma.push_back(antecedent); - } - } - } - - unsigned skip_above_conflict_level() { - unsigned idx = m_trail.size(); - if (idx == 0) { - return idx; - } - idx--; - // skip literals from levels above the conflict level - while (lvl(m_trail[idx]) > m_conflict_lvl) { - SASSERT(idx > 0); - idx--; - } - return idx; - } - - void set_conflict(unsigned idx, justification const& justification) { - if (!inconsistent()) { - TRACE("opt", tout << "conflict: " << idx << "\n";); - m_inconsistent = true; - m_conflict_j = justification; - m_conflict_l = idx; - } - } - - unsigned next_var() { - update_heap(); - - value_lt lt(m_scored_weights); - std::sort(m_indices.begin(), m_indices.end(), lt); - unsigned idx = m_indices[0]; - if (m_scores[idx] == 0) return UINT_MAX; - return idx; -#if 0 - int min_val = m_heap.min_value(); - if (min_val == -1) { - return UINT_MAX; - } - SASSERT(0 <= min_val && static_cast(min_val) < m_weights.size()); - if (m_scores[min_val] == 0) { - return UINT_MAX; - } - return static_cast(min_val); -#endif - } - - bool decide() { - unsigned idx = next_var(); - if (idx == UINT_MAX) { - return false; - } - else { - push(); - TRACE("opt", tout << "decide " << idx << "\n";); - assign(idx, l_true, justification(justification::DECISION)); - return true; - } - } - - void propagate() { - TRACE("opt", display(tout);); - SASSERT(invariant()); - while (m_qhead < m_trail.size() && !inconsistent() && !canceled()) { - unsigned idx = m_trail[m_qhead]; - ++m_qhead; - switch (value(idx)) { - case l_undef: - UNREACHABLE(); - break; - case l_true: - propagate(idx, l_false, m_fwatch, m_F); - break; - case l_false: - propagate(idx, l_true, m_twatch, m_T); - break; - } - } - prune_branch(); - } - - void propagate(unsigned idx, lbool good_val, vector& watch, ptr_vector& Fs) - { - TRACE("opt", tout << idx << " " << value(idx) << "\n";); - unsigned_vector& w = watch[idx]; - unsigned sz = w.size(); - lbool bad_val = ~good_val; - SASSERT(value(idx) == bad_val); - unsigned l = 0; - for (unsigned i = 0; i < sz && !canceled(); ++i, ++l) { - unsigned clause_id = w[i]; - set& F = *Fs[clause_id]; - SASSERT(F.size() >= 2); - bool k1 = (F[0] != idx); - bool k2 = !k1; - SASSERT(F[k1] == idx); - SASSERT(value(F[k1]) == bad_val); - if (value(F[k2]) == good_val) { - w[l] = w[i]; - continue; - } - bool found = false; - unsigned sz2 = F.size(); - for (unsigned j = 2; !found && j < sz2; ++j) { - unsigned idx2 = F[j]; - if (value(idx2) != bad_val) { - found = true; - std::swap(F[k1], F[j]); - --l; - watch[idx2].push_back(clause_id); - } - } - if (!found) { - if (value(F[k2]) == bad_val) { - set_conflict(F[k2], justification(clause_id, good_val == l_true)); - if (i == l) { - l = sz; - } - else { - for (; i < sz; ++i, ++l) { - w[l] = w[i]; - } - } - break; - } - else { - SASSERT(value(F[k2]) == l_undef); - assign(F[k2], good_val, justification(clause_id, good_val == l_true)); - w[l] = w[i]; - } - } - } - watch[idx].shrink(l); - SASSERT(invariant()); - TRACE("opt", tout << idx << " " << value(idx) << "\n";); - SASSERT(value(idx) == bad_val); - } - - bool infeasible_lookahead() { - if (m_enable_simplex && L3() >= m_max_weight) { - return true; - } - return - (L1() >= m_max_weight) || - (L2() >= m_max_weight); - } - - void prune_branch() { - if (inconsistent() || !infeasible_lookahead()) { - return; - } - - IF_VERBOSE(4, verbose_stream() << "(hs.prune-branch " << m_weight << ")\n";); - m_lemma.reset(); - unsigned i = 0; - rational w(0); - for (; i < m_trail.size() && w < m_max_weight; ++i) { - unsigned idx = m_trail[i]; - if (m_justification[idx].is_decision()) { - SASSERT(value(idx) == l_true); - m_lemma.push_back(idx); - w += m_weights[idx]; - } - } - // undo the lower bounds. - TRACE("opt", - tout << "prune branch: " << m_weight << " "; - display_lemma(tout); - display(tout); - ); - justification j = add_exists_false(m_lemma.size(), m_lemma.c_ptr()); - unsigned idx = m_lemma.empty()?0:m_lemma[0]; - set_conflict(idx, j); - } - - // TBD: derive strong inequalities and add them to Simplex. - // x_i1 + .. + x_ik >= k-1 for each subset k from set n: x_1 + .. + x_n >= k - }; - - - hitting_sets::hitting_sets(reslimit& lim) { m_imp = alloc(imp, lim); } - hitting_sets::~hitting_sets() { dealloc(m_imp); } - void hitting_sets::add_weight(rational const& w) { m_imp->add_weight(w); } - void hitting_sets::add_exists_true(unsigned sz, unsigned const* elems) { m_imp->add_exists_true(sz, elems); } - void hitting_sets::add_exists_false(unsigned sz, unsigned const* elems) { m_imp->add_exists_false(sz, elems); } - lbool hitting_sets::compute_lower() { return m_imp->compute_lower(); } - lbool hitting_sets::compute_upper() { return m_imp->compute_upper(); } - rational hitting_sets::get_lower() { return m_imp->get_lower(); } - rational hitting_sets::get_upper() { return m_imp->get_upper(); } - void hitting_sets::set_upper(rational const& r) { return m_imp->set_upper(r); } - bool hitting_sets::get_value(unsigned idx) { return m_imp->get_value(idx); } - void hitting_sets::collect_statistics(::statistics& st) const { m_imp->collect_statistics(st); } - void hitting_sets::reset() { m_imp->reset(); } - - -}; diff --git a/src/opt/hitting_sets.h b/src/opt/hitting_sets.h deleted file mode 100644 index c9708710f..000000000 --- a/src/opt/hitting_sets.h +++ /dev/null @@ -1,52 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - hitting_sets.h - -Abstract: - - Hitting set approximations. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-06-06 - -Notes: - ---*/ -#ifndef HITTING_SETS_H_ -#define HITTING_SETS_H_ - -#include "rational.h" -#include "statistics.h" -#include "lbool.h" -#include "rlimit.h" - -namespace opt { - - class hitting_sets { - struct imp; - imp* m_imp; - public: - hitting_sets(reslimit& lim); - ~hitting_sets(); - void add_weight(rational const& w); - void add_exists_true(unsigned sz, unsigned const* elems); - void add_exists_false(unsigned sz, unsigned const* elems); - lbool compute_lower(); - lbool compute_upper(); - void set_upper(rational const& r); - rational get_lower(); - rational get_upper(); - bool get_value(unsigned idx); - void set_cancel(bool f); - void collect_statistics(::statistics& st) const; - void reset(); - }; - - -}; - -#endif diff --git a/src/opt/maxhs.cpp b/src/opt/maxhs.cpp deleted file mode 100644 index 2297bdc20..000000000 --- a/src/opt/maxhs.cpp +++ /dev/null @@ -1,556 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - maxhs.cpp - -Abstract: - - maxhs based MaxSAT. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-4-17 - -Notes: - ---*/ -#include "optsmt.h" -#include "hitting_sets.h" -#include "stopwatch.h" -#include "ast_pp.h" -#include "model_smt2_pp.h" -#include "uint_set.h" -#include "maxhs.h" -#include "opt_context.h" - -namespace opt { - - class scoped_stopwatch { - double& m_time; - stopwatch m_watch; - public: - scoped_stopwatch(double& time): m_time(time) { - m_watch.start(); - } - ~scoped_stopwatch() { - m_watch.stop(); - m_time += m_watch.get_seconds(); - } - }; - - - // ---------------------------------- - // MaxSatHS+MSS - // variant of MaxSAT-HS (Algorithm 9) - // that also refines upper bound during progressive calls - // to the underlying optimization solver for the soft constraints. - // - - class maxhs : public maxsmt_solver_base { - struct stats { - stats() { reset(); } - void reset() { memset(this, 0, sizeof(*this)); } - unsigned m_num_iterations; - unsigned m_num_core_reductions_success; - unsigned m_num_core_reductions_failure; - unsigned m_num_model_expansions_success; - unsigned m_num_model_expansions_failure; - double m_core_reduction_time; - double m_model_expansion_time; - double m_aux_sat_time; - double m_disjoint_cores_time; - }; - - hitting_sets m_hs; - expr_ref_vector m_aux; // auxiliary (indicator) variables. - obj_map m_aux2index; // expr |-> index - unsigned_vector m_core_activity; // number of times soft constraint is used in a core. - svector m_seed; // clause selected in current model. - svector m_aux_active; // active soft clauses. - ptr_vector m_asms; // assumptions (over aux) - stats m_stats; - bool m_at_lower_bound; - - - public: - maxhs(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): - maxsmt_solver_base(c, ws, soft), - m_hs(m.limit()), - m_aux(m), - m_at_lower_bound(false) { - } - virtual ~maxhs() {} - - virtual void collect_statistics(statistics& st) const { - maxsmt_solver_base::collect_statistics(st); - m_hs.collect_statistics(st); - st.update("maxhs-num-iterations", m_stats.m_num_iterations); - st.update("maxhs-num-core-reductions-n", m_stats.m_num_core_reductions_failure); - st.update("maxhs-num-core-reductions-y", m_stats.m_num_core_reductions_success); - st.update("maxhs-num-model-expansions-n", m_stats.m_num_model_expansions_failure); - st.update("maxhs-num-model-expansions-y", m_stats.m_num_model_expansions_success); - st.update("maxhs-core-reduction-time", m_stats.m_core_reduction_time); - st.update("maxhs-model-expansion-time", m_stats.m_model_expansion_time); - st.update("maxhs-aux-sat-time", m_stats.m_aux_sat_time); - st.update("maxhs-disj-core-time", m_stats.m_disjoint_cores_time); - } - - lbool operator()() { - ptr_vector hs; - init(); - init_local(); - if (!disjoint_cores(hs)) { - return l_undef; - } - seed2assumptions(); - while (m_lower < m_upper) { - ++m_stats.m_num_iterations; - trace_bounds("maxhs"); - TRACE("opt", tout << "(maxhs [" << m_lower << ":" << m_upper << "])\n";); - if (m.canceled()) { - return l_undef; - } - - lbool core_found = generate_cores(hs); - switch(core_found) { - case l_undef: - return l_undef; - case l_true: { - lbool is_sat = next_seed(); - switch(is_sat) { - case l_true: - seed2hs(false, hs); - break; - case l_false: - TRACE("opt", tout << "no more seeds\n";); - IF_VERBOSE(1, verbose_stream() << "(opt.maxhs.no-more-seeds)\n";); - m_lower = m_upper; - return l_true; - case l_undef: - return l_undef; - } - break; - } - case l_false: - IF_VERBOSE(1, verbose_stream() << "(opt.maxhs.no-more-cores)\n";); - TRACE("opt", tout << "no more cores\n";); - m_lower = m_upper; - return l_true; - } - } - return l_true; - } - - private: - - unsigned num_soft() const { return m_soft.size(); } - - void init_local() { - unsigned sz = num_soft(); - app_ref fml(m), obj(m); - expr_ref_vector sum(m); - m_asms.reset(); - m_seed.reset(); - m_aux.reset(); - m_aux_active.reset(); - m_aux2index.reset(); - m_core_activity.reset(); - for (unsigned i = 0; i < sz; ++i) { - bool tt = is_true(m_model, m_soft[i]); - m_seed.push_back(tt); - m_aux. push_back(mk_fresh(m.mk_bool_sort())); - m_aux_active.push_back(false); - m_core_activity.push_back(0); - m_aux2index.insert(m_aux.back(), i); - if (tt) { - m_asms.push_back(m_aux.back()); - ensure_active(i); - } - } - - for (unsigned i = 0; i < m_weights.size(); ++i) { - m_hs.add_weight(m_weights[i]); - } - TRACE("opt", print_seed(tout);); - } - - - void hs2seed(ptr_vector const& hs) { - for (unsigned i = 0; i < num_soft(); ++i) { - m_seed[i] = true; - } - for (unsigned i = 0; i < hs.size(); ++i) { - m_seed[m_aux2index.find(hs[i])] = false; - } - TRACE("opt", - print_asms(tout << "hitting set: ", hs); - print_seed(tout);); - } - - void seed2hs(bool pos, ptr_vector& hs) { - hs.reset(); - for (unsigned i = 0; i < num_soft(); ++i) { - if (pos == m_seed[i]) { - hs.push_back(m_aux[i].get()); - } - } - TRACE("opt", - print_asms(tout << "hitting set: ", hs); - print_seed(tout);); - - } - - void seed2assumptions() { - seed2hs(true, m_asms); - } - - - // - // Find disjoint cores for soft constraints. - // - bool disjoint_cores(ptr_vector& hs) { - scoped_stopwatch _sw(m_stats.m_disjoint_cores_time); - m_asms.reset(); - svector active(num_soft(), true); - rational lower(0); - update_assumptions(active, lower, hs); - SASSERT(lower.is_zero()); - while (true) { - lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); - switch (is_sat) { - case l_true: - if (lower > m_lower) { - m_lower = lower; - } - return true; - case l_false: - if (!shrink()) return false; - block_up(); - update_assumptions(active, lower, hs); - break; - case l_undef: - return false; - } - } - } - - void update_assumptions(svector& active, rational& lower, ptr_vector& hs) { - rational arg_min(0); - expr* e = 0; - for (unsigned i = 0; i < m_asms.size(); ++i) { - unsigned index = m_aux2index.find(m_asms[i]); - active[index] = false; - if (arg_min.is_zero() || arg_min > m_weights[index]) { - arg_min = m_weights[index]; - e = m_asms[i]; - } - } - if (e) { - hs.push_back(e); - lower += arg_min; - } - m_asms.reset(); - for (unsigned i = 0; i < num_soft(); ++i) { - if (active[i]) { - m_asms.push_back(m_aux[i].get()); - ensure_active(i); - } - } - } - - // - // Auxiliary Algorithm 10 for producing cores. - // - lbool generate_cores(ptr_vector& hs) { - bool core = !m_at_lower_bound; - while (true) { - hs2seed(hs); - lbool is_sat = check_subset(); - switch(is_sat) { - case l_undef: - return l_undef; - case l_true: - if (!grow()) return l_undef; - block_down(); - return core?l_true:l_false; - case l_false: - core = true; - if (!shrink()) return l_undef; - block_up(); - find_non_optimal_hitting_set(hs); - break; - } - } - } - - struct lt_activity { - maxhs& hs; - lt_activity(maxhs& hs):hs(hs) {} - bool operator()(expr* a, expr* b) const { - unsigned w1 = hs.m_core_activity[hs.m_aux2index.find(a)]; - unsigned w2 = hs.m_core_activity[hs.m_aux2index.find(b)]; - return w1 < w2; - } - }; - - // - // produce the non-optimal hitting set by using the 10% heuristic. - // of most active cores constraints. - // m_asms contains the current core. - // - void find_non_optimal_hitting_set(ptr_vector& hs) { - std::sort(m_asms.begin(), m_asms.end(), lt_activity(*this)); - for (unsigned i = m_asms.size(); i > 9*m_asms.size()/10;) { - --i; - hs.push_back(m_asms[i]); - } - } - - // - // retrieve the next seed that satisfies state of hs. - // state of hs must be satisfiable before optimization is called. - // - lbool next_seed() { - scoped_stopwatch _sw(m_stats.m_aux_sat_time); - TRACE("opt", tout << "\n";); - - // min c_i*(not x_i) for x_i are soft clauses. - // max c_i*x_i for x_i are soft clauses - - m_at_lower_bound = false; - - lbool is_sat = m_hs.compute_upper(); - - if (is_sat == l_true) { - is_sat = m_hs.compute_lower(); - } - if (is_sat == l_true) { - m_at_lower_bound = m_hs.get_upper() == m_hs.get_lower(); - if (m_hs.get_lower() > m_lower) { - m_lower = m_hs.get_lower(); - } - for (unsigned i = 0; i < num_soft(); ++i) { - m_seed[i] = is_active(i) && !m_hs.get_value(i); - } - TRACE("opt", print_seed(tout);); - } - return is_sat; - } - - // - // check assignment returned by HS with the original - // hard constraints. - // - lbool check_subset() { - TRACE("opt", tout << "\n";); - m_asms.reset(); - for (unsigned i = 0; i < num_soft(); ++i) { - if (m_seed[i]) { - m_asms.push_back(m_aux[i].get()); - ensure_active(i); - } - } - return s().check_sat(m_asms.size(), m_asms.c_ptr()); - } - - // - // extend the current assignment to one that - // satisfies as many soft constraints as possible. - // update the upper bound based on this assignment - // - bool grow() { - scoped_stopwatch _sw(m_stats.m_model_expansion_time); - model_ref mdl; - s().get_model(mdl); - for (unsigned i = 0; i < num_soft(); ++i) { - ensure_active(i); - m_seed[i] = false; - } - for (unsigned i = 0; i < m_asms.size(); ++i) { - m_seed[m_aux2index.find(m_asms[i])] = true; - } - - for (unsigned i = 0; i < num_soft(); ++i) { - if (m_seed[i]) { - // already an assumption - } - else if (is_true(mdl, m_soft[i])) { - m_seed[i] = true; - m_asms.push_back(m_aux[i].get()); - } - else { - m_asms.push_back(m_aux[i].get()); - lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); - switch(is_sat) { - case l_undef: - return false; - case l_false: - ++m_stats.m_num_model_expansions_failure; - m_asms.pop_back(); - break; - case l_true: - ++m_stats.m_num_model_expansions_success; - s().get_model(mdl); - m_seed[i] = true; - break; - } - } - } - rational upper(0); - for (unsigned i = 0; i < num_soft(); ++i) { - if (!m_seed[i]) { - upper += m_weights[i]; - } - } - if (upper < m_upper) { - m_upper = upper; - m_hs.set_upper(upper); - m_model = mdl; - m_assignment.reset(); - m_assignment.append(m_seed); - TRACE("opt", - tout << "new upper: " << m_upper << "\n"; - model_smt2_pp(tout, m, *(mdl.get()), 0);); - } - DEBUG_CODE( - for (unsigned i = 0; i < num_soft(); ++i) { - SASSERT(is_true(mdl, m_soft[i]) == m_seed[i]); - }); - - return true; - } - - // - // remove soft constraints from the current core. - // - bool shrink() { - scoped_stopwatch _sw(m_stats.m_core_reduction_time); - m_asms.reset(); - s().get_unsat_core(m_asms); - TRACE("opt", print_asms(tout, m_asms);); - obj_map asm2index; - for (unsigned i = 0; i < m_asms.size(); ++i) { - asm2index.insert(m_asms[i], i); - } - obj_map::iterator it = asm2index.begin(), end = asm2index.end(); - for (; it != end; ++it) { - unsigned i = it->m_value; - if (i < m_asms.size()) { - expr* tmp = m_asms[i]; - expr* back = m_asms.back(); - m_asms[i] = back; - m_asms.pop_back(); - lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); - TRACE("opt", tout << "checking: " << mk_pp(tmp, m) << ": " << is_sat << "\n";); - switch(is_sat) { - case l_true: - ++m_stats.m_num_core_reductions_failure; - // put back literal into core - m_asms.push_back(back); - m_asms[i] = tmp; - break; - case l_false: - // update the core - m_asms.reset(); - ++m_stats.m_num_core_reductions_success; - s().get_unsat_core(m_asms); - TRACE("opt", print_asms(tout, m_asms);); - update_index(asm2index); - break; - case l_undef: - return false; - } - } - } - return true; - } - - void print_asms(std::ostream& out, ptr_vector const& asms) { - for (unsigned j = 0; j < asms.size(); ++j) { - out << mk_pp(asms[j], m) << " "; - } - out << "\n"; - } - - void print_seed(std::ostream& out) { - out << "seed: "; - for (unsigned i = 0; i < num_soft(); ++i) { - out << (m_seed[i]?"1":"0"); - } - out << "\n"; - } - - // - // must include some literal not from asms. - // (furthermore, update upper bound constraint in HS) - // - void block_down() { - uint_set indices; - unsigned_vector c_indices; - for (unsigned i = 0; i < m_asms.size(); ++i) { - indices.insert(m_aux2index.find(m_asms[i])); - } - for (unsigned i = 0; i < num_soft(); ++i) { - if (!indices.contains(i)) { - c_indices.push_back(i); - } - } - m_hs.add_exists_false(c_indices.size(), c_indices.c_ptr()); - } - - // should exclude some literal from core. - void block_up() { - unsigned_vector indices; - for (unsigned i = 0; i < m_asms.size(); ++i) { - unsigned index = m_aux2index.find(m_asms[i]); - m_core_activity[index]++; - indices.push_back(index); - } - m_hs.add_exists_true(indices.size(), indices.c_ptr()); - } - - void update_index(obj_map& asm2index) { - obj_map::iterator it = asm2index.begin(), end = asm2index.end(); - for (; it != end; ++it) { - it->m_value = UINT_MAX; - } - for (unsigned i = 0; i < m_asms.size(); ++i) { - asm2index.find(m_asms[i]) = i; - } - } - - app_ref mk_fresh(sort* s) { - app_ref r(m); - r = m.mk_fresh_const("r", s); - m_c.fm().insert(r->get_decl()); - return r; - } - - bool is_true(model_ref& mdl, expr* e) { - expr_ref val(m); - return mdl->eval(e, val) && m.is_true(val); - } - - bool is_active(unsigned i) const { - return m_aux_active[i]; - } - - void ensure_active(unsigned i) { - if (!is_active(i)) { - expr_ref fml(m); - fml = m.mk_implies(m_aux[i].get(), m_soft[i]); - s().assert_expr(fml); - m_aux_active[i] = true; - } - } - - }; - - maxsmt_solver_base* mk_maxhs( - maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) { - return alloc(maxhs, c, ws, soft); - } - -} diff --git a/src/opt/maxhs.h b/src/opt/maxhs.h deleted file mode 100644 index 903354c0e..000000000 --- a/src/opt/maxhs.h +++ /dev/null @@ -1,29 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - maxhs.h - -Abstract: - - HS-max based MaxSAT. - -Author: - - Nikolaj Bjorner (nbjorner) 2014-4-17 - -Notes: - ---*/ - -#ifndef HS_MAX_H_ -#define HS_MAX_H_ - -#include "maxsmt.h" - -namespace opt { - maxsmt_solver_base* mk_maxhs(maxsat_context& c, - weights_t& ws, expr_ref_vector const& soft); -} -#endif diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 5229fafab..992e13fe4 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -19,10 +19,7 @@ Notes: #include #include "maxsmt.h" -#include "fu_malik.h" #include "maxres.h" -#include "maxhs.h" -#include "bcd2.h" #include "wmax.h" #include "maxsls.h" #include "ast_pp.h" @@ -166,19 +163,10 @@ namespace opt { else if (maxsat_engine == symbol("pd-maxres")) { m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints); } - else if (maxsat_engine == symbol("bcd2")) { - m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints); - } - else if (maxsat_engine == symbol("maxhs")) { - m_msolver = mk_maxhs(m_c, m_weights, m_soft_constraints); - } else if (maxsat_engine == symbol("sls")) { // NB: this is experimental one-round version of SLS m_msolver = mk_sls(m_c, m_weights, m_soft_constraints); } - else if (is_maxsat_problem(m_weights) && maxsat_engine == symbol("fu_malik")) { - m_msolver = mk_fu_malik(m_c, m_weights, m_soft_constraints); - } else { if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) { warning_msg("solver %s is not recognized, using default 'wmax'", diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 629b3aa53..eb8d61423 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -2,7 +2,7 @@ def_module_params('opt', description='optimization parameters', export=True, params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), - ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'pd-maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"), + ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres', 'sls'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), ('print_model', BOOL, False, 'display model for satisfiable constraints'),