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.

• Type: Conference
• Year: 2003
• Where: GLVLSI
• Authors: Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah
• Keywords: GLVLSI 2003, MINCE, MINCE Orderings, Pre-existing Min-cut Placer, VLSI