Synthesis of domain specific CNF encoders for bit-vector solvers

SMT solvers are at the heart of a number of software engineering tools. These SMT solvers use a SAT solver as the back-end and convert the high-level constraints given by the user down to low-level boolean formulas that can be efficiently mapped to CNF clauses and fed into a SAT solver. Current SMT solvers are designed to be general purpose solvers that are suited to a wide range of problems. However, SAT solvers are very non-deterministic and hence, it is difficult to optimize a general purpose solver across all different problems. In this thesis, we propose a system that can automatically generate parts of SMT solvers in a way that is tailored to particular problem domains. In particular, we target the translation from high-level constraints to CNF clauses which is one of the crucial parts of all SMT solvers. We achieve this goal by using a combination of program synthesis and machine learning techniques. We use a program synthesis tool called Sketch to generate optimal encoding rules for this translation and then use auto-tuning to only select the subset of these encodings that actually improve the performance for a particular class of problems. Using this technique, the thesis shows that we can improve upon the basic encoding strategy used by CVC4 (a state of the art SMT solver). We can automatically generate variants of the solver tailored to different domains of problems represented in the bit-vector benchmark suite from the SMT competition 2015.

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2016

Author dc:creator

• Inala, Jeevana Priya

Advisor dc:contributor.advisor

• Armando Solar-Lezama.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/106008

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/106008