SAT Solvers

Entry: SAT / SMT
Date: Sat Aug  4 13:35:06 EDT 2018

SAT

First: how to specify a problem?  Conjunctive Normal Form (CNF).

^ of | of (-)x_i

https://www.dwheeler.com/essays/minisat-user-guide.html


Main question: is it possible to put opaque boolean functions in
there?  I guess the whole idea is to be able to use the structure of
the function to perform the search, so likely not.

That means the problem needs to be translated into CNF.

E.g. a+b=c

To encode it, implement an adder?

Let's try this:

a+b=2, for a,b 2-bit values

https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/

"Many research papers have been written about the efficient encoding
of specific constraints and other gadgets"



https://yurichev.com/writings/SAT_SMT_by_example.pdf

- Uses one-hot encoding.

- SMT vs. SAT: SMT-solvers are frontends to SAT solvers (bit blasting)

- SMT vs. SAT is like high level PL vs. assembly language. The latter
  can be much more efficient, but it’s hard to program in it.

- z3 is used in the notes.  http://hackage.haskell.org/package/z3

- SMT-LIB spec language is s-expressions



Entry: How to use a SMT, SAT solver?
Date: Sun Sep 16 11:29:07 EDT 2018

- 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
  intuitions.

- 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.