[<<][sat][>>][..]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

[Reply][About]

[<<][sat][>>][..]