Institutional Repository
| An Efficient Approach for Solving Optimization over Linear Arithmetic Constraints | |
Chen, L; Wu, JZ; Lv, YR ; Wang, YJ
| |
| 2016 | |
| Source | JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY
 |
| ISSN | 1000-9000 |
| Volume | 31Issue:5Pages:987-1011 |
| English Abstract | Satisfiability Modulo Theories (SMT) have been widely investigated over the last decade. Recently researchers have extended SMT to the optimization problem over linear arithmetic constraints. To the best of our knowledge, Symba and OPT-MathSAT are two most efficient solvers available for this problem. The key algorithms used by Symba and OPT-MathSAT consist of the loop of two procedures: 1) critical finding for detecting a critical point, which is very likely to be globally optimal, and 2) global checking for confirming the critical point is really globally optimal. In this paper, we propose a new approach based on the Simplex method widely used in operation research. Our fundamental idea is to find several critical points by constructing and solving a series of linear problems with the Simplex method. Our approach replaces the algorithms of critical finding in Symba and OPT-MathSAT, and reduces the runtime of critical finding and decreases the number of executions of global checking. The correctness of our approach is proved. The experiment evaluates our implementation against Symba and OPT-MathSAT on a critical class of problems in real-time systems. Our approach outperforms Symba on 99.6% of benchmarks and is superior to OPT-MathSAT in large-scale cases where the number of tasks is more than 24. The experimental results demonstrate that our approach has great potential and competitiveness for the optimization problem.; Satisfiability Modulo Theories (SMT) have been widely investigated over the last decade. Recently researchers have extended SMT to the optimization problem over linear arithmetic constraints. To the best of our knowledge, Symba and OPT-MathSAT are two most efficient solvers available for this problem. The key algorithms used by Symba and OPT-MathSAT consist of the loop of two procedures: 1) critical finding for detecting a critical point, which is very likely to be globally optimal, and 2) global checking for confirming the critical point is really globally optimal. In this paper, we propose a new approach based on the Simplex method widely used in operation research. Our fundamental idea is to find several critical points by constructing and solving a series of linear problems with the Simplex method. Our approach replaces the algorithms of critical finding in Symba and OPT-MathSAT, and reduces the runtime of critical finding and decreases the number of executions of global checking. The correctness of our approach is proved. The experiment evaluates our implementation against Symba and OPT-MathSAT on a critical class of problems in real-time systems. Our approach outperforms Symba on 99.6% of benchmarks and is superior to OPT-MathSAT in large-scale cases where the number of tasks is more than 24. The experimental results demonstrate that our approach has great potential and competitiveness for the optimization problem. |
| Indexed Type | SCI |
| Keyword | Constrained Optimization Satisfiability Modulo Theories Linear Programming |
| Department | Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing 100190, Peoples R China. Univ Chinese Acad Sci, Beijing 100190, Peoples R China. Chinese Acad Sci, Inst Software, Natl Engn Res Ctr Fundamental Software, Beijing 100190, Peoples R China. |
| Language | 英语 |
| WOS ID | WOS:000383055100009 |
| Citation statistics | |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/17303 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Chen, L,Wu, JZ,Lv, YR,et al. An Efficient Approach for Solving Optimization over Linear Arithmetic Constraints[J]. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY,2016,31(5):987-1011. |
| APA | Chen, L,Wu, JZ,Lv, YR,&Wang, YJ.(2016).An Efficient Approach for Solving Optimization over Linear Arithmetic Constraints.JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY,31(5),987-1011. |
| MLA | Chen, L,et al."An Efficient Approach for Solving Optimization over Linear Arithmetic Constraints".JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY 31.5(2016):987-1011. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| art%3A10.1007%2Fs113（4198KB） | 开放获取 | License | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment