Paper Info
Title
Partitioning methods for satisfiability testing on large formulas
Abstract
A propositional satisfiability tester is needed as a subroutine for many applications in automated verification, automated theorem proving, and other fields. Such applications may generate very large formulas, some of which are beyond the capabilities of known algorithms. This paper investigates methods for partitioning such formulas effectively, to produce smaller formulas within the reach of known algorithms. CNF formula partitioning can be viewed as hypergraph partitioning, which has been studied extensively in VLSI design. Although CNF formulas have been considered as hypergraphs before, we found that this viewpoint was not productive for partitioning, and we introduce a new viewpoint in the dual hypergraph. Hypergraph partitioning technology from VLSI design is adapted to this problem. The overall goal of satisfiability testing requires criteria different from those used in VLSI design. Several heuristics are described, and investigated experimentally. Some formulas from circuit applications that were extremely difficult or impossible for existing algorithms have been solved. However, the method is not useful on formulas with little or no structure, such as randomly generated formulas.
Year
DOI
Venue
1996
10.1006/inco.1999.2860
Information and Computation/information and Control
Keywords
DocType
Volume
partitioning methods,large formulas,satisfiability testing,partitioning method,large formula,vlsi design,automated theorem proving,satisfiability
Conference
162
Issue
ISSN
ISBN
1-2
Information and Computation
3-540-61511-3
Citations 
PageRank 
References 
20
1.14
9
Authors
2
Name
Order
Citations
PageRank
Tai Joon Park1201.14
Allen Van Gelder23443721.45