Chapter 2 Satisfiability Solvers

摘要: Publisher Summary The past few years have seen enormous progress in the performance of Boolean satisfiability (SAT) solvers. Despite worst-case exponential run time all known algorithms, solvers are increasingly leaving their mark as a general-purpose tool areas diverse software and hardware verification, automatic test-pattern generation, planning, scheduling, even challenging problems from algebra. Annual SAT competitions led to development dozens clever implementations such solvers, exploration new techniques, creation an extensive suite real-world instances well hand-crafted benchmark problems. Modern provide black-box procedure that can often solve hard structured with over million variables several constraints. This chapter describes main solution techniques used modern classifying them complete incomplete methods. It discusses recent insights explaining effectiveness these on practical encodings presents extensions approach currently under development. These further expand range applications include multiagent probabilistic reasoning.