On Modern Clause-Learning Satisfiability Solvers

摘要

In this paper, we present a perspective on modern clause-learning SAT solvers that highlights the roles of, and the interactions between, decision making and clause learning in these solvers. We discuss two limitations of these solvers from this perspective and discuss techniques for dealing with them. We show empirically that the proposed techniques significantly improve state-of-the-art solvers.