This paper presents a Boolean SAT constraint satisfaction formulation of the detailed placement problem for programmable logic. The detailed placement problem is usually considered a poor candidate for a SAT-based solution due to complex timing constraints and the large size of the problem space. To overcome these challenges, we encode domain-specific knowledge into the problem formulation and add new features to the SAT solver. First, a Boolean encoding of timing constraints is presented that utilizes concepts from static timing analysis. Second, future cost clauses are added to the formulation to guide the SAT solver in a manner similar to A*search. Third, a dynamic clause generation approach is described that keeps the working problem size small by adding clauses on demand as the SAT solver explores the problem space. This includes dynamic cardinality clauses and dynamic addition of literals to cardinality clauses. © 2013 Springer-Verlag.
CITATION STYLE
Mihal, A., & Teig, S. (2013). A constraint satisfaction approach for programmable logic detailed placement. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7962 LNCS, pp. 208–223). https://doi.org/10.1007/978-3-642-39071-5_16
Mendeley helps you to discover research relevant for your work.