SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering

摘要

The propositional satisfiability problem (SAT) is one of the simplest instances of Constraint Programming (CP): variables are bi-valued (can only take values 0 or 1), and all constraints are clauses (disjunctions of literals) like x V (y-) V (z-) (meaning that x = 1 or y = 0 or z = 0). In spite of its simplicity, SAT has become very important for practical applications, especially in the multi-billion industry of electronic design automation (EDA), and, in general, hardware and software verification.