search

tnelson / Margrave

The Margrave tool for policy analysis
9 stars 1 forks source link

Show Realized could be much faster. Current design too complicated. #100

Closed tnelson closed 11 years ago

tnelson commented 12 years ago

SHOW REALIZED accepts* sets of atomic formulas like: permit(s, a, r), and returns the subset such that some model realizes

Since the inputs are atomic formulas, terms are involved. Right now, the conversion from terms to model-elements is all done "by hand", and the FULL IDB is axiomatized. E.g.:

forall s, forall a, forall r permit(s, a, r) <---> idbfmla(permit)

Kodkod does not support nullary relations, so we cannot do:

permitsar <----> idbfmla(permit)(s, a, r)
(which would be fine, since s, a and r are free and will be existentially closed.)

Hence the gyrations we go through to convert to and from terms in Java's MShowRealized, and the big slow-down when there are many tuples that can be permitted -- there are #tuples (well sorted of course) prop. variables used. And a large number of clauses to account for variable-assignments...

...but we CAN do something like this:

\forall dummy^UNIV permitsar(dummy) <----> idbfmla(permit)(s,a,r)

Now there are only #elements prop. variables assigned to each condition. With this method, Kodkod is doing the conversion from/to terms for us (still only one translation), and the number of new vars/clauses shrinks substantially, making SR much faster to execute.

tnelson commented 12 years ago

Above soln raises concerns of multiplicities of models b/c of variation in what goes into idbfmla. Instead, let's bound the IDBT relation (one per idbname/tuple pair of interest) to , and use this axiomatization fmla instead:

(\exists d^UNIV IDBT(d)) <---> \alpha(tvec)

Now only one specific ele is in IDBT's upper bound (or none). This removes the multiplicity concern and makes the axiomatization more efficient.

tnelson commented 11 years ago

upping priority of this change since it lowers complexity of sat-solver twiddling, which we clearly need after this week's show realized problems (when a candidate is unsat via contradiction exception).

tnelson commented 11 years ago

improvement: add ONE "srhelper" atom. ub of each helper idb = it. now we just say "some helperidb iff...". and for adding that atom, SR is now just assumptions. no new clauses needed.

tnelson commented 11 years ago

Implemented. This should also resolve the odd satsolver null ptr problem we got at Cornell: SR is much simpler now, and only needs to remove a single goal clause.