Sun Sep 16 11:29:07 EDT 2018

How to use a SMT, SAT solver?

- The model is the bridge between a solution of the SAT,SMT problem,
  and the actual problem you're facing.  Building this model is
  everything, and it seems this requires a whole new set of

- Just sitting down and writing down constraints and variables exposes
  a lot of "variables" that do not vary at all, e.g. they are just
  extra constraints, or can disappear completely into implicit
  properties of the encoding.  Gradually, your problem translates into
  something that resembles a SAT/SMT problem.

- Similarly, sometimes the problem is "triangular".  There are a
  couple of constraints, but they can be solved sequentially, similar
  to solving triangular linear systems.  This allows a part of the
  problem to be solved by hand, allowing a problem transformation to
  reduce the parameter/constraint set.

- There seems to be a sweet spot, trading off a more complex encoding
  vs. a simpler encoding with some more constraints.  Even if further
  reduction of the description is possible, the time to do so is
  longer than encoding and running the solver for the larger problem.