Stronger, Better, Faster: Optimally Propagating SAT Encodings

Martin Brain

Almost all applications of SAT solvers generate Boolean formulae from higher level expression graphs by encoding the semantics of each operation or relation. Non-trivial operations often have many different possible encodings and which is used use can have a major effect on the performance of the system. This talk describes our work on an abstract satisfaction based formalisation of one aspect of encoding quality, the propagation strength, which shows that optimally propagating encodings exist and can be computed for key operations. This allows a more rigorous approach to designing encodings as well as improved performance.