As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
Over the last two decades, we have witnessed a silent revolution in software engineering thanks in part to Boolean SAT and SMT solvers. These tools have made it significantly easier to design, build, and maintain myriad kinds of program analysis, testing, synthesis and verification systems. Further, they have enabled new software engineering methods that were otherwise deemed infeasible. In these lecture notes, we provide an introductory overview of SAT and SMT solvers, from both practical as well as theoretical points of view. Specifically, we describe in detail the architecture of the DPLL, CDCL, and SMT algorithms. Further, we provide theoretical understanding of these solvers through the lens of proof complexity. Finally, we showcase the power of machine learning techniques to fundamentally transform solver design.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.