Satisfiability Algorithms and Finite Quantification

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.

• Type: Conference
• Year: 2000
• Where: KR
• Authors: Matthew L. Ginsberg, Andrew J. Parkes
• Keywords: Automated Reasoning, KR 2000, Realistic Problems, Satisfiability Algorithm, Specific Calculation