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.