TY - GEN
T1 - Using higher levels of abstraction for solving optimization problems by Boolean Satisfiability
AU - Wille, Robert
AU - Große, Daniel
AU - Soeken, Mathias
AU - Drechsler, Rolf
PY - 2008
Y1 - 2008
N2 - Optimization problems can be solved using Boolean Satisfiability by mapping them to a sequence of decision problems. Therefore, in the last years several encodings have been developed. Independently, also new solvers have been introduced lifting Boolean Satisfiability to higher levels of abstraction, e.g. SAT Modulo Theories (SMT) solvers and word level solvers. Both support bit-vector logic and thus allow more compact encodings of the problems. In this paper we investigate the efficiency of these new solver paradigms applied to optimization problems. We show for two case studies - graph coloring and exact synthesis of reversible logic - that the resulting problem instances can be reduced with respect to the size. In addition for the synthesis problem significant run-time improvements can be achieved.
AB - Optimization problems can be solved using Boolean Satisfiability by mapping them to a sequence of decision problems. Therefore, in the last years several encodings have been developed. Independently, also new solvers have been introduced lifting Boolean Satisfiability to higher levels of abstraction, e.g. SAT Modulo Theories (SMT) solvers and word level solvers. Both support bit-vector logic and thus allow more compact encodings of the problems. In this paper we investigate the efficiency of these new solver paradigms applied to optimization problems. We show for two case studies - graph coloring and exact synthesis of reversible logic - that the resulting problem instances can be reduced with respect to the size. In addition for the synthesis problem significant run-time improvements can be achieved.
UR - http://www.scopus.com/inward/record.url?scp=51849091482&partnerID=8YFLogxK
U2 - 10.1109/ISVLSI.2008.82
DO - 10.1109/ISVLSI.2008.82
M3 - Conference contribution
AN - SCOPUS:51849091482
SN - 9780769531700
T3 - Proceedings - IEEE Computer Society Annual Symposium on VLSI: Trends in VLSI Technology and Design, ISVLSI 2008
SP - 411
EP - 416
BT - Proceedings - IEEE Computer Society Annual Symposium on VLSI
T2 - IEEE Computer Society Annual Symposium on VLSI: Trends in VLSI Technology and Design, ISVLSI 2008
Y2 - 7 April 2008 through 9 April 2008
ER -