Satisfiability Algorithms and Finite Quantification
Matthew L. Ginsberg, Andrew J. Parkes · 2000
This paper makes three observations with regard to the application of algorithms such as wsat and relsat to problems of practical interest. First, we identify a specific calculation ("subsearch") that is performed at each inference step by any existing satisfiability algorithm. We then show that for realistic problems, the time spent on subsearch can be expected to dominate the computational cost of the algorithm. Finally, we present a specific modification to the representation that exploits the structure of naturally occurring problems and leads to exponential reductions in the time needed for subsearch. 1 Introduction The last few years have seen extraordinary improvements in the effectiveness of general-purpose Boolean satisfiability algorithms. This work began with the application of wsat [Selman et al., 1996] to "practical" problems in a variety of domains (generative planning [Kautz and Selman, 1992], circuit layout, and others) by translating these problems into ...