中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 会议论文
Title:
solving generalized optimization problems subject to smt constraints
Author: Ma Feifei ; Yan Jun ; Zhang Jian
Source: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Conference Name: 6th International Frontiers of Algorithmics Workshop, FAW 2012 and 8th International Conference on Algorithmic Aspects of Information and Management, AAIM 2012
Conference Date: May 14, 2012 - May 16, 2012
Issued Date: 2012
Conference Place: Beijing, China
Keyword: Algorithms ; Constrained optimization
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
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.
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.
Language: 英语
Content Type: 会议论文
URI: http://ir.iscas.ac.cn/handle/311060/15733
Appears in Collections:软件所图书馆_会议论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
Ma Feifei,Yan Jun,Zhang Jian. solving generalized optimization problems subject to smt constraints[C]. 见:6th International Frontiers of Algorithmics Workshop, FAW 2012 and 8th International Conference on Algorithmic Aspects of Information and Management, AAIM 2012. Beijing, China. May 14, 2012 - May 16, 2012.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Ma Feifei]'s Articles
[Yan Jun]'s Articles
[Zhang Jian]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Ma Feifei]‘s Articles
[Yan Jun]‘s Articles
[Zhang Jian]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace