DESC.txt

Modified: August 31st 2012 (TN)
Contact: tn@cs.wpi.edu

This document describes the classes we added to Kodkod in order to
produce minimal models and allow augmentation of those models. 

ADVANTAGES:

Aluminum (our modified version of Alloy that produces minimal models)
required these changes to Kodkod, and only some UI alterations to
Alloy otherwise. With these changes, Aluminum could use Kodkod
out-of-the-box to produce models and perform augmentation.

THEORY: 

We'll use the term "relational fact" to mean whether, in an instance
I, a given tuple is in a relation. These are the relational entities
that Kodkod maps to/from propositional variables via its Translation
class. 

There is a partial order <= on all instances given by relational
facts: I <= I' if and only if the relational facts true in I are a
subset of the relational facts true in I'. We are interested in
finding and manipulating the models that are minimal under this
ordering.

CAVEATS:

* The new classes are just modifications to the originals.  Where
Kodkod has Solver, we have MinSolver. SolutionIterator becomes
MinSolutionIterator, and so on. Since many of Kodkod's classes were
final, we duplicate some code (e.g. Solver and MinSolver). Since many
of Kodkod's fields and constructors are not accessible from outside
the Kodkod package, our package (minkodkod) contains verbatim copies
of some Kodkod files. Files that we have modified have the "Min"
prefix; others can be ignored.

New classes describe their purpose in their javadoc, or in a comment
marked "ALUMINUM:" after the imports in the file.

* Our code only uses SAT4J, not any of the other solvers that Kodkod
supports. To support other solvers, some additional work would be
needed.

* SAT4J does not handle removing unit clauses well. Since we often
need to remove clauses as well as add them, we tend to keep separate
sets of unit and non-unit clauses and pass units as "assumptions" that
are not permanently learned by the solver.

* In our prototype code, all MinSolutionIterators share the same SAT4J
instance. More details on this decision follow, but this is why you
will see calls to e.g. reclaim the solver (claimSATSolver()) or remove
constraints (removeAllConstraints()) in iterator code.


IMPLEMENTATION:

All kodkod-level changes are confined to the minkodkod/ directory of
the repository. The minalloy/ directory contains the UI changes we
made to Alloy.

----------------------------------------

KEEPING THE SYMMETRY-BREAKING PREDICATE SEPARATE

Some of our changes required separating out the CNF for the original
sentence and the symmetry-breaking predicate that Kodkod
produces. This required some changes to the fol2sat package:

* MinSymmetryBreaker.java records the permutations of atoms that are
  broken in the SBP.

* MinTranslator.java, MinTranslation.java and
  MinBool2CNFTranslator.java keep the original CNF and the SBP's CNF
  separate rather than conjoining them in the Boolean-circuit stage.
  This is not without performance cost; by splitting the two formulas
  we sacrifice some simplification. Without this change, minimization
  is profoundly unsound. So enabling minimization should probably be
  an option.

and in the root minkodkod package:

* MinSATSolver.java is our wrapper for SAT4J, and it implements the
  SATSolver interface from Kodkod. We added the ability to add/remove
  the SBP's clauses via its activateSBP() and deactivateSBP() methods.

----------------------------------------

PRODUCING MINIMAL MODELS

MinSolver.java produces iterators (MinSolutionIterator) over only the
<=-minimal instances. The actual minimization is done in the iterator
itself (also defined in MinSolver.java).

* The MinSolutionIterator.solve() method prepares minimal models,
returning true iff there are more minimal models to give. It first
finds a candidate propositional model by calling
translation.cnf().solve() --- just as Kodkod does --- and then calls
minimize() on it. minimize() iteratively removes facts that can be
consistently removed from the model. It terminates when no more facts
can be removed.

* Note that we want models that are minimal with respect to the CNF of
the original relational sentence; NOT with respect to the
symmetry-breaking predicate as well. So we keep the two separate as
mentioned above, and minimize() calls deactivateSBP() before trying to
minimize.

* Of course, we make sure that minimal models are never
repeated. Where Kodkod would issue a clause with the negation of the
diagram of M ("Never give me this model again"), we issue the negation
of the positive diagram of (minimal) M ("Never give me a model >= this
one."); we call this the "cone-restriction" clause in some of the
comments. Each iterator remembers its cone-restriction clauses
(MinSolutionIterator.coneRestrictionClauses). This is done in the
nonTrivialSolution() method of MinSolutionIterator.

* We issue additional cone restriction clauses in an attempt to rule
out isomorphic models admitted by disabling the SBP for
minimization. We call these the "shadow" or "permutation" clauses in
some of the comments. The cone-restriction clause and the shadow
clauses are added separately via calls to addConeRestriction()
vs. addPermConeRestriction().

---------------------------------------- 

GETTING ALL CONSISTENT FACTS

Given an instance I, a consistent-fact of I is a relational fact F
that is *not* true in I, but for which there exists an I' > I where F
is true. 

Given a MinSolutionIterator, MinSolver.getConsistentFacts() produces
the consistent-fact set of the last instance that the iterator
produced. This involves some translation between the propositional and
relational views, which is handled by the MinTwoWayTranslator
class. The CF set is returned as an Instance whose tuples are the
consistent facts.

We disable symmetry-breaking via deactivateSBP() when computing this
set. (I can give more detail here if desired.)

---------------------------------------- 

AUGMENTING MODELS WITH CONSISTENT FACTS

MinSolver can "augment" the latest model of one of its iterators with
a relational fact F, producing a *new* iterator for the models that are

(a) <=-minimal under the original CNF plus F.
(b) <=-reachable from the current model.

We do all of this without re-translating, modifying the original
bounds, or losing our place in the model iterator. Instead, we
manipulate the SAT-solver.

This is all done via the augment() method of MinSolver.

As mentioned above, we made the design choice to have all these
iterators (the original, augments of the original, etc.) share a SAT4J
instance. It would also be possible to give each iterator its own
SAT4J instance, as Kodkod does. This would result in more space
consumption and more time to construct a fresh iterator, but simpler
code and faster performance otherwise. We were unsure which would be
best. When an iterator is invoked, it calls claimSATSolver(),
re-asserting its constraints and forcing the current owner of the
iterator to remove its constraints.

We deactivate symmetry-breaking entirely for the new iterator, for
the same reasons as before. (More detail on request.)

----------------------------------------