research-article

Exploiting hierarchy and structure to efficiently solve graph coloring as SAT

Author:

Miroslav N. VelevAuthors Info & Claims

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

Pages 135 - 142

Published: 05 November 2007 Publication History

Abstract

Many important EDA problems can be formulated as graph coloring, which is a class of the Constraint Satisfaction Problem (CSP). This paper makes three contributions. First, we define new encodings for representing CSPs as equivalent Boolean Satisfiability (SAT) problems: 1) a generalization of the log encoding by using ITE trees to select the domain values of a CSP variable, so that only conflict clauses are required; and 2) a simplified direct encoding, derived from the direct encoding (where each domain value of a CSP variable is indexed by a unique Boolean variable) by omitting one of the Boolean variables and the at-least-one clause. Second, we propose the use of hierarchical encodings that combine several simple encodings to index the domain values of CSP variables, in order to produce SAT formulas that depend on fewer Boolean variables and are easier to solve. Third, we study schemes for static ordering of the Boolean variables in a Conjunctive Normal Form (CNF) representation of a CSP, based on the structure of the CSP graph, such that the resulting variable order is used for the decisions made by a SAT solver when evaluating the CNF. We compare 12 previously known SAT encodings for CSP with the two new encodings, as well as with 10 hybrid encodings. With symmetry-breaking constraints enforced, static variable ordering produced up to 2 orders of magnitude speedup. Additionally exploiting hierarchical encodings resulted in another order of magnitude speedup.

References

[1]

E. Amir, and S. McIlraith, "Partition-Based Logical Reasoning for First-Order and Propositional Theories," Artificial Intelligence, 2005.

[2]

P. Beame, H. Kautz, and A. Sabharwal, "Understanding the Power of Clause Learning," Int'l. Joint Conference on Artificial Intelligence (IJCAI '03), August 2003.

[3]

