mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

add cube mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-24 10:53:57 -07:00
commit ae9a6664d4
144 changed files with 6012 additions and 3174 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/CMakeLists.txt
View file

@ -3,7 +3,6 @@ z3_add_component(sat
ba_solver.cpp
dimacs.cpp
sat_asymm_branch.cpp
sat_ccc.cpp
sat_clause.cpp
sat_clause_set.cpp
sat_clause_use_list.cpp

604
src/sat/sat_ccc.cpp
View file

@ -1,604 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
sat_ccc.cpp
Abstract:
A variant of Concurrent Cube and Conquer
Author:
Nikolaj Bjorner (nbjorner) 2017-4-17
Notes:
The cube process spawns conquer threads to search parts of the
state space.
The conquer threads have two modes:
- emulation mode - where they try to outpace the cuber on the same search tree
- complement mode - where they solve a sub-branch not yet explored by the cuber.
When the conquer thread returns a solved cube it is processed in the following ways:
- ignore if solved_id \not\in decisions
- mark d as closed if d \in decisions, such that d is marked by solved id
- backjump otherwise, conquer thread has solved a branch attempted by the cuber
--*/
#include "sat_solver.h"
#include "sat_lookahead.h"
#include "sat_ccc.h"
using namespace sat;
// ------------
// cuber
ccc::cuber::cuber(ccc& c): m_ccc(c), m_lh(alloc(lookahead, c.m_s)), m_branch_id(0) {}
lbool ccc::cuber::search() {
while (true) {
m_branch_id = 0;
m_last_closure_level = 1000;
m_lh->init_search();
m_lh->m_model.reset();
lookahead::scoped_level _sl(*m_lh.get(), m_lh->c_fixed_truth);
m_lh->m_search_mode = lookahead_mode::searching;
lbool r = research();
if (r == l_true) {
m_ccc.m_model = m_lh->get_model();
}
if (false && r == l_undef) {
continue;
}
m_lh->collect_statistics(m_ccc.m_lh_stats);
return r;
}
}
lbool ccc::cuber::research() {
m_ccc.m_s.checkpoint();
if (m_lh->inconsistent()) {
return l_false;
}
if (pop_lookahead()) {
return l_undef;
}
if (get_solved()) {
return l_false;
}
m_lh->inc_istamp();
literal l = m_lh->choose();
if (m_lh->inconsistent()) {
return l_false;
}
if (l == null_literal) {
return l_true;
}
if (!m_decisions.empty()) {
m_ccc.put_decision(m_decisions.back());
}
// update trail and m_decisions
++m_lh->m_stats.m_decisions;
unsigned parent_id = m_decisions.empty() ? 0 : m_decisions.back().m_id;
unsigned spawn_id = spawn_conquer();
unsigned branch1 = m_branch_id++;
unsigned branch2 = m_branch_id++;
decision d(branch1, m_decisions.size() + 1, l, parent_id, spawn_id);
m_decisions.push_back(d);
IF_VERBOSE(2, d.pp(verbose_stream() << "select " << m_last_closure_level << " ") << "\n";);
IF_VERBOSE(2, verbose_stream() << "select " << pp_prefix(m_lh->m_prefix, m_lh->m_trail_lim.size()) << ": " << l << " " << m_lh->m_trail.size() << "\n";);
IF_VERBOSE(3, pp(verbose_stream(), m_decisions) << "\n"; );
TRACE("sat", tout << "choose: " << l << "\n";);
m_lh->push(l, m_lh->c_fixed_truth);
lbool r = research();
if (r == l_false) {
m_lh->pop();
if (m_decisions.back().is_closed()) {
// branch was solved by a spawned conquer process
IF_VERBOSE(1, m_decisions.back().pp(verbose_stream() << "closed ") << "\n";);
r = l_false;
m_decisions.pop_back();
}
else {
if (spawn_id > 0) {
free_conquer(spawn_id);
m_last_closure_level *= 3;
m_last_closure_level /= 4;
}
m_lh->inc_istamp();
m_lh->flip_prefix();
m_lh->push(~l, m_lh->c_fixed_truth);
m_decisions.back().negate();
m_decisions.back().m_id = branch2;
m_decisions.back().m_spawn_id = 0;
r = research();
if (r == l_false) {
m_lh->pop();
m_decisions.pop_back();
}
}
}
return r;
}
bool ccc::cuber::pop_lookahead() {
return false;
scoped_ptr<lookahead> new_lh;
bool result = false;
#pragma omp critical (ccc_new_lh)
{
if (m_ccc.m_new_lh) {
new_lh = m_ccc.m_new_lh.detach();
result = true;
}
}
if (new_lh) {
m_lh->collect_statistics(m_ccc.m_lh_stats);
m_lh = new_lh.detach();
}
return result;
}
void ccc::cuber::update_closure_level(decision const& d, int offset) {
m_last_closure_level = (d.m_depth + 3*m_last_closure_level) / 4;
if (m_last_closure_level >= static_cast<unsigned>(abs(offset))) {
m_last_closure_level += offset;
}
}
unsigned ccc::cuber::spawn_conquer() {
unsigned result = 0;
//
// decisions must have been solved at a higher level by a conquer thread
//
if (!m_free_threads.empty()) {
if (m_last_closure_level <= m_decisions.size()) {
result = m_free_threads.back();
++m_ccc.m_ccc_stats.m_spawn_opened;
m_free_threads.pop_back();
}
else {
IF_VERBOSE(1, verbose_stream() << m_last_closure_level << " " << m_decisions.size() << "\n";);
}
}
return result;
}
void ccc::cuber::free_conquer(unsigned id) {
if (id != 0) {
m_free_threads.push_back(id);
}
}
bool ccc::cuber::get_solved() {
// check if CDCL solver got ahead.
bool do_pop = false;
solution sol;
while (true) {
bool is_empty = true;
#pragma omp critical (ccc_solved)
{
if (do_pop) m_ccc.m_solved.pop_front();
if (!m_ccc.m_solved.empty()) {
sol = m_ccc.m_solved.top();
is_empty = false;
}
}
if (is_empty) {
return false;
}
do_pop = true;
unsigned branch_id = sol.m_branch_id;
unsigned thread_id = sol.m_thread_id;
bool found = false;
for (unsigned i = m_decisions.size(); i > 0; ) {
--i;
decision& d = m_decisions[i];
if (branch_id == d.m_id) {
if (d.m_spawn_id == thread_id && thread_id != 0) {
SASSERT(d.m_spawn_id > 0);
IF_VERBOSE(2, d.pp(verbose_stream() << thread_id << ": spawn close ") << "\n";);
++m_ccc.m_ccc_stats.m_spawn_closed;
d.close();
free_conquer(thread_id);
update_closure_level(d, -1);
break;
}
else {
IF_VERBOSE(2, d.pp(verbose_stream() << thread_id << ": conquer ") << "\n";);
++m_ccc.m_ccc_stats.m_cdcl_closed;
update_closure_level(d, 1);
return true;
}
}
// branch is even, d has moved to the next branch
if (branch_id == (d.m_id & ~0x1) && d.m_spawn_id == thread_id && thread_id != 0) {
IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": spawn conquer ") << "\n";);
++m_ccc.m_ccc_stats.m_cdcl_closed;
update_closure_level(d, 1);
return true;
}
}
}
}
// ---------------------
// conquer state machine
lbool ccc::conquer::search() {
try {
if (s.inconsistent()) return l_false;
s.init_search();
s.propagate(false);
if (s.inconsistent()) return l_false;
s.cleanup();
s.simplify_problem();
if (s.inconsistent()) return l_false;
while (true) {
SASSERT(!s.inconsistent());
lbool r = bounded_search();
if (r != l_undef)
return r;
s.restart();
s.simplify_problem();
if (s.check_inconsistent()) return l_false;
s.gc();
push_lookahead();
}
}
catch (solver::abort_solver) {
return l_undef;
}
}
void ccc::conquer::replay_decisions() {
s.propagate(true);
for (unsigned i = s.scope_lvl(); !s.inconsistent() && i < m_decisions.size(); ++i) {
decision const& d = m_decisions[i];
IF_VERBOSE(2, verbose_stream() << thread_id << ": replay " << d.get_literal(thread_id) << " " << s.value(d.get_literal(thread_id)) << "\n";);
if (!push_decision(d)) {
// negation of decision is implied.
IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": backjump to level " << i << " ") << "\n";);
while (m_decisions.size() > i) {
pop_decision(m_decisions.back());
m_decisions.pop_back();
}
break;
}
if (d.m_spawn_id == thread_id && d.is_left()) {
// we pushed the right branch on this thread.
IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": skip left branch on level " << i + 1 << " ") << "\n";);
break;
}
}
}
void ccc::conquer::pop_decision(decision const& d) {
unsigned tid = 0;
if (d.is_spawned(thread_id)) {
tid = thread_id;
m_spawned = false;
IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << ": retire spawn ") << "\n";);
}
#pragma omp critical (ccc_solved)
{
m_ccc.m_solved.push(solution(tid, d.m_id));
}
}
void ccc::conquer::push_lookahead() {
return;
#pragma omp critical (ccc_new_lh)
{
if (!m_ccc.m_new_lh && m_ccc.m_num_clauses > s.num_clauses()) {
std::cout << "push " << s.num_clauses() << "\n";
m_ccc.m_new_lh = alloc(lookahead, s);
m_ccc.m_num_clauses = s.num_clauses();
}
}
}
bool ccc::conquer::push_decision(decision const& d) {
literal lit = d.get_literal(thread_id);
switch (s.value(lit)) {
case l_false:
//TBD:
s.m_restart_threshold = s.m_config.m_restart_initial;
//s.m_conflicts_since_last_restart = 0;
return false;
case l_true:
s.push();
break;
case l_undef:
s.push();
s.assign(lit, justification());
s.propagate(true);
break;
}
m_spawned |= d.is_spawned(thread_id);
return true;
}
bool ccc::conquer::cube_decision() {
decision d;
bool use_cube_decision = false;
SASSERT(s.m_qhead == s.m_trail.size());
while (true) {
if (!m_ccc.get_decision(thread_id, d)) {
return false;
}
if (d.is_spawned(thread_id)) IF_VERBOSE(1, d.pp(verbose_stream() << thread_id << " ") << "\n";);
if (!m_decisions.empty() && m_decisions.back().m_depth + 1 < d.m_depth) {
if (d.is_spawned(thread_id)) {
pop_decision(d);
}
}
else {
break;
}
}
SASSERT(m_decisions.empty() || m_decisions.back().m_depth + 1 >= d.m_depth);
if (!m_decisions.empty() && m_decisions.back().is_spawned(thread_id) && m_decisions.back().m_depth == d.m_depth) {
SASSERT(d.m_spawn_id == 0);
SASSERT(m_decisions.back().is_left());
SASSERT(!d.is_left());
IF_VERBOSE(1, verbose_stream() << thread_id << " inherit spawn\n";);
m_decisions.back().m_spawn_id = 0;
m_spawned = false;
}
SASSERT(m_decisions.empty() || m_decisions.back().m_depth + 1 >= d.m_depth);
while (!m_decisions.empty() && m_decisions.back().m_depth >= d.m_depth) {
// check_non_model("cube decision", m_decisions);
if (m_decisions.back().is_spawned(thread_id)) {
pop_decision(m_decisions.back());
}
m_decisions.pop_back();
}
SASSERT(m_decisions.empty() || m_decisions.back().m_depth + 1 == d.m_depth);
SASSERT(m_decisions.empty() || m_decisions.back().m_id == d.m_parent);
if (m_spawned) {
m_decisions.push_back(d);
return true;
}
s.pop_reinit(s.scope_lvl() - m_decisions.size());
SASSERT(s.m_qhead == s.m_trail.size());
SASSERT(s.scope_lvl() == m_decisions.size());
literal lit = d.get_literal(thread_id);
IF_VERBOSE(2, d.pp(verbose_stream() << thread_id << ": cube ") << "\n";);
IF_VERBOSE(3, pp(verbose_stream() << thread_id << ": push ", m_decisions) << " @ " << s.scope_lvl() << " " << s.value(lit) << "\n";
if (s.value(lit) == l_false) verbose_stream() << "level: " << s.lvl(lit) << "\n";);
if (push_decision(d)) {
m_decisions.push_back(d);
}
else {
pop_decision(d);
}
return true;
}
lbool ccc::conquer::bounded_search() {
while (true) {
s.checkpoint();
bool done = false;
while (!done) {
replay_decisions();
lbool is_sat = s.propagate_and_backjump_step(done);
if (is_sat != l_true) return is_sat;
}
s.gc();
if (!cube_decision() && !s.decide()) {
lbool is_sat = s.final_check();
if (is_sat != l_undef) {
return is_sat;
}
}
}
}
// --------------
// shared state
std::ostream& ccc::decision::pp(std::ostream& out) const {
out << "("
<< "id:" << m_id
<< " l:" << m_literal
<< " d:" << m_depth;
if (m_spawn_id != 0) {
out << " s:" << m_spawn_id;
}
out << ") ";
return out;
}
std::ostream& ccc::pp(std::ostream& out, svector<decision> const& v) {
for (unsigned i = 0; i < v.size(); ++i) {
v[i].pp(out);
}
return out;
}
bool ccc::get_decision(unsigned thread_id, decision& d) {
SASSERT(0 < thread_id && thread_id <= m_decisions.size());
bool result = false;
#pragma omp critical (ccc_decisions)
{
if (!m_decisions[thread_id - 1].empty()) {
d = m_decisions[thread_id - 1].pop_front();
result = true;
}
}
return result;
}
void ccc::put_decision(decision const& d) {
for (unsigned i = 0; i < m_num_conquer; ++i) {
#pragma omp critical (ccc_decisions)
{
while (false && !m_decisions[i].empty()) { // introduces contention.
decision d = m_decisions[i].back();
if (d.m_depth < d.m_depth || d.m_spawn_id != 0) {
break;
}
m_decisions[i].pop_back();
}
m_decisions[i].push(d);
}
}
}
lbool ccc::search() {
enum par_exception_kind {
DEFAULT_EX,
ERROR_EX
};
// set_model();
m_cancel = false;
scoped_limits scoped_rlimit(m_s.rlimit());
ptr_vector<conquer> solvers;
int finished_id = -1;
std::string ex_msg;
par_exception_kind ex_kind;
unsigned error_code = 0;
lbool result = l_undef;
m_decisions.reset();
cuber cuber(*this);
m_num_conquer = m_s.m_config.m_num_threads;
int num_threads = 1 + m_num_conquer; // for ccc-infinity only two threads.
for (int i = 1; i < num_threads; ++i) {
m_s.m_params.set_uint("random_seed", m_s.m_rand());
conquer* s1 = alloc(conquer, *this, m_s.m_params, i);
solvers.push_back(s1);
s1->s.copy(m_s);
scoped_rlimit.push_child(&(s1->m_limit));
m_decisions.push_back(queue<decision>());
}
for (unsigned i = 1; i < m_num_conquer; ++i) {
cuber.m_free_threads.push_back(i);
}
#pragma omp parallel for
for (int i = 0; i < num_threads; ++i) {
try {
lbool r = l_undef;
if (i == 0) {
r = cuber.search();
}
else {
r = solvers[i-1]->search();
}
bool first = false;
#pragma omp critical (par_solver)
{
if (finished_id == -1) {
finished_id = i;
first = true;
result = r;
}
}
if (first) {
for (unsigned j = 0; j < solvers.size(); ++j) {
solvers[j]->m_limit.cancel();
}
// cancel lookahead solver:
m_cancel = true;
}
}
catch (z3_error & err) {
error_code = err.error_code();
ex_kind = ERROR_EX;
}
catch (z3_exception & ex) {
ex_msg = ex.msg();
ex_kind = DEFAULT_EX;
}
}
if (finished_id > 0 && result == l_true) {
// set model from auxiliary solver
m_model = solvers[finished_id - 1]->s.get_model();
}
for (unsigned i = 0; i < solvers.size(); ++i) {
solvers[i]->s.collect_statistics(m_lh_stats);
dealloc(solvers[i]);
}
if (finished_id == -1) {
switch (ex_kind) {
case ERROR_EX: throw z3_error(error_code);
default: throw default_exception(ex_msg.c_str());
}
}
#if 0
if (result == l_true) {
for (unsigned i = 1; i < m_model.size(); ++i) {
std::cout << "push_model(" << i << ", " << (m_model[i] > 0 ? "false" : "true") << ");\n";
}
}
#endif
return result;
}
#if 0
void ccc::push_model(unsigned v, bool sign) {
if (m_values.size() <= v) {
m_values.resize(v + 1);
}
m_values[v] = sign;
}
void ccc::check_non_model(char const* fn, svector<decision> const& decisions) {
for (unsigned i = 0; i < decisions.size(); ++i) {
decision d = decisions[i];
literal lit = d.m_literal;
if (m_values[lit.var()] != lit.sign()) return;
}
IF_VERBOSE(1, pp(verbose_stream() << "backtracking from model " << fn << " ", decisions) << "\n";);
}
#endif

150
src/sat/sat_ccc.h
View file

@ -1,150 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
sat_ccc.h
Abstract:
A variant of Concurrent Cube and Conquer
Author:
Nikolaj Bjorner (nbjorner) 2017-4-17
Notes:
--*/
#ifndef _SAT_CCC_H_
#define _SAT_CCC_H_
#include "util/queue.h"
namespace sat {
class ccc {
struct decision {
unsigned m_id; // unique identifier for decision
unsigned m_depth; // depth of decision
literal m_literal; // decision literal
unsigned m_parent; // id of parent
int m_spawn_id; // thread id of conquer thread processing complented branch.
// = 0 if not spawned.
// > 0 if active spawn is in progress
// < 0 if thread has closed the branch
decision(unsigned id, unsigned d, literal last, unsigned parent_id, unsigned spawn):
m_id(id), m_depth(d), m_literal(last), m_parent(parent_id), m_spawn_id(spawn) {}
decision():
m_id(0), m_depth(0), m_literal(null_literal), m_parent(0), m_spawn_id(0) {}
void close() { SASSERT(m_spawn_id > 0); m_spawn_id = -m_spawn_id; }
bool is_closed() const { return m_spawn_id < 0; }
void negate() { m_literal.neg(); }
bool is_left() const { return 0 == (m_id & 0x1); }
bool is_spawned(unsigned thread_id) const { return m_spawn_id == thread_id; }
// the left branch has an even branch_id.
// the branch is spawned if it is even and the spawn_id is the same as the thread_id, and furthermore it is exploring the left branch.
// it may explore the right branch, but is then not in a spawned mode.
// we retain the spawn id so that the spawned thread can be re-spun.
literal get_literal(unsigned thread_id) const { return ((m_id & 0x1) == 0 && thread_id == m_spawn_id) ? ~m_literal : m_literal; }
std::ostream& pp(std::ostream& out) const;
};
struct solution {
unsigned m_thread_id;
unsigned m_branch_id;
solution(unsigned t, unsigned s): m_thread_id(t), m_branch_id(s) {}
solution(): m_thread_id(0), m_branch_id(0) {}
};
struct stats {
unsigned m_spawn_closed;
unsigned m_spawn_opened;
unsigned m_cdcl_closed;
stats() { reset(); }
void reset() {
memset(this, 0, sizeof(*this));
}
};
struct conquer {
reslimit m_limit;
ccc& m_ccc;
solver s;
svector<decision> m_decisions;
unsigned thread_id;
bool m_spawned;
conquer(ccc& super, params_ref const& p, unsigned tid): m_ccc(super), s(p, m_limit), thread_id(tid), m_spawned(false) {}
lbool search();
bool cube_decision();
lbool bounded_search();
bool push_decision(decision const& d);
void pop_decision(decision const& d);
void push_lookahead();
void replay_decisions();
};
struct cuber {
ccc& m_ccc;
scoped_ptr<lookahead> m_lh;
unsigned m_branch_id;
unsigned m_last_closure_level;
unsigned_vector m_free_threads;
svector<decision> m_decisions;
cuber(ccc& c);
lbool search();
lbool research();
bool get_solved();
void update_closure_level(decision const& d, int offset);
unsigned spawn_conquer();
void free_conquer(unsigned thread_id);
bool pop_lookahead();
};
solver& m_s;
queue<solution> m_solved;
vector<queue<decision> > m_decisions;
scoped_ptr<lookahead> m_new_lh;
unsigned m_num_clauses;
unsigned m_num_conquer;
model m_model;
volatile bool m_cancel;
::statistics m_lh_stats;
stats m_ccc_stats;
void put_decision(decision const& d);
bool get_decision(unsigned thread_id, decision& d);
static std::ostream& pp(std::ostream& out, svector<decision> const& v);
void push_model(unsigned v, bool sign);
void set_model();
bool trail_in_model(literal_vector const& trail) const;
void check_non_model(char const* fn, svector<decision> const& decisions);
public:
ccc(solver& s): m_s(s), m_num_clauses(s.num_clauses()) {}
lbool search();
model const& get_model() const { return m_model; }
void collect_statistics(::statistics& st) {
st.copy(m_lh_stats);
st.update("ccc-spawn-closed", m_ccc_stats.m_spawn_closed);
st.update("ccc-cdcl-closed", m_ccc_stats.m_cdcl_closed);
st.update("ccc-spawn-opened", m_ccc_stats.m_spawn_opened);
}
};
}
#endif

