Sciweavers

GLVLSI
2003
IEEE

FORCE: a fast and easy-to-implement variable-ordering heuristic

14 years 16 days ago
FORCE: a fast and easy-to-implement variable-ordering heuristic
The MINCE heuristic for variable-ordering [1] successfully reduces the size of BDDs and can accelerate SAT-solving. Applications to reachability analysis have also been successful [12]. The main drawback of MINCE is its implementation complexity - the authors used a pre-existing min-cut placer [6] that is several times larger than any existing SAT solver. Tweaking MINCE is difficult. In this work we propose a replacement heuristic, FORCE which is easy to implement from scratch and tweak. It is dramatically faster than MINCE in practice. While FORCE may produce seemingly inferior variable orderings, the difference with MINCE orderings does not affect subsequent SAT-solving. Categories and Subject Descriptors I.1 [Symbolic and Algebraic Manipulation]: Algorithms. General Terms Algorithms, Performance, Experimentation, Verification. Keywords BDDs, SAT, CNF, backtrack search, variable order, pre-processing, hypergraph, partitioning, placement.
Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
Added 04 Jul 2010
Updated 04 Jul 2010
Type Conference
Year 2003
Where GLVLSI
Authors Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
Comments (0)