alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

spot: Implement dt*a_sat_minimize_assume(...) methods

Browse source 
* python/spot/__init__.py: Add 'assume' option.
* spot/misc/satsolver.cc: Add function to handle assumptions.
* spot/misc/satsolver.hh: Declare assumption function.
* spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_assume.
* spot/twaalgos/dtbasat.hh: Declare it.
* spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_assume and
handle options.
* spot/twaalgos/dtwasat.hh: Declare it.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Use param_ var for incr and assume.
* tests/core/satmin.test: Add tests for the new function.
* tests/core/satmin2.test: Add tests for the new function.
* tests/python/satmin.py: Add tests for the new function.
This commit is contained in:
Alexandre GBAGUIDI AISSE 2016-10-11 16:08:46 +02:00
parent ee17c2dee4
commit 9a204b770f
12 changed files with 1021 additions and 69 deletions
Download patch file Download diff file Expand all files Collapse all files

30
spot/misc/satsolver.cc
View file

@ -74,7 +74,7 @@ namespace spot
// easy to check if psat_ was initialized or not.
satsolver::satsolver()
: cnf_tmp_(nullptr), cnf_stream_(nullptr), nclauses_(0), nvars_(0),
psat_(nullptr)
nassumptions_vars_(0), nsols_(0), psat_(nullptr)
{
if (cmd_.command_given())
{
@ -123,21 +123,27 @@ namespace spot
void satsolver::adjust_nvars(int nvars)
{
if (nvars < 0)
throw std::runtime_error(": total number of lits. must be at least 0.");
throw std::runtime_error("variable number must be at least 0");
if (psat_)
{
picosat_adjust(psat_, nvars);
picosat_adjust(psat_, nvars + nassumptions_vars_);
}
else
{
if (nvars < nvars_)
if (nvars + nassumptions_vars_ < nvars_)
{
throw std::runtime_error(
": wrong number of variables, a bigger one was already added.");
}
nvars_ = nvars;
nvars_ = nvars + nassumptions_vars_;
}
nsols_ = nvars;
}
void satsolver::set_nassumptions_vars(int nassumptions_vars)
{
nassumptions_vars_ = nassumptions_vars;
}
void satsolver::add(std::initializer_list<int> values)
@ -196,6 +202,15 @@ namespace spot
return std::make_pair(get_nb_vars(), get_nb_clauses());
}
void satsolver::assume(int lit)
{
if (psat_)
picosat_assume(psat_, lit);
else
throw std::runtime_error(
"satsolver::assume(...) can not be used with an external satsolver");
}
satsolver::solution
spot::satsolver::satsolver_get_sol(const char* filename)
{
@ -249,11 +264,8 @@ namespace spot
{
satsolver::solution sol;
if (res == PICOSAT_SATISFIABLE)
{
int nvars = get_nb_vars();
for (int lit = 1; lit <= nvars; ++lit)
for (int lit = 1; lit <= nsols_; ++lit)
sol.push_back(picosat_deref(psat_, lit) > 0);
}
return sol;
}

12
spot/misc/satsolver.hh
View file

@ -79,6 +79,9 @@ namespace spot
/// \brief Adjust the number of variables used in the cnf formula.
void adjust_nvars(int nvars);
/// \brief Declare the number of vars reserved for assumptions.
void set_nassumptions_vars(int nassumptions_vars);
/// \brief Add a list of lit. to the current clause.
void add(std::initializer_list<int> values);
@ -114,6 +117,10 @@ namespace spot
template<typename T, typename... Args>
void comment(T first, Args... args);
/// \brief Assume a litteral value.
/// Must only be used with distributed picolib.
void assume(int lit);
typedef std::vector<bool> solution;
typedef std::pair<int, solution> solution_pair;
@ -146,6 +153,11 @@ namespace spot
std::ostream* cnf_stream_;
int nclauses_;
int nvars_;
int nassumptions_vars_; // Surplus of vars (for 'assume' algorithm).
/// \brief Number of solutions to obtain from the satsolver
/// (without assuming litterals).
int nsols_;
/// \brief Picosat satsolver instance.
PicoSAT* psat_;

156
spot/twaalgos/dtbasat.cc
View file

@ -297,7 +297,8 @@ namespace spot
static
sat_stats dtba_to_sat(satsolver& solver,
const const_twa_graph_ptr& ref,
dict& d, bool state_based)
dict& d,
bool state_based)
{
// Compute the AP used.
bdd ap = ref->ap_vars();
@ -744,6 +745,159 @@ namespace spot
return res;
}
static twa_graph_ptr
dichotomy_dtba_research(int max,
dict& d,
satsolver& solver,
timer_map& t1,
const_twa_graph_ptr& prev,
bool state_based)
{
trace << "dichotomy_dtba_research(...)\n";
int min = 1;
int target = 0;
twa_graph_ptr res = nullptr;
while (min < max)
{
target = (max + min) / 2;
trace << "min:" << min << ", max:" << max << ", target:" << target
<< '\n';
solver.assume(d.nvars + target);
trace << "solver.assume(" << d.nvars + target << ")\n";
satsolver::solution_pair solution = solver.get_solution();
if (solution.second.empty())
{
trace << "UNSAT\n";
max = target;
}
else
{
trace << "SAT\n";
res = sat_build(solution.second, d, prev, state_based);
min = d.cand_size - stats_reachable(res).states + 1;
}
}
trace << "End with max:" << max << ", min:" << min << '\n';
if (!res)
{
trace << "All assumptions are UNSAT, let's try without...";
satsolver::solution_pair solution = solver.get_solution();
trace << (solution.second.empty() ? "UNSAT!\n" : "SAT\n");
res = solution.second.empty() ? nullptr :
sat_build(solution.second, d, prev, state_based);
}
t1.stop("solve");
print_log(t1, d.cand_size - target, res, solver); // SPOT_SATLOG.
return res ? res : std::const_pointer_cast<spot::twa_graph>(prev);
}
twa_graph_ptr
dtba_sat_minimize_assume(const const_twa_graph_ptr& a,
bool state_based,
int max_states,
int sat_incr_steps)
{
if (!a->acc().is_buchi())
throw std::runtime_error
("dtba_sat_minimize_assume() can only work with Büchi acceptance");
if (sat_incr_steps < 0)
throw std::runtime_error("with 'assume' algorithm, sat_incr_steps value "
" must be >= 0");
const_twa_graph_ptr prev = a;
dict d;
d.cand_size = (max_states < 0) ?
stats_reachable(prev).states - 1 : max_states;
if (d.cand_size == 0)
return nullptr;
trace << "dtba_sat_minimize_assume(..., states = " << d.cand_size
<< ", state_based = " << state_based << ")\n";
trace << "sat_incr_steps: " << sat_incr_steps << '\n';
twa_graph_ptr next = spot::make_twa_graph(spot::make_bdd_dict());
while (next && d.cand_size > 0)
{
// Warns the satsolver of the number of assumptions.
int n_assumptions = (int) d.cand_size < sat_incr_steps ?
d.cand_size - 1 : sat_incr_steps;
trace << "number of assumptions:" << n_assumptions << '\n';
satsolver solver;
solver.set_nassumptions_vars(n_assumptions);
// First iteration of classic solving.
timer_map t1;
t1.start("encode");
dtba_to_sat(solver, prev, d, state_based);
// Compute the AP used.
bdd ap = prev->ap_vars();
// Add all assumptions clauses.
unsigned dst = d.cand_size - 1;
unsigned alpha_size = d.alpha_vect.size();
for (int i = 1; i <= n_assumptions; i++, dst--)
{
cnf_comment("Next iteration:", dst, "\n");
int assume_lit = d.nvars + i;
cnf_comment("Add clauses to forbid the dst state.\n");
for (unsigned l = 0; l < alpha_size; ++l)
for (unsigned j = 0; j < d.cand_size; ++j)
{
cnf_comment(assume_lit, "→ ¬", d.fmt_t(j, l, dst), '\n');
solver.add({-assume_lit, -d.transid(j, l, dst), 0});
}
// The assumption which has just been encoded implies the preceding
// ones.
if (i != 1)
{
cnf_comment(assume_lit, "→", assume_lit - 1, '\n');
solver.add({-assume_lit, assume_lit - 1, 0});
}
}
t1.stop("encode");
t1.start("solve");
if (n_assumptions)
{
trace << "solver.assume(" << d.nvars + n_assumptions << ")\n";
solver.assume(d.nvars + n_assumptions);
}
satsolver::solution_pair solution = solver.get_solution();
if (solution.second.empty() && n_assumptions) // UNSAT
{
trace << "UNSAT\n";
return dichotomy_dtba_research(n_assumptions, d, solver, t1, prev,
state_based);
}
t1.stop("solve");
trace << "SAT, restarting from zero\n";
next = solution.second.empty() ? nullptr :
sat_build(solution.second, d, prev, state_based);
print_log(t1, d.cand_size - n_assumptions, next, solver); // SPOT_SATLOG.
if (next)
{
prev = next;
d = dict();
d.cand_size = stats_reachable(prev).states - 1;
if (d.cand_size == 0)
next = nullptr;
}
}
return prev == a ? nullptr : std::const_pointer_cast<spot::twa_graph>(prev);
}
twa_graph_ptr
dtba_sat_minimize_incr(const const_twa_graph_ptr& a,
bool state_based, int max_states, int sat_incr_steps)

19
spot/twaalgos/dtbasat.hh
View file

@ -81,4 +81,23 @@ namespace spot
bool state_based = false,
int max_states = -1,
int param = 2);
/// \brief Attempt to minimize a deterministic TBA incrementally with a SAT
/// solver.
///
/// This acts like dtba_sat_synthetize() and obtains a first minimized
/// automaton. Then, it adds <param> assumptions, such that each assumption
/// removes a new state and implies the previous assumptions. A first
/// resolution is attempted assuming the last assumption (thus involving all
/// the previous ones). If the problem is SAT several stages have just been
/// won and all this process is restarted. Otherwise, we know that the
/// minimal automaton can be obtained with fewer assumption. This
/// automaton is found dichotomously.
///
/// If no smaller TBA exist, this returns a null pointer.
SPOT_API twa_graph_ptr
dtba_sat_minimize_assume(const const_twa_graph_ptr& a,
bool state_based = false,
int max_states = -1,
int param = 6);
}

