Exploiting hierarchy and structure to efficiently solve graph coloring as SAT

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.