Jat SMT Solver

The Jat SMT solver is a 100% Java SMT solver which will compete in the QF_RDL
category only.  The solver is developed by Scott Cotton at Verimag, under the
supervision of Oded Maler (also at Verimag).

The architecture of Jat can be described roughly as lazily eager.  Like other
lazy approaches, the solver falls in the framework of a modern DPLL
propositional satisfiability solver, only Jat interprets the propositions in
the framework of the background theory as the DPLL search develops a partial
truth assignment.  The solver moreover performs exhaustive theory propagation.
In this sense, the solver is quite "eager"; however, Jat performs this theory
propagation lazily, in particular only when no unit propagation is possible
under the current truth assignment.  This feature retains the benefits of
exhaustive theory propagation but reduces its cost by avoiding it whenever
possible.  At the same time, Jat does perform consistency checks on 
all partial assignments.

For difference logic, Jat uses a fairly sophisticated approach which combines 
consistency checks and theory propagation in a way that is asymptotically 
faster than performing full theory propagation without consistency checks. 
As difference logic consistency checking and propagation boils down to 
shortest paths problems, this combination can be seen as an application of 
the principle behind Johnson's algorithm for solving all pairs shortest path
problems with arbitrary edge weights.  In particular, one single source
shortest path solution can speed up the all pairs shortest paths by using the
single source distances to produce alternate, non-negative edge weights.  This
restriction on edge weights leads to the possibility of using faster methods
for solving the all pairs problem.  When translated to differnce logic, this
property says that one satisfying assignment can speed up theory propagation. 
When in addition we apply the result that incremental consistency checking can
be formed in O(m + n log n) time (m=number of difference constraints, n=number
of variables),  we arrive at a near O(m + n log n) method of performing full 
theory propagation.

Jat will only participate in QF_RDL category of SMT-COMP'06.  Nevertheless, 
the software architecture has a well defined Java interface for a theory 
and we have successfully plugged in alternate theories.   Hopefully in the
near future we will have adequately mature theories for linear real arithmetic
and Nelson-Oppen combination.  Alas, these features didn't make it to
SMT-COMP'06. 

We expect that Jat will perform fairly well on QF_RDL problems which are
strongly numerically constrained and atleast fairly difficult, but that it will
fall well short of the optimized natively-compiled solvers implemented in lower
level languages such as C when applied to problems which are strongly
propositionally constrained (eg fisher protocol verification).