spot: Abstract cnf writing in SAT-based minimisation
* spot/misc/satsolver.hh: Declare all functions needed. * spot/misc/satsolver.cc: Implement them. * spot/twaalgos/dtbasat.cc: Abstract writing. * spot/twaalgos/dtwasat.cc: Abstract writing.
This commit is contained in:
Alexandre GBAGUIDI AISSE
parent
f2e091b9cd
commit
596bdec910
4 changed files with 213 additions and 156 deletions
|
|
@ -51,8 +51,10 @@
|
|||
#define DEBUG 0
|
||||
#if DEBUG
|
||||
#define dout out << "c "
|
||||
#define cnf_comment(...) solver.comment(__VA_ARGS__)
|
||||
#define trace std::cerr
|
||||
#else
|
||||
#define cnf_comment(...) while (0) solver.comment(__VA_ARGS__)
|
||||
#define dout while (0) std::cout
|
||||
#define trace dout
|
||||
#endif
|
||||
|
|
@ -596,13 +598,12 @@ namespace spot
|
|||
typedef std::pair<int, int> sat_stats;
|
||||
|
||||
static
|
||||
sat_stats dtwa_to_sat(std::ostream& out, const_twa_graph_ptr ref,
|
||||
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();
|
||||
#endif
|
||||
clause_counter nclauses;
|
||||
|
||||
// Compute the AP used in the hard way.
|
||||
bdd ap = bddtrue;
|
||||
|
|
@ -629,23 +630,17 @@ namespace spot
|
|||
|
||||
// empty automaton is impossible
|
||||
if (d.cand_size == 0)
|
||||
{
|
||||
out << "p cnf 1 2\n-1 0\n1 0\n";
|
||||
return std::make_pair(1, 2);
|
||||
}
|
||||
|
||||
// An empty line for the header
|
||||
out << " \n";
|
||||
return solver.stats();
|
||||
|
||||
#if DEBUG
|
||||
debug_ref_acc = &ref->acc();
|
||||
debug_cand_acc = &d.cacc;
|
||||
dout << "ref_size: " << ref_size << '\n';
|
||||
dout << "cand_size: " << d.cand_size << '\n';
|
||||
solver.comment("ref_size:", ref_size, '\n');
|
||||
solver.comment("cand_size:", d.cand_size, '\n');
|
||||
#endif
|
||||
auto& racc = ref->acc();
|
||||
|
||||
dout << "symmetry-breaking clauses\n";
|
||||
cnf_comment("symmetry-breaking clauses\n");
|
||||
int j = 0;
|
||||
bdd all = bddtrue;
|
||||
while (all != bddfalse)
|
||||
|
|
@ -657,16 +652,15 @@ namespace spot
|
|||
{
|
||||
transition t(i, s, k);
|
||||
int ti = d.transid[t];
|
||||
dout << "¬" << t << '\n';
|
||||
out << -ti << " 0\n";
|
||||
++nclauses;
|
||||
cnf_comment("¬", t, '\n');
|
||||
solver.add({-ti, 0});
|
||||
}
|
||||
++j;
|
||||
}
|
||||
if (!nclauses.nb_clauses())
|
||||
dout << "(none)\n";
|
||||
if (!solver.get_nb_clauses())
|
||||
cnf_comment("(none)\n");
|
||||
|
||||
dout << "(8) the candidate automaton is complete\n";
|
||||
cnf_comment("(8) the candidate automaton is complete\n");
|
||||
for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
|
||||
{
|
||||
bdd all = bddtrue;
|
||||
|
|
@ -676,15 +670,15 @@ namespace spot
|
|||
all -= s;
|
||||
|
||||
#if DEBUG
|
||||
dout;
|
||||
solver.comment("");
|
||||
for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
|
||||
{
|
||||
transition t(q1, s, q2);
|
||||
out << t << "δ";
|
||||
solver.comment_rec(t, "δ");
|
||||
if (q2 != d.cand_size)
|
||||
out << " ∨ ";
|
||||
solver.comment_rec(" ∨ ");
|
||||
}
|
||||
out << '\n';
|
||||
solver.comment_rec('\n');
|
||||
#endif
|
||||
|
||||
for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
|
||||
|
|
@ -692,26 +686,24 @@ namespace spot
|
|||
transition t(q1, s, q2);
|
||||
int ti = d.transid[t];
|
||||
|
||||
out << ti << ' ';
|
||||
solver.add(ti);
|
||||
}
|
||||
out << "0\n";
|
||||
++nclauses;
|
||||
solver.add(0);
|
||||
}
|
||||
}
|
||||
|
||||
dout << "(9) the initial state is reachable\n";
|
||||
cnf_comment("(9) the initial state is reachable\n");
|
||||
{
|
||||
unsigned init = ref->get_init_state_number();
|
||||
dout << path(0, init) << '\n';
|
||||
out << d.pathid[path(0, init)] << " 0\n";
|
||||
++nclauses;
|
||||
cnf_comment(path(0, init), '\n');
|
||||
solver.add({d.pathid[path(0, init)], 0});
|
||||
}
|
||||
|
||||
if (colored)
|
||||
{
|
||||
unsigned nacc = d.cand_nacc;
|
||||
dout << "transitions belong to exactly one of the "
|
||||
<< nacc << " acceptance set\n";
|
||||
cnf_comment("transitions belong to exactly one of the", nacc,
|
||||
"acceptance set\n");
|
||||
bdd all = bddtrue;
|
||||
while (all != bddfalse)
|
||||
{
|
||||
|
|
@ -730,25 +722,23 @@ namespace spot
|
|||
{
|
||||
transition_acc tj(q1, l, {j}, q2);
|
||||
int taj = d.transaccid[tj];
|
||||
out << -tai << ' ' << -taj << " 0\n";
|
||||
++nclauses;
|
||||
solver.add({-tai, -taj, 0});
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < nacc; ++i)
|
||||
{
|
||||
transition_acc ti(q1, l, {i}, q2);
|
||||
int tai = d.transaccid[ti];
|
||||
out << tai << ' ';
|
||||
solver.add(tai);
|
||||
}
|
||||
out << "0\n";
|
||||
++nclauses;
|
||||
solver.add(0);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (!d.all_silly_cand_acc.empty())
|
||||
{
|
||||
dout << "no transition with silly acceptance\n";
|
||||
cnf_comment("no transition with silly acceptance\n");
|
||||
bdd all = bddtrue;
|
||||
while (all != bddfalse)
|
||||
{
|
||||
|
|
@ -758,25 +748,24 @@ namespace spot
|
|||
for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
|
||||
for (auto& s: d.all_silly_cand_acc)
|
||||
{
|
||||
dout << "no (" << q1 << ','
|
||||
<< bdd_format_formula(debug_dict, l)
|
||||
<< ',' << s << ',' << q2 << ")\n";
|
||||
cnf_comment("no (", q1, ',',
|
||||
bdd_format_formula(debug_dict, l), ',', s,
|
||||
',', q2, ")\n");
|
||||
for (unsigned v: s.sets())
|
||||
{
|
||||
transition_acc ta(q1, l, d.cacc.mark(v), q2);
|
||||
int tai = d.transaccid[ta];
|
||||
assert(tai != 0);
|
||||
out << ' ' << -tai;
|
||||
solver.add(-tai);
|
||||
}
|
||||
for (unsigned v: d.cacc.comp(s).sets())
|
||||
{
|
||||
transition_acc ta(q1, l, d.cacc.mark(v), q2);
|
||||
int tai = d.transaccid[ta];
|
||||
assert(tai != 0);
|
||||
out << ' ' << tai;
|
||||
solver.add(tai);
|
||||
}
|
||||
out << " 0\n";
|
||||
++nclauses;
|
||||
solver.add(0);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -786,8 +775,8 @@ namespace spot
|
|||
{
|
||||
if (!sm.reachable_state(q1p))
|
||||
continue;
|
||||
dout << "(10) augmenting paths based on Cand[" << q1
|
||||
<< "] and Ref[" << q1p << "]\n";
|
||||
cnf_comment("(10) augmenting paths based on Cand[", q1,
|
||||
"] and Ref[", q1p, "]\n");
|
||||
path p1(q1, q1p);
|
||||
int p1id = d.pathid[p1];
|
||||
|
||||
|
|
@ -811,9 +800,8 @@ namespace spot
|
|||
if (p1id == succ)
|
||||
continue;
|
||||
|
||||
dout << p1 << " ∧ " << t << "δ → " << p2 << '\n';
|
||||
out << -p1id << ' ' << -ti << ' ' << succ << " 0\n";
|
||||
++nclauses;
|
||||
cnf_comment(p1, "∧", t, "δ →", p2, '\n');
|
||||
solver.add({-p1id, -ti, succ, 0});
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -854,7 +842,8 @@ namespace spot
|
|||
path p(q1, q1p, q2, q2p,
|
||||
d.all_cand_acc[f], refhist);
|
||||
|
||||
dout << "(11&12&13) paths from " << p << '\n';
|
||||
cnf_comment("(11&12&13) paths from ", p,
|
||||
'\n');
|
||||
|
||||
int pid = d.pathid[p];
|
||||
|
||||
|
|
@ -892,10 +881,9 @@ namespace spot
|
|||
for (auto& v: missing)
|
||||
{
|
||||
#if DEBUG
|
||||
dout << (rejloop ?
|
||||
"(11) " : "(12) ")
|
||||
<< p << " ∧ "
|
||||
<< t << "δ → (";
|
||||
solver.comment((rejloop ?
|
||||
"(11) " : "(12) "), p,
|
||||
" ∧ ", t, "δ → (");
|
||||
const char* orsep = "";
|
||||
for (int s: v)
|
||||
{
|
||||
|
|
@ -905,21 +893,23 @@ namespace spot
|
|||
ta(q2, l,
|
||||
d.cacc.mark(-s - 1),
|
||||
q1);
|
||||
out << orsep << "¬" << ta;
|
||||
solver.comment_rec(orsep,
|
||||
"¬", ta);
|
||||
}
|
||||
else
|
||||
{
|
||||
transition_acc
|
||||
ta(q2, l,
|
||||
d.cacc.mark(s), q1);
|
||||
out << orsep << ta;
|
||||
solver.comment_rec(orsep,
|
||||
ta);
|
||||
}
|
||||
out << "FC";
|
||||
solver.comment_rec("FC");
|
||||
orsep = " ∨ ";
|
||||
}
|
||||
out << ")\n";
|
||||
solver.comment_rec(")\n");
|
||||
#endif // DEBUG
|
||||
out << -pid << ' ' << -ti;
|
||||
solver.add({-pid, -ti});
|
||||
for (int s: v)
|
||||
if (s < 0)
|
||||
{
|
||||
|
|
@ -929,7 +919,7 @@ namespace spot
|
|||
q1);
|
||||
int tai = d.transaccid[ta];
|
||||
assert(tai != 0);
|
||||
out << ' ' << -tai;
|
||||
solver.add(-tai);
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -938,10 +928,9 @@ namespace spot
|
|||
d.cacc.mark(s), q1);
|
||||
int tai = d.transaccid[ta];
|
||||
assert(tai != 0);
|
||||
out << ' ' << tai;
|
||||
solver.add(tai);
|
||||
}
|
||||
out << " 0\n";
|
||||
++nclauses;
|
||||
solver.add(0);
|
||||
}
|
||||
}
|
||||
// (13) augmenting paths (always).
|
||||
|
|
@ -964,8 +953,8 @@ namespace spot
|
|||
if (pid == p2id)
|
||||
continue;
|
||||
#if DEBUG
|
||||
dout << "(13) " << p << " ∧ "
|
||||
<< t << "δ ";
|
||||
solver.comment("(13) ", p, " ∧ ",
|
||||
t, "δ ");
|
||||
|
||||
auto biga_ = d.all_cand_acc[f];
|
||||
for (unsigned m = 0;
|
||||
|
|
@ -977,12 +966,13 @@ namespace spot
|
|||
const char* not_ = "¬";
|
||||
if (biga_.has(m))
|
||||
not_ = "";
|
||||
out << " ∧ " << not_
|
||||
<< ta << "FC";
|
||||
solver.comment_rec(" ∧ ", not_,
|
||||
ta, "FC");
|
||||
}
|
||||
out << " → " << p2 << '\n';
|
||||
solver.comment_rec(" → ", p2,
|
||||
'\n');
|
||||
#endif
|
||||
out << -pid << ' ' << -ti << ' ';
|
||||
solver.add({-pid, -ti});
|
||||
auto biga = d.all_cand_acc[f];
|
||||
for (unsigned m = 0;
|
||||
m < d.cand_nacc; ++m)
|
||||
|
|
@ -993,11 +983,9 @@ namespace spot
|
|||
int tai = d.transaccid[ta];
|
||||
if (biga.has(m))
|
||||
tai = -tai;
|
||||
out << tai << ' ';
|
||||
solver.add(tai);
|
||||
}
|
||||
|
||||
out << p2id << " 0\n";
|
||||
++nclauses;
|
||||
solver.add({p2id, 0});
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1007,9 +995,7 @@ namespace spot
|
|||
}
|
||||
}
|
||||
}
|
||||
out.seekp(0);
|
||||
out << "p cnf " << d.nvars << ' ' << nclauses.nb_clauses();
|
||||
return std::make_pair(d.nvars, nclauses.nb_clauses());
|
||||
return solver.stats(d.nvars);
|
||||
}
|
||||
|
||||
static twa_graph_ptr
|
||||
|
|
@ -1136,7 +1122,7 @@ namespace spot
|
|||
|
||||
timer_map t;
|
||||
t.start("encode");
|
||||
sat_stats s = dtwa_to_sat(solver(), a, d, state_based, colored);
|
||||
sat_stats s = dtwa_to_sat(solver, a, d, state_based, colored);
|
||||
t.stop("encode");
|
||||
t.start("solve");
|
||||
solution = solver.get_solution();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue