Article

Faster SAT and smaller BDDs via common function structure

Authors:

Igor L. Markov,

Karem A. SakallahAuthors Info & Claims

ICCAD '01: Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design

Pages 443 - 448

Published: 04 November 2001 Publication History

Abstract

The increasing popularity of SAT and BDD techniques in verification and synthesis encourages the search for additional speed-ups. Since typical SAT and BDD algorithms are exponential in the worst-case, the structure of real-world instances is a natural source of improvements. While SAT and BDD techniques are often presented as mutually exclusive alternatives, our work points out that both can be improved via the use of the same structural properties of instances. Our proposed methods are based on efficient problem partitioning and can be easily applied as pre-processing with arbitrary SAT solvers and BDD packages without source code modifications.Finding a better variable-ordering is a well recognized problem for both SAT solvers and BDD packages. Currently, all leading edge variable-ordering algorithms are dynamic, in the sense that they are invoked many times in the course of the "host" algorithm that solves SAT or manipulates BDDs. Examples include the DLCS ordering for SAT solvers and variable-sifting during BDD manipulations. In this work we propose a universal variable-ordering MINCE (MIN Cut Etc.) that pre-processes a given Boolean formula in CNF. MINCE is completely independent from target algorithms and outperforms both DLCS for SAT and variable sifting for BDDs. We argue that MINCE tends to capture structural properties of Boolean functions arising from real-world applications. Our contribution is validated on the ISCAS circuits and the DIMACS benchmarks. Empirically, our technique often outperforms existing techniques by a factor of two or more. Our results motivate search for stronger dynamic ordering heuristics and combined static/dynamic techniques.

References

[1]

C. Berman, "Circuit Width, Register Allocation, and Ordered Binary Decision Diagrams," in IEEE Transactions on Computer Aided Design, 10(8), 1991.

[2]

A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, "Symbolic Model Checking using SAT procedures instead of BDDs," in Proc. of the Design Automation Conference (DAC), 1999.

Digital Library

[3]

F. Brglez, D. Bryan, and K. Kozminski, "Combinational problems of sequential benchmark circuits," in Proc. of the International Symposium on Circuits and Systems, 1989.

[4]

R. Bryant, "Graph-based algorithms for Boolean function manipulation," in IEEE Transactions on Computers, 35(8), 1986.

Digital Library

[5]

A. Caldwell, A. Kahng, and I. Markov, "Can Recursive Bisection Produce Routable Placements?" in Proc. of the Design Automation Conference (DAC), 2000.

Digital Library

[6]

A. Caldwell, A. Kahng, and I. Markov, "Improved Algorithms for Hypergraph Bipartitioning," in Proc. of the IEEE ACM Asia and South Pacific Design Automation Conference, 2000.

Digital Library

[7]

R. Drechsler and B. Becker, "Binary Decision Diagrams, Theory and Implementation," Kluwer Academic Publishers, 1998.

[8]

DIMACS Challenge benchmarks in ftp://Dimacs.rutgers.EDU/pub/challenge/sat/benchmarks/cnf.

[9]

M. Fujita, H. Fujisawa, and N. Kawato, "Evaluation and Improvements of Boolean Comparison Method Based on Binary Decision Diagrams," in Proc. of the International Conference on Computer Aided Design (ICCAD), 1988.

[10]

C. Gomes, B. Selman, and H. Kautz, "Boosting Combinatorial Search Through Randomization," in Proc. of the National Conference on Artificial Intelligence (AAAI), 1998.

Digital Library

[11]

G. Hachtel and F. Somenzi, "Logic Synthesis and Verification Algorithms," Kluwer Academic Publishers, 3rd edition, 2000.

Digital Library

[12]

S. Hur and J. Lillis, "Relaxation and clustering in a local search framework: application to linear placement," in Proc. of the Design Automation Conference (DAC), 1999.

Digital Library

[13]

