Partitioning methods for satisfiability testing on large formulas

被引:6
|
作者
Park, TJ [1 ]
Van Gelder, A [1 ]
机构
[1] Univ Calif Santa Cruz, Dept Comp Sci, Santa Cruz, CA 95064 USA
基金
美国国家科学基金会;
关键词
D O I
10.1006/inco.1999.2860
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Methods for partitioning large propositional formulas are investigated, with the goal of producing a set of smaller formulas whose satisfiability can be determined within reasonable time frames by 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. (C) 2000 Academic Press.
引用
收藏
页码:179 / 184
页数:6
相关论文
共 50 条