solving generalized optimization problems subject to smt constraints

ISCAS OpenIR

	solving generalized optimization problems subject to smt constraints
	Ma Feifei; Yan Jun; Zhang Jian
	2012
会议名称	6th International Frontiers of Algorithmics Workshop, FAW 2012 and 8th International Conference on Algorithmic Aspects of Information and Management, AAIM 2012
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	247-258
会议日期	May 14, 2012 - May 16, 2012
会议地点	Beijing, China
收录类别	EI
ISSN	0302-9743
ISBN	9783642296994
部门归属	(1) Institute of Software Chinese Academy of Sciences China; (2) State Key Laboratory of Computer Science China
摘要	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.
关键词	Algorithms Constrained Optimization
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15733
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Ma Feifei,Yan Jun,Zhang Jian. solving generalized optimization problems subject to smt constraints[C],2012:247-258.