C. Bessière, E. Hebrard, and T. Walsh, "Local Consistencies in SAT," Conference Theory and Applications of Satisfiability Testing (SAT '06), LNCS 2919, May 2003.

[4]

P. Briggs, K. Cooper, K. Kennedy, and L. Torczon, "Coloring Heuristics for Register Allocation," Conference on Program Language Design and Implementation, 1989.

Digital Library

[5]

M. Büttner, and J. Rintanen, "Improving Parallel Planning with Constraints on the Number of Operators," Automated Planning and Scheduling (ICAPS '05), June 2005.

[6]

G. J. Chaitin, M. A. Auslander, A. K. Chandra, J. Cocke, M. E. Hopkins, and P. W. Markstein, "Register Allocation via Coloring," Computer Languages, Vol. 6, No. 1 (January 1981), pp. 47--57.

Digital Library

[7]

G. J. Chaitin, "Register Allocation and Spilling via Graph Coloring," Symposium on Compiler Construction, SIGPLAN Notices, Vol. 17, No. 6 (June 1982), pp. 98--105.

Digital Library

[8]

F. C. Chow, and J. L. Hennessy, "Register Allocation by Priority-Based Coloring," ACM SIGPLAN Symposium on Compiler Construction, 1984.

Digital Library

[9]

F. C. Chow, and J. L. Hennessy, "The Priority-Based Coloring Approach to Register Allocation," ACM Transactions on Programming Languages and Systems, Vol. 12, No. 4 (1990), pp. 501--536.

Digital Library

[10]

A. Chmeiss, and L. Sais, "About Neighborhood Substitutability in CSPs," Third Int'l Workshop on Symmetry in Constraint Satisfaction Problems, Kinsale, Ireland, 2003.

[11]

J.-D. Cho, and M. Sarrafzadeh, "Fast Approximation Algorithms on Maxcut, k-Coloring and k-Color Ordering for VLSI applications," IEEE Transactions on Computers, Vol. 47, No. 11 (November 1998).

Digital Library

[12]

O. Coudert, "Exact Coloring of Real-Life Graphs is Easy," Design Automation Conference (DAC '97), June 1997, pp. 121--126.

Digital Library

[13]

J. Culberson, Graph Coloring Page. http://www.cs.ualberta.ca/~joe/Coloring/

[14]

R. Dechter, Constraint Processing, Morgan Kaufmann Publishers, 2003.

Digital Library

[15]

J. de Kleer, "A Comparison of ATMS and CSP Techniques," 11<sup>th</sup> IJCAI. International Joint Conference on Artificial Intelligence, August 1989.

[16]

DIMACS Graph-Coloring Problems. http://mat.gsia.cmu.edu/COLOR04/

[17]

L. Drake, A. M. Frisch, I. P. Gent, and T. Walsh, "Automatically Reformulating SAT-Encoded CSPs," Workshop on Reformulating Constraint Satisfaction Problems 2002.

[18]

V. Durairaj, and P. Kalla, "Guiding CNF-SAT Search via Efficient Constraint Partitioning," Int'l Conference on Computer-Aided Design (ICCAD'04), November 2004.

Digital Library

[19]

V. Durairaj, and P. Kalla, "Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies," International Conference on Theory and Applications of Satisfiability Testing (SAT '05), LNCS 3569, June 2005, pp. 415--422.

Digital Library

[20]

M. Ernst, T. Millstein, and D. Weld, "Automatic SAT-Compilation of Planning Problems," Int'l. Joint Conference on AI, 1997.

[21]

A. Frisch, and T. Peugniez, "Solving Non-Boolean Satisfiability Problems with Stochastic Local Search," Int'l Joint Conference on Artificial Intelligence, 2001.

[22]

Z. Fu, Y. Mahajan, and S. Malik, "New features of the SAT'04 versions of zChaff," Working Notes on the SAT'04 Solver Competition, 2004.

[23]

D. Gajski, N. Dutt, A. Wu, and S. Lin, High-Level Synthesis: Introduction to Chip and System Design, Kluwer Academic Publishers, 1992.

Digital Library

[24]

M. R. Garey, and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman and Co., New York, 1979.

Digital Library

[25]

I. Gent, "Arc Consistency in SAT," European Conf. on AI, 2002.

[26]

E. Goldberg, and Y. Novikov, "BerkMin: A Fast and Robust SAT-Solver," Design, Automation, and Test in Europe, March 2002.

Digital Library

[27]

C. Haubelt, J. Teich, R. Feldmann, and B. Monien, "SAT-Based Techniques in System Synthesis," DATE '03, March 2003, pp. 1168--1169.

Digital Library

[28]

H. H. Hoos, "SAT-Encodings, Search Space Structure, and Local Search Performance," Int'l. Joint Conference on Artificial Intelligence, 1999.

Digital Library

[29]

W. N. N. Hung, X. Song, E. M. Aboulhamid, A. Kennings, and A. Coppola, "Segmented Channel Routability via Satisfiability," ACM Transactions on Design Automation of Electronic Systems (TODAES), Vol. 9, No. 4 (October 2004).

Digital Library

[30]

W. N. N. Hung, X. Song, T. Kam, L. Cheng, and G. Yang, "Routability Checking for Three-Dimensional Architectures," IEEE Transactions on VLSI Systems, Vol. 12, No. 12 (December 2004), pp. 1398--1401.

[31]

K. Iwama, and S. Miyazaki, "SAT-Variable Complexity of Hard Combinatorial Problems," IFIP World Computer Congress, 1994, pp. 253--258.

[32]

D. S. Johnson, and M. A. Trick, eds., "The Second DIMACS Implementation Challenge," DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1993. http://dimacs.rutgers.edu/Challenges

[33]

S. Kasif, "On the Parallel Complexity of Discrete Relaxation in Constraint Satisfaction Networks," Artificial Intelligence, Vol. 45, No. 3.

Digital Library

[34]

H. Kautz, and B. Selman, "Planning as Satisfiability," 10<sup>th</sup> European Conference on Artificial Intelligence (ECAI '92), August 1992.

Digital Library

[35]

H. Kautz, D. McAllester, and B. Selman, "Encoding Plans in Propositional Logic," 5<sup>th</sup> International Conference on the Principle of Knowledge Representation and Reasoning (KR '96), November 1996.

[36]

H. Kautz, and B. Selman, "Unifying SAT-based and Graph-based Planning," International Joint Conference on Artificial Intelligence (IJCAI '99), July-August 1999.

Digital Library

[37]

H. Kautz, "SATPLAN04: Planning as Satisfiability," Working Notes on the International Planning Competition (IPC '04), 2004, pp. 44--45.

[38]

H. Kautz et al., SATPLAN: Planning as Satisfiability. http://www.cs.washington.edu/homes/kautz/satplan/index.htm

[39]

D. Kirovski, and M. Potkonjak, "Efficient Coloring of a Large Spectrum of Graphs," Design Automation Conference (DAC '98), June 1998.

Digital Library

[40]

D. Le Berre, and L. Simon, "Results from the SAT'03 Solver Competition," Int'l. Conference on Theory and Applications of Satisfiability Testing (SAT '03), 2003. http://www.lri.fr/~simon/contest03/results/

[41]

S. O. Memik, and F. Fallah, "Accelerated SAT-Based Scheduling of Control/Data Flow Graphs," ICCD '02, September 2002, pp. 395--400.

Digital Library

[42]

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver," DAC '01, June 2001.

Digital Library

[43]

G.-J. Nam, F. A. Aloul, K. A. Sakallah, R. A. Rutenbar, "A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints," IEEE Transactions on Computers, Vol. 53, No. 6 (2004).

Digital Library

[44]

M. Perkowski, R. Malvi, S. Grygiel, M. Burns, and A. Mishchenko, "Graph Coloring Algorithms for Fast Evaluation of Curtis Decompositions," Design Automation Conference (DAC '99), June 1999.

Digital Library

[45]

S. D. Prestwich, "Maintaining Arc-Consistency in Stochastic Local Search," Techniques for Implementing Constraint Programming Systems, 2002.

[46]

S. D. Prestwich, "Local Search on SAT-Encoded Colouring Problems," Theory and Applications of Satisfiability Testing (SAT '03), 2003.

[47]

S. D. Prestwich, "Full Dynamic Interchangeability with Forward Checking and Arc Consistency," Workshop on Modeling and Solving Problems With Constraints, 2004.

[48]

S. D. Prestwich, "Full Dynamic Substitutability by SAT Encoding," Principles and Practice of Constraint Programming (CP '04), 2004.

[49]

S. D. Prestwich, Personal Communication, 2005.

[50]

D. Ramachandran, and E. Amir, "Compact Propositional Encodings of First-Order Theories," National Conference on AI, 2005.

Digital Library

[51]

A. Ramani, F. Aloul, I. Markov, and K. Sakallah, "Breaking Instance-Independent Symmetries in Exact Graph Coloring," Journal of Artificial Intelligence Research (JAIR), 2005.

Digital Library

[52]

S. Reda, R. Drechsler, and A. Orailoglu, "On the Relation Between SAT and BDDs for Equivalence Checking," International Symposium on Quality of Electronic Design (ISQED '02), 2002, pp. 394--399.

Digital Library

[53]

J. Rintanen, K. Heljanko, and I. Niemelä, "Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search," Technical Report 216, Institute of Computer Science, University of Freiburg, Germany, 2005.

[54]

L. Ryan, Efficient Algorithms for Clause Learning SAT Solvers, M.S. thesis, Simon Fraser University, Canada, 2004.

[55]

A. Sabharwal, P. Beame, and H. Kautz, "Using Problem Structure for Efficient Clause Learning," Theory and Applications of Satisfiability Testing (SAT '03), 2003.

[56]

B. Selman, H. Levesque, and D. Mitchell, "A New Method for Solving Hard Satisfiability Problems," AAAI '92, 1992, pp. 440--446.

[57]

N. Sherwani, Algorithms for VLSI Physical Design Automation, 3<sup>rd</sup> ed., Kluwer Academic Publishers, 1998.

Digital Library

[58]

A. Singh, M. Marek-Sadowska, "Circuit Clustering Using Graph Coloring," International Symposium on Physical Design, 1999, pp. 164--169.

Digital Library

[59]

M. D. Smith, N. Ramsey, and G. Holloway, "A Generalized Algorithm for Graph-Coloring Register Allocation," ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, 2004.

Digital Library

[60]

X. Song, W. N. N. Hung, A. Mishchenko, M. Chrzanowska-Jeske, A. Kennings, and A. Coppola, "Board-Level Multi-Terminal Net Assignment for the Partial Crossbar Architecture," IEEE Transactions on VLSI Systems, Vol. 11, No. 3 (June 2003).

Digital Library

[61]

M. Trick, Network Resources for Coloring a Graph. http://mat.gsia.cmu.edu/COLOR/color.html

[62]

A. Van Gelder, "Another Look at Graph Coloring via Propositional Satisfiability," accepted to appear in Discrete Applied Mathematics, 2005.

Digital Library

[63]

M. N. Velev, "Efficient Translation of Boolean Formulas to CNF in Formal Verification of Microprocessors," Asia and South Pacific Design Automation Conference (ASP-DAC '04), January 2004, pp. 310--315.

Digital Library

[64]

M. N. Velev, "Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors," DATE '04, February 2004, pp. 266--271.

Digital Library

[65]

M. N. Velev, "Comparative Study of Strategies for Formal Verification of High-Level Processors," ICCD '04, October 2004, pp. 119--124.

Digital Library

[66]

M. N. Velev, "Comparison of Schemes for Encoding Unobservability in Translation to SAT," ASP-DAC '05, January 2005, pp. 1056--1059.

Digital Library

[67]

T. Walsh, "Search in a Small World," Sixteenth International Joint Conference on Artificial Intelligence (IJCAI '99), T. Dean, ed., July - August 1999, pp. 1172--1177.

Digital Library

[68]

T. Walsh, "SAT v CSP," Principles and Practice of Constraint Programming, 2000.

Digital Library

[69]

H. Xu, R. A. Rutenbar, and K. A. Sakallah, "sub-SAT: A Formulation for Relaxed Boolean Satisfiability with Applications in Routing," International Symposium on Physical Design (ISPD '02), April 2002.

Digital Library

Cited By

Park DKang IKim YGao SLin BCheng CBustany ISwartz W(2019)ROADProceedings of the 2019 International Symposium on Physical Design10.1145/3299902.3309752(65-72)Online publication date: 4-Apr-2019
https://dl.acm.org/doi/10.1145/3299902.3309752
Nguyen VThang HHu ZBui MSikdar BIDE IBinh HEngchuan WSang DOanh N(2017)SAT Encodings of Finite-CSP DomainsProceedings of the 8th International Symposium on Information and Communication Technology10.1145/3155133.3155167(84-91)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3155133.3155167
Nguyen VMai SThang HPhuong LDe Raedt LDeville YBui MLinh TOanh NSang DNgoc N(2015)A New Method to Encode the At-Most-One Constraint into SATProceedings of the 6th International Symposium on Information and Communication Technology10.1145/2833258.2833293(46-53)Online publication date: 3-Dec-2015
https://dl.acm.org/doi/10.1145/2833258.2833293
Show More Cited By

Recommendations

A Hierarchy of Tractable Subclasses for SAT and Counting SAT Problems
SYNASC '09: Proceedings of the 2009 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing

Finding subclasses of formulae for which the SAT problem can be solved in polynomial time has been an important problem in computer science. We present a new hierarchy of propositional formulæ subclasses for which the SAT and counting SAT problems can ...
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 ...
Non-restarting SAT solvers with simple preprocessing can efficiently simulate resolution
AAAI'14: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence

Propositional satisfiability (SAT) solvers based on conflict directed clause learning (CDCL) implicitly produce resolution refutations of unsatisfiable formulas. The precise class of formulas for which they can produce polynomial size refutations has ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

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

November 2007

933 pages

ISBN:1424413826

General Chair:
Georges Gielen
ESAT-MICAS, Katholieke Univ. Leuven, Leuven, Belgium

Sponsors

CEDA: Council on Electronic Design Automation
SIGDA: ACM Special Interest Group on Design Automation
IEEE CASS/CANDE
IEEE-CS\DATC: IEEE Computer Society

Publisher

IEEE Press

Publication History

Published: 05 November 2007

Check for updates

Qualifiers

Research-article

Conference

ICCAD07

Sponsor:

CEDA
SIGDA
IEEE-CS\DATC

ICCAD07: The International Conference on Computer-Aided Design 2007

November 5 - 8, 2007

California, San Jose

Acceptance Rates

ICCAD '07 Paper Acceptance Rate 139 of 510 submissions, 27%;

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
356
Total Downloads

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

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Park DKang IKim YGao SLin BCheng CBustany ISwartz W(2019)ROADProceedings of the 2019 International Symposium on Physical Design10.1145/3299902.3309752(65-72)Online publication date: 4-Apr-2019
https://dl.acm.org/doi/10.1145/3299902.3309752
Nguyen VThang HHu ZBui MSikdar BIDE IBinh HEngchuan WSang DOanh N(2017)SAT Encodings of Finite-CSP DomainsProceedings of the 8th International Symposium on Information and Communication Technology10.1145/3155133.3155167(84-91)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3155133.3155167
Nguyen VMai SThang HPhuong LDe Raedt LDeville YBui MLinh TOanh NSang DNgoc N(2015)A New Method to Encode the At-Most-One Constraint into SATProceedings of the 6th International Symposium on Information and Communication Technology10.1145/2833258.2833293(46-53)Online publication date: 3-Dec-2015
https://dl.acm.org/doi/10.1145/2833258.2833293
Velev MGao PChang Y(2014)Improving the efficiency of automated debugging of pipelined microprocessors by symmetry breaking in modular schemes for boolean encoding of cardinalityProceedings of the 2014 IEEE/ACM International Conference on Computer-Aided Design10.5555/2691365.2691502(676-683)Online publication date: 3-Nov-2014
https://dl.acm.org/doi/10.5555/2691365.2691502
Nguyen VSon MGiang NThang HKhalil ISon NDeville YBui M(2014)Solving the all-interval series problemProceedings of the 5th Symposium on Information and Communication Technology10.1145/2676585.2676605(65-74)Online publication date: 4-Dec-2014
https://dl.acm.org/doi/10.1145/2676585.2676605
Velev MGao PPhillips JHu AGraeb H(2011)Automatic formal verification of multithreaded pipelined microprocessorsProceedings of the International Conference on Computer-Aided Design10.5555/2132325.2132476(679-686)Online publication date: 7-Nov-2011
https://dl.acm.org/doi/10.5555/2132325.2132476
Velev MGao PSciuto D(2008)Comparison of Boolean satisfiability encodings on FPGA detailed routing problemsProceedings of the conference on Design, automation and test in Europe10.1145/1403375.1403682(1268-1273)Online publication date: 10-Mar-2008
https://dl.acm.org/doi/10.1145/1403375.1403682

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.

Figures

Tables

Media

View Table of Conten