Towards an Efficient Library for SAT: a Manifesto

In recent years, prepositional satisfiability (SAT) has become increasingly popular outside its traditional AI and automated reasoning niche. Applications from diverse fields require efficient and sophisticated SAT solvers that can be easily integrated into existing tools. In this paper we outline a path towards an efficient library for SAT that should meet the rising standards of research and applications. Our first milestone is SIM, a library for clausal SAT based on the well known Davis-Logemann-Loveland (DLL) method. SIM provides a choice of heuristics and optimizations that are found separately in most state-of-the-art DLL-based solvers, and extensive experimental evaluation confirms that SIMʹs generality does not hinder its performance.