G. Janssen, "Design of a Pointerless BDD Package," in International Workshop on Logic Synthesis (IWLS), 2001.

[14]

G. Karypis, R. Aggarwal, V. Kumar, and S. Shekhar, "Multilevel Hypergraph Partitioning: Applications in VLSI Design," in Proc. of the Design Automation Conference (DAC), 1997.

Digital Library

[15]

T. Larrabee, "Test Pattern Generation Using Boolean Satisfiability," IEEE Transactions on Computer-Aided Design, 11(1), 1992.

Digital Library

[16]

Y. Lu, J. Jain, and K. Takayama, "BDD Variable Ordering Using Window-based Sampling," in International Workshop on Logic Synthesis (IWLS), 2000.

[17]

S. Malik, A. Wang, R. Brayton, and A. Sangiovanni-Vincentelli, "Logic Verification using Binary Decision Diagrams in a Logic Synthesis Environment," in Proc. of the International Conference on Computer Aided Design (ICCAD), 1988.

[18]

M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver," in Proc. of the Design Automation Conference (DAC), 2001.

Digital Library

[19]

G. Nam, F. Aloul, K. Sakallah, and R. Rutenbar, "A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints," in Proc. of the International Symposium on Physical Design (ISPD), 2001.

Digital Library

[20]

S. Panda and F. Somenzi, "Who are the variables in your neighborhood," in Proc. of the International Conference on Computer Aided Design (ICCAD), 1995.

Digital Library

[21]

M. Prasad, P. Chong, and K. Keutzer, "Why is ATPG easy?" in Proc. of the Design Automation Conference (DAC), 1999.

Digital Library

[22]

R. Rudell, "Dynamic variable ordering for ordered binary decision diagrams," in Proc. of the International Conference on Computer Aided Design (ICCAD), 1993.

Digital Library

[23]

J. Silva and K. Sakallah, "GRASP-A New Search Algorithm for Satisfiability," in Proc. of the International Conference on Computer Aided Design (ICCAD), 1996.

Digital Library

[24]

L. Silva, J. Silva, L. Silveira, and K. Sakallah, "Timing Analysis Using Propositional Satisfiability," in IEEE International Conference on Electronics, Circuits and Systems, 1998.

[25]

F. Somenzi, "Colorado University Decision Diagram package (CUDD)," http://vlsi.colorado.edu/~fabio/CUDD, 1997.

[26]

G. Stalmarck, "System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from Boolean Formula," United States Patent no. 5,276,897, 1994.

[27]

P. R. Stephan, R. K. Brayton, and A. L. Sangiovanni-Vincentelli, "Combinational Test Generation Using Satisfiability," in IEEE Transactions on Computer-Aided Design, 1996.

Digital Library

[28]

D. Wang and E. Clarke, "Efficient Formal Verification through Cutwidth," unpublished manuscript, 2001.

[29]

R. Wood and R. Rutenbar, "FPGA Routing and Routability Estimation Via Boolean Satisfiability," in IEEE Transactions on VLSI, 6(2), 1998.

Digital Library

[30]

H. Zhang, "SATO: An Efficient Propositional Prover," in International Conference on Automated Deduction, 1997.

Digital Library

Cited By

Brauer JKing AKriener J(2011)Existential quantification as incremental SATProceedings of the 23rd international conference on Computer aided verification10.5555/2032305.2032322(191-207)Online publication date: 14-Jul-2011
https://dl.acm.org/doi/10.5555/2032305.2032322
Mantadelis TJanssens G(2010)Variable compression in ProbLogProceedings of the 17th international conference on Logic for programming, artificial intelligence, and reasoning10.5555/1928380.1928416(504-518)Online publication date: 10-Oct-2010
https://dl.acm.org/doi/10.5555/1928380.1928416
Huang JDarwiche A(2007)The language of searchJournal of Artificial Intelligence Research10.5555/1622606.162261329:1(191-219)Online publication date: 1-Jun-2007
https://dl.acm.org/doi/10.5555/1622606.1622613
Show More Cited By