181
spot/twaalgos/dtwasat.cc
View file

@ -532,8 +532,11 @@ namespace spot
typedef std::pair<int, int> sat_stats;
static
sat_stats dtwa_to_sat(satsolver& solver, const_twa_graph_ptr ref,
dict& d, bool state_based, bool colored)
sat_stats dtwa_to_sat(satsolver& solver,
const_twa_graph_ptr ref,
dict& d,
bool state_based,
bool colored)
{
#if DEBUG
debug_dict = ref->get_dict();
@ -1054,6 +1057,166 @@ namespace spot
}
}
static twa_graph_ptr
dichotomy_dtwa_research(int max,
dict& d,
satsolver& solver,
timer_map& t1,
const_twa_graph_ptr& prev,
bool state_based)
{
trace << "dichotomy_dtwa_research(...)\n";
int min = 1;
int target = 0;
twa_graph_ptr res = nullptr;
while (min < max)
{
target = (max + min) / 2;
trace << "min:" << min << ", max:" << max << ", target:" << target
<< '\n';
solver.assume(d.nvars + target);
trace << "solver.assume(" << d.nvars + target << ")\n";
satsolver::solution_pair solution = solver.get_solution();
if (solution.second.empty())
{
trace << "UNSAT\n";
max = target;
}
else
{
trace << "SAT\n";
res = sat_build(solution.second, d, prev, state_based);
min = d.cand_size - stats_reachable(res).states + 1;
}
}
trace << "End with max:" << max << ", min:" << min << '\n';
if (!res)
{
trace << "All assumptions are UNSAT, let's try without...";
satsolver::solution_pair solution = solver.get_solution();
trace << (solution.second.empty() ? "UNSAT!\n" : "SAT\n");
res = solution.second.empty() ? nullptr :
sat_build(solution.second, d, prev, state_based);
}
t1.stop("solve");
print_log(t1, d.cand_size - target , res, solver); // SPOT_SATLOG.
return res ? res : std::const_pointer_cast<spot::twa_graph>(prev);
}
twa_graph_ptr
dtwa_sat_minimize_assume(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based,
int max_states,
bool colored,
int sat_incr_steps)
{
if (sat_incr_steps < 0)
throw std::runtime_error("with 'assume' algorithm, sat_incr_steps value "
"must be >= 0");
const_twa_graph_ptr prev = a;
dict d(prev);
d.cand_size = (max_states < 0) ?
stats_reachable(prev).states - 1 : max_states;
d.cand_nacc = target_acc_number;
d.cand_acc = target_acc;
if (d.cand_size == 0)
return nullptr;
trace << "dtwa_sat_minimize_assume(..., nacc = " << target_acc_number
<< ", acc = \"" << target_acc << "\", states = " << d.cand_size
<< ", state_based = " << state_based << ")\n";
trace << "sat_incr_steps: " << sat_incr_steps << '\n';
twa_graph_ptr next = spot::make_twa_graph(spot::make_bdd_dict());
while (next && d.cand_size > 0)
{
// Warns the satsolver of the number of assumptions.
int n_assumptions = (int) d.cand_size < sat_incr_steps ?
d.cand_size - 1 : sat_incr_steps;
trace << "number of assumptions:" << n_assumptions << '\n';
satsolver solver;
solver.set_nassumptions_vars(n_assumptions);
// First iteration of classic solving.
timer_map t1;
t1.start("encode");
dtwa_to_sat(solver, prev, d, state_based, colored);
// Compute the AP used.
bdd ap = prev->ap_vars();
// Add all assumptions clauses.
unsigned dst = d.cand_size - 1;
unsigned alpha_size = d.alpha_vect.size();
for (int i = 1; i <= n_assumptions; i++, dst--)
{
cnf_comment("Next iteration:", dst, "\n");
int assume_lit = d.nvars + i;
cnf_comment("Add clauses to forbid the dst state.\n");
for (unsigned l = 0; l < alpha_size; ++l)
for (unsigned j = 0; j < d.cand_size; ++j)
{
cnf_comment(assume_lit, "→ ¬", d.fmt_t(j, l, dst), '\n');
solver.add({-assume_lit, -d.transid(j, l, dst), 0});
}
// The assumption which has just been encoded implies the preceding
// ones.
if (i != 1)
{
cnf_comment(assume_lit, "→", assume_lit - 1, '\n');
solver.add({-assume_lit, assume_lit - 1, 0});
}
}
t1.stop("encode");
t1.start("solve");
if (n_assumptions)
{
trace << "solver.assume(" << d.nvars + n_assumptions << ")\n";
solver.assume(d.nvars + n_assumptions);
}
satsolver::solution_pair solution = solver.get_solution();
if (solution.second.empty() && n_assumptions) // UNSAT
{
trace << "UNSAT\n";
twa_graph_ptr res = dichotomy_dtwa_research(n_assumptions, d, solver,
t1, prev, state_based);
return res == a ? nullptr : res;
}
t1.stop("solve");
trace << "SAT, restarting from zero\n";
next = solution.second.empty() ? nullptr :
sat_build(solution.second, d, prev, state_based);
print_log(t1, d.cand_size - n_assumptions, next, solver); // SPOT_SATLOG.
if (next)
{
prev = next;
d = dict(prev);
d.cand_size = stats_reachable(prev).states - 1;
d.cand_nacc = target_acc_number;
d.cand_acc = target_acc;
if (d.cand_size == 0)
next = nullptr;
}
}
return prev == a ? nullptr : std::const_pointer_cast<spot::twa_graph>(prev);
}
twa_graph_ptr
dtwa_sat_minimize_incr(const const_twa_graph_ptr& a,
unsigned target_acc_number,
@ -1220,13 +1383,14 @@ namespace spot
("SAT-based minimization only works with deterministic automata");
bool dicho = om.get("dichotomy", 0);
bool incr = om.get("incr", 0);
bool assume = om.get("assume", 0);
int param = om.get("param", 0);
int states = om.get("states", -1);
int max_states = om.get("max-states", -1);
auto accstr = om.get_str("acc");
bool colored = om.get("colored", 0);
int preproc = om.get("preproc", 3);
bool incr = om.get("incr", 0);
int param = om.get("param", 0);
// No more om.get() below this.
om.report_unused_options();
@ -1323,6 +1487,11 @@ namespace spot
if (incr)
a = dtwa_sat_minimize_incr(a, nacc, target_acc, state_based,
max_states, colored, param);
else if (assume)
a = dtwa_sat_minimize_assume(a, nacc, target_acc, state_based,
max_states, colored, param);
else
a = (dicho ? dtwa_sat_minimize_dichotomy
: dtwa_sat_minimize)
@ -1332,6 +1501,10 @@ namespace spot
{
if (incr)
a = dtba_sat_minimize_incr(a, state_based, max_states, param);
else if (assume)
a = dtba_sat_minimize_assume(a, state_based, max_states, assume);
else
a = (dicho ? dtba_sat_minimize_dichotomy
: dtba_sat_minimize)

21
spot/twaalgos/dtwasat.hh
View file

@ -102,6 +102,27 @@ namespace spot
bool colored = false,
int param = 2);
/// \brief Attempt to minimize a deterministic TωA with a SAT solver.
///
/// This acts like dtba_sat_synthetize() and obtains a first minimized
/// automaton. Then, it adds <param> assumptions, such that each assumption
/// removes a new state and implies the previous assumptions. A first
/// resolution is attempted assuming the last assumption (thus involving all
/// the previous ones). If the problem is SAT several stages have just been
/// won and all this process is restarted. Otherwise, it is known that the
/// minimal automaton can be obtained with fewer assumption. This
/// automaton is found dichotomously.
///
/// If no smaller TGBA exists, this returns a null pointer.
SPOT_API twa_graph_ptr
dtwa_sat_minimize_assume(const const_twa_graph_ptr& a,
unsigned target_acc_number,
const acc_cond::acc_code& target_acc,
bool state_based = false,
int max_states = -1,
bool colored = false,
int param = 6);
/// \brief High-level interface to SAT-based minimization
///
/// Minimize the automaton \a aut, using options \a opt.

19
spot/twaalgos/postproc.cc
View file

@ -69,8 +69,8 @@ namespace spot
scc_filter_ = opt->get("scc-filter", -1);
ba_simul_ = opt->get("ba-simul", -1);
tba_determinisation_ = opt->get("tba-det", 0);
incr_ = opt->get("incr", 0);
sat_minimize_ = opt->get("sat-minimize", 0);
param_ = opt->get("param", 0);
sat_acc_ = opt->get("sat-acc", 0);
sat_states_ = opt->get("sat-states", 0);
state_based_ = opt->get("state-based", 0);
@ -430,8 +430,10 @@ namespace spot
res = dtba_sat_minimize(res, state_based_);
else if (sat_minimize_ == 2)
res = dtba_sat_minimize_dichotomy(res, state_based_);
else // sat_minimize_ = 3
res = dtba_sat_minimize_incr(res, state_based_, -1, incr_);
else if (sat_minimize_ == 3)
res = dtba_sat_minimize_incr(res, state_based_, -1, param_);
else // if (sat_minimize == 4)
res = dtba_sat_minimize_assume(res, state_based_, -1, param_);
}
else
{
@ -450,12 +452,17 @@ namespace spot
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_);
else // sat_minimize_ = 3
else if (sat_minimize_ == 3)
res = dtwa_sat_minimize_incr
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_, -1, false, incr_);
}
state_based_, -1, false, param_);
else // if (sat_minimize_ == 4)
res = dtwa_sat_minimize_assume
(res, target_acc,
acc_cond::acc_code::generalized_buchi(target_acc),
state_based_, -1, false, param_);
}
if (res)
{

2
spot/twaalgos/postproc.hh
View file

@ -188,8 +188,8 @@ namespace spot
int scc_filter_ = -1;
int ba_simul_ = -1;
bool tba_determinisation_ = false;
int incr_ = 0;
int sat_minimize_ = 0;
int param_ = 0;
int sat_acc_ = 0;
int sat_states_ = 0;
bool state_based_ = false;