6
src/sat/sat_config.cpp
View file

@ -39,7 +39,6 @@ namespace sat {
m_local_search = 0;
m_lookahead_search = false;
m_lookahead_simplify = false;
m_ccc = false;
updt_params(p);
}
@ -86,9 +85,11 @@ namespace sat {
m_local_search = p.local_search();
m_local_search_threads = p.local_search_threads();
m_lookahead_simplify = p.lookahead_simplify();
m_lookahead_cube = p.lookahead_cube();
m_lookahead_search = p.lookahead_search();
m_lookahead_reward = p.lookahead_reward();
m_ccc = p.ccc();
m_lookahead_cube_fraction = p.lookahead_cube_fraction();
m_lookahead_cube_cutoff = p.lookahead_cube_cutoff();
// These parameters are not exposed
m_simplify_mult1 = _p.get_uint("simplify_mult1", 300);
@ -166,6 +167,7 @@ namespace sat {
else {
throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting");
}
m_dimacs_display = p.dimacs_display();
}
void config::collect_param_descrs(param_descrs & r) {

6
src/sat/sat_config.h
View file

@ -75,8 +75,10 @@ namespace sat {
bool m_local_search;
bool m_lookahead_search;
bool m_lookahead_simplify;
bool m_lookahead_cube;
unsigned m_lookahead_cube_cutoff;
double m_lookahead_cube_fraction;
symbol m_lookahead_reward;
bool m_ccc;
unsigned m_simplify_mult1;
double m_simplify_mult2;
@ -96,6 +98,8 @@ namespace sat {
symbol m_drat_file;
bool m_drat_check;
bool m_dimacs_display;
symbol m_always_true;
symbol m_always_false;
symbol m_caching;

57
src/sat/sat_lookahead.cpp
View file

@ -1710,6 +1710,47 @@ namespace sat {
return true;
}
void lookahead::cube() {
m_model.reset();
scoped_level _sl(*this, c_fixed_truth);
literal_vector trail;
m_search_mode = lookahead_mode::searching;
double freevars_threshold = 0;
while (true) {
TRACE("sat", display(tout););
inc_istamp();
checkpoint();
literal l = choose();
if (inconsistent()) {
freevars_threshold = m_freevars.size();
if (!backtrack(trail)) return;
continue;
}
unsigned depth = m_trail_lim.size();
if (l == null_literal ||
(m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
(m_config.m_cube_cutoff == 0 && m_freevars.size() < freevars_threshold)) {
display_cube(std::cout);
set_conflict();
if (!backtrack(trail)) return;
freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
continue;
}
TRACE("sat", tout << "choose: " << l << " " << trail << "\n";);
++m_stats.m_decisions;
IF_VERBOSE(1, printf("\r");
std::stringstream strm;
strm << pp_prefix(m_prefix, m_trail_lim.size());
for (unsigned i = 0; i < 50; ++i) strm << " ";
printf(strm.str().c_str());
fflush(stdout);
);
push(l, c_fixed_truth);
trail.push_back(l);
SASSERT(inconsistent() || !is_unsat());
}
}
lbool lookahead::search() {
m_model.reset();
scoped_level _sl(*this, c_fixed_truth);
@ -1719,10 +1760,6 @@ namespace sat {
TRACE("sat", display(tout););
inc_istamp();
checkpoint();
if (inconsistent()) {
if (!backtrack(trail)) return l_false;
continue;
}
literal l = choose();
if (inconsistent()) {
if (!backtrack(trail)) return l_false;
@ -1764,6 +1801,14 @@ namespace sat {
}
}
std::ostream& lookahead::display_cube(std::ostream& out) const {
out << "c";
for (literal l : m_assumptions) {
out << " " << ~l;
}
return out << "\n";
}
std::ostream& lookahead::display_binary(std::ostream& out) const {
for (unsigned i = 0; i < m_binary.size(); ++i) {
literal_vector const& lits = m_binary[i];
@ -1818,7 +1863,7 @@ namespace sat {
literal lookahead::choose() {
literal l = null_literal;
while (l == null_literal) {
while (l == null_literal && !inconsistent()) {
pre_select();
if (m_lookahead.empty()) {
break;
@ -2013,6 +2058,8 @@ namespace sat {
else {
warning_msg("Reward type not recognized");
}
m_config.m_cube_cutoff = m_s.m_config.m_lookahead_cube_cutoff;
m_config.m_cube_fraction = m_s.m_config.m_lookahead_cube_fraction;
}
void lookahead::collect_statistics(statistics& st) const {

14
src/sat/sat_lookahead.h
View file

@ -84,6 +84,8 @@ namespace sat {
unsigned m_dl_max_iterations;
unsigned m_tc1_limit;
reward_t m_reward_type;
unsigned m_cube_cutoff;
double m_cube_fraction;
config() {
m_max_hlevel = 50;
@ -95,6 +97,8 @@ namespace sat {
m_dl_max_iterations = 32;
m_tc1_limit = 10000000;
m_reward_type = ternary_reward;
m_cube_cutoff = 0;
m_cube_fraction = 0.4;
}
};
@ -446,6 +450,8 @@ namespace sat {
std::ostream& display_clauses(std::ostream& out) const;
std::ostream& display_values(std::ostream& out) const;
std::ostream& display_lookahead(std::ostream& out) const;
std::ostream& display_cube(std::ostream& out) const;
void init_search();
void checkpoint();
@ -474,6 +480,14 @@ namespace sat {
return search();
}
/**
\brief create cubes to std-out in DIMACS form.
The cubes are controlled using cut-depth and cut-fraction parameters.
If cut-depth != 0, then it is used to control the depth of cuts.
Otherwise, cut-fraction gives an adaptive threshold for creating cuts.
*/
void cube();
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
/**
\brief simplify set of clauses by extracting units from a lookahead at base level.

7
src/sat/sat_params.pyg
View file

@ -34,8 +34,11 @@ def_module_params('sat',
('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', BOOL, False, 'use local search instead of CDCL'),
('lookahead_cube', BOOL, False, 'use lookahead solver to create cubes'),
('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. 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_simplify', BOOL, False, 'use lookahead solver during simplification'),
('lookahead.reward', SYMBOL, 'heuleu', 'select lookahead heuristic: ternary, hs (Heule Schur), heuleu (Heule Unit), or unit'),
('ccc', BOOL, False, 'use Concurrent Cube and Conquer solver')
))
('dimacs.display', BOOL, False, 'display SAT instance in DIMACS format and return unknown instead of solving')))

44
src/sat/sat_solver.cpp
View file

@ -20,7 +20,6 @@ Revision History:
#include "sat/sat_solver.h"
#include "sat/sat_integrity_checker.h"
#include "sat/sat_lookahead.h"
#include "sat/sat_ccc.h"
#include "util/luby.h"
#include "util/trace.h"
#include "util/max_cliques.h"
@ -847,16 +846,25 @@ namespace sat {
pop_to_base_level();
IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";);
SASSERT(at_base_lvl());
if (m_config.m_dimacs_display) {
display_dimacs(std::cout);
for (unsigned i = 0; i < num_lits; ++lits) {
std::cout << dimacs_lit(lits[i]) << " 0\n";
}
return l_undef;
}
if (m_config.m_lookahead_search && num_lits == 0) {
return lookahead_search();
}
if (m_config.m_lookahead_cube && num_lits == 0) {
lookahead_cube();
return l_undef;
}
if (m_config.m_local_search) {
return do_local_search(num_lits, lits);
}
if (m_config.m_ccc && num_lits == 0) {
return do_ccc();
}
if ((m_config.m_num_threads > 1 || m_config.m_local_search_threads > 0) && !m_par) {
SASSERT(scope_lvl() == 0);
return check_par(num_lits, lits);
}
flet<bool> _searching(m_searching, true);
@ -913,13 +921,6 @@ namespace sat {
if (check_inconsistent()) return l_false;
gc();
#if 0
if (m_clauses.size() < 65000) {
return do_ccc();
return lookahead_search();
}
#endif
if (m_config.m_restart_max <= m_restarts) {
m_reason_unknown = "sat.max.restarts";
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";);
@ -951,12 +952,16 @@ namespace sat {
return r;
}
lbool solver::do_ccc() {
ccc c(*this);
lbool r = c.search();
m_model = c.get_model();
c.collect_statistics(m_aux_stats);
return r;
void solver::lookahead_cube() {
lookahead lh(*this);
try {
lh.cube();
}
catch (z3_exception&) {
lh.collect_statistics(m_aux_stats);
throw;
}
lh.collect_statistics(m_aux_stats);
}
lbool solver::lookahead_search() {
@ -1497,10 +1502,7 @@ namespace sat {
}
void solver::sort_watch_lits() {
vector<watch_list>::iterator it = m_watches.begin();
vector<watch_list>::iterator end = m_watches.end();
for (; it != end; ++it) {
watch_list & wlist = *it;
for (watch_list & wlist : m_watches) {
std::stable_sort(wlist.begin(), wlist.end(), watched_lt());
}
}

1
src/sat/sat_solver.h
View file

@ -403,6 +403,7 @@ namespace sat {
void exchange_par();
lbool check_par(unsigned num_lits, literal const* lits);
lbool lookahead_search();
void lookahead_cube();
lbool do_local_search(unsigned num_lits, literal const* lits);
lbool do_ccc();

14
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -149,7 +149,6 @@ public:
virtual void set_progress_callback(progress_callback * callback) {}
void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) {
if (weights != 0) {
for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]);
@ -212,6 +211,11 @@ public:
init_reason_unknown();
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
if (r == l_undef && m_solver.get_config().m_dimacs_display) {
for (auto const& kv : m_map) {
std::cout << "c " << kv.m_value << " " << mk_pp(kv.m_key, m) << "\n";
}
}
switch (r) {
case l_true:
@ -806,14 +810,12 @@ private:
}
sat::model const & ll_m = m_solver.get_model();
model_ref md = alloc(model, m);
atom2bool_var::iterator it = m_map.begin();
atom2bool_var::iterator end = m_map.end();
for (; it != end; ++it) {
expr * n = it->m_key;
for (auto const& kv : m_map) {
expr * n = kv.m_key;
if (is_app(n) && to_app(n)->get_num_args() > 0) {
continue;
}
sat::bool_var v = it->m_value;
sat::bool_var v = kv.m_value;
switch (sat::value_at(v, ll_m)) {
case l_true:
md->register_decl(to_app(n)->get_decl(), m.mk_true());

35
src/sat/tactic/sat_tactic.cpp
View file

@ -16,11 +16,11 @@ Author:
Notes:
--*/
#include "ast/ast_pp.h"
#include "tactic/tactical.h"
#include "tactic/filter_model_converter.h"
#include "sat/tactic/goal2sat.h"
#include "sat/sat_solver.h"
#include "tactic/filter_model_converter.h"
#include "ast/ast_smt2_pp.h"
#include "model/model_v2_pp.h"
class sat_tactic : public tactic {
@ -56,11 +56,9 @@ class sat_tactic : public tactic {
sat::literal_vector assumptions;
m_goal2sat(*g, m_params, m_solver, map, dep2asm);
TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n";
atom2bool_var::iterator it = map.begin();
atom2bool_var::iterator end = map.end();
for (; it != end; ++it) {
if (!is_uninterp_const(it->m_key))
tout << mk_ismt2_pp(it->m_key, m) << "\n";
for (auto const& kv : map) {
if (!is_uninterp_const(kv.m_key))
tout << mk_ismt2_pp(kv.m_key, m) << "\n";
});
g->reset();
g->m().compact_memory();
@ -70,6 +68,11 @@ class sat_tactic : public tactic {
TRACE("sat_dimacs", m_solver.display_dimacs(tout););
dep2assumptions(dep2asm, assumptions);
lbool r = m_solver.check(assumptions.size(), assumptions.c_ptr());
if (r == l_undef && m_solver.get_config().m_dimacs_display) {
for (auto const& kv : map) {
std::cout << "c " << kv.m_value << " " << mk_pp(kv.m_key, g->m()) << "\n";
}
}
if (r == l_false) {
expr_dependency * lcore = 0;
if (produce_core) {
@ -90,11 +93,9 @@ class sat_tactic : public tactic {
model_ref md = alloc(model, m);
sat::model const & ll_m = m_solver.get_model();
TRACE("sat_tactic", for (unsigned i = 0; i < ll_m.size(); i++) tout << i << ":" << ll_m[i] << " "; tout << "\n";);
atom2bool_var::iterator it = map.begin();
atom2bool_var::iterator end = map.end();
for (; it != end; ++it) {
expr * n = it->m_key;
sat::bool_var v = it->m_value;
for (auto const& kv : map) {
expr * n = kv.m_key;
sat::bool_var v = kv.m_value;
TRACE("sat_tactic", tout << "extracting value of " << mk_ismt2_pp(n, m) << "\nvar: " << v << "\n";);
switch (sat::value_at(v, ll_m)) {
case l_true:
@ -126,17 +127,15 @@ class sat_tactic : public tactic {
void dep2assumptions(obj_map<expr, sat::literal>& dep2asm,
sat::literal_vector& assumptions) {
obj_map<expr, sat::literal>::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
assumptions.push_back(it->m_value);
for (auto const& kv : dep2asm) {
assumptions.push_back(kv.m_value);
}
}
void mk_asm2dep(obj_map<expr, sat::literal>& dep2asm,
u_map<expr*>& lit2asm) {
obj_map<expr, sat::literal>::iterator it = dep2asm.begin(), end = dep2asm.end();
for (; it != end; ++it) {
lit2asm.insert(it->m_value.index(), it->m_key);
for (auto const& kv : dep2asm) {
lit2asm.insert(kv.m_value.index(), kv.m_key);
}
}
};