Sat Aug 4 13:35:06 EDT 2018



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

^ of | of (-)x_i


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


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


- 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