Index Terms

Faster SAT and smaller BDDs via common function structure
1. General and reference
  1. Cross-computing tools and techniques
    1. Performance
2. Hardware

Recommendations

Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

We first introduce Abstract DPLL, a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason ...
Generating SAT instances with community structure

Nowadays, modern SAT solvers are able to efficiently solve many industrial, or real-world, SAT instances. However, the process of development and testing of new SAT solving techniques is conditioned to the finite and reduced number of known industrial ...
Clause elimination for SAT and QSAT

The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '01: Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design

November 2001

656 pages

ISBN:0780372492

Conference Chair:
Rolf Ernst
Tech. Univ. of Braunschweig, Braunschweig, Germany

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE Circuits & Systems Society
The IEEE Computer Society DATC

Publisher

IEEE Press

Publication History

Published: 04 November 2001

Check for updates

Qualifiers

Article

Conference

ICCAD01

Sponsor:

SIGDA

ICCAD01: International Conference on Computer Aided Design

November 4 - 8, 2001

California, San Jose

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
268
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Brauer JKing AKriener J(2011)Existential quantification as incremental SATProceedings of the 23rd international conference on Computer aided verification10.5555/2032305.2032322(191-207)Online publication date: 14-Jul-2011
https://dl.acm.org/doi/10.5555/2032305.2032322
Mantadelis TJanssens G(2010)Variable compression in ProbLogProceedings of the 17th international conference on Logic for programming, artificial intelligence, and reasoning10.5555/1928380.1928416(504-518)Online publication date: 10-Oct-2010
https://dl.acm.org/doi/10.5555/1928380.1928416
Huang JDarwiche A(2007)The language of searchJournal of Artificial Intelligence Research10.5555/1622606.162261329:1(191-219)Online publication date: 1-Jun-2007
https://dl.acm.org/doi/10.5555/1622606.1622613
Torta GTorasso P(2007)An on-line approach to the computation and presentation of preferred diagnoses for dynamic systemsAI Communications10.5555/1365518.136552620:2(93-116)Online publication date: 1-Apr-2007
https://dl.acm.org/doi/10.5555/1365518.1365526
Torasso PTorta G(2006)Model-Based diagnosis through OBDD compilationReasoning, Action and Interaction in AI Theories and Systems10.5555/2124265.2124281(287-305)Online publication date: 1-Jan-2006
https://dl.acm.org/doi/10.5555/2124265.2124281
Huang JDarwiche A(2005)DPLL with a traceProceedings of the 19th international joint conference on Artificial intelligence10.5555/1642293.1642318(156-162)Online publication date: 30-Jul-2005
https://dl.acm.org/doi/10.5555/1642293.1642318
Huang JDarwiche A(2005)On compiling system models for faster and more scalable diagnosisProceedings of the 20th national conference on Artificial intelligence - Volume 110.5555/1619332.1619382(300-306)Online publication date: 9-Jul-2005
https://dl.acm.org/doi/10.5555/1619332.1619382
Huang JTang T(2005)MUPProceedings of the 2005 Asia and South Pacific Design Automation Conference10.1145/1120725.1120907(432-437)Online publication date: 18-Jan-2005
https://dl.acm.org/doi/10.1145/1120725.1120907
Motter DRoy JMarkov I(2005)Resolution cannot polynomially simulate compressed-BFSAnnals of Mathematics and Artificial Intelligence10.1007/s10472-004-8427-244:1-2(121-156)Online publication date: 1-May-2005
https://dl.acm.org/doi/10.1007/s10472-004-8427-2
Velev M(2004)Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of MicroprocessorsProceedings of the conference on Design, automation and test in Europe - Volume 110.5555/968878.969033Online publication date: 16-Feb-2004
https://dl.acm.org/doi/10.5555/968878.969033
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents