Institutional Repository
| solving generalized optimization problems subject to smt constraints | |
| Ma Feifei; Yan Jun; Zhang Jian | |
| 2012 | |
| Conference Name | 6th International Frontiers of Algorithmics Workshop, FAW 2012 and 8th International Conference on Algorithmic Aspects of Information and Management, AAIM 2012 |
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 247-258 |
| Conference Date | May 14, 2012 - May 16, 2012 |
| Conference Place | Beijing, China |
| Indexed Type | EI |
| ISSN | 0302-9743 |
| ISBN | 9783642296994 |
| Department | (1) Institute of Software Chinese Academy of Sciences China; (2) State Key Laboratory of Computer Science China |
| English Abstract | In a classical constrained optimization problem, the logical relationship among the constraints is normally the logical conjunction. However, in many real applications, the relationship among the constraints might be more complex. This paper investigates a generalized class of optimization problems whose constraints are connected by various kinds of logical operators in addition to conjunction. Such optimization problems have been rarely studied in literature in contrast to the classical ones. A framework which integrates classical optimization procedures into the DPLL(T) architecture for solving Satisfiability Modulo Theories (SMT) problems is proposed. Two novel techniques for improving the solving efficiency w.r.t. linear arithmetic theory are also presented. Experiments show that the proposed techniques are quite effective. © 2012 Springer-Verlag.; In a classical constrained optimization problem, the logical relationship among the constraints is normally the logical conjunction. However, in many real applications, the relationship among the constraints might be more complex. This paper investigates a generalized class of optimization problems whose constraints are connected by various kinds of logical operators in addition to conjunction. Such optimization problems have been rarely studied in literature in contrast to the classical ones. A framework which integrates classical optimization procedures into the DPLL(T) architecture for solving Satisfiability Modulo Theories (SMT) problems is proposed. Two novel techniques for improving the solving efficiency w.r.t. linear arithmetic theory are also presented. Experiments show that the proposed techniques are quite effective. © 2012 Springer-Verlag. |
| Keyword | Algorithms Constrained Optimization |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15733 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Ma Feifei,Yan Jun,Zhang Jian. solving generalized optimization problems subject to smt constraints[C],2012:247-258. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment