Computing with SAT oracles: Past, present and future

Abstract

Boolean Satisfiability (SAT) epitomizes NP-completeness, and so what is arguably the best known class of intractable problems. NP-complete decision problems are pervasive in all areas of computing, with literally thousands of well-known examples. Nevertheless, SAT solvers routinely challenge the problem’s intractability by solving propositional formulas with millions of variables, many representing the translation from some other NP-complete or NP-hard problem. The practical effectiveness of SAT solvers has motivated their use as oracles for NP, enabling new algorithms that solve an ever-increasing range of hard computational problems. This paper provides a brief overview of this ongoing effort, summarizing some of the recent past and present main successes, and highlighting directions for future research.