›› 2016, Vol. 31 ›› Issue (5): 987-1011.doi: 10.1007/s11390-016-1675-x

Special Issue: Theory and Algorithms

• Theory and Algorithms • Previous Articles     Next Articles

An Efficient Approach for Solving Optimization over Linear Arithmetic Constraints

Li Chen, Jing-Zheng Wu, Yin-Run Lv, and Yong-Ji Wang*, Senior Member, CCF   

  1. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China University of Chinese Academy of Sciences, Beijing 100190, China;
    National Engineering Research Center of Fundamental Software, Institute of Software Chinese Academy of Sciences Beijing 100190, China
  • Received:2015-04-02 Revised:2015-12-08 Online:2016-09-05 Published:2016-09-05
  • Contact: Yong-Ji Wang E-mail:ywang@itechs.iscas.ac.cn
  • About author:Li Chen is currently a Ph.D. student at the Institute of Software, Chinese Academy of Sciences, Beijing. He received his B.S. degree in mathematics from the University of Science and Technology of China, Hefei. His primary research interests include satisfiability modulo theories (SMT), constrained optimization, real-time systems, and robotics.
  • Supported by:

    This work is supported by the National Natural Science Foundation of China under Grant No. 61170072, and the Chinese Academy of Sciences/State Administration of Foreign Experts Affairs (CAS/SAFEA) International Partnership Program for Creative Research Teams.

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.

[1] Barrett CW, Sebastiani R, Seshia S A, Tinelli C. Satisfiability modulo theories. In Handbook of Satisfiability: Volume 185 of Frontiers in Artificial Intelligence and Applications, Biere A, Heule M J H, Van Maaren H and Walsh T (eds.), IOS Press, 2009, pp.825-885.

[2] Nelson G, Oppen D C. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 1979, 1(2): 245-257.

[3] Armando A, Castellini C, Giunchiglia E. SAT-based procedures for temporal reasoning. In Proc. the 5th European Conference on Planning on Recent Advances in AI Planning, September 1999, pp.97-108.

[4] Audemard G, Bertoli P, Cimatti A, Kornilowicz A, Sebastiani R. A SAT based approach for solving formulas over Boolean and linear mathematical propositions. In Proc. the 18th Int. Conf. Automated Deduction, July 2002, pp.195-210.

[5] Armando A, Ranise S, Rusinowitch M. A rewriting approach to satisfiability procedures. Information and Computation, 2003, 183(2): 140-164.

[6] Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(t). Journal of the ACM, 2006, 53(6): 937-977.

[7] De Moura L, Bjørner N. Satisfiability modulo theories: Introduction and applications. Communications of the ACM, 2011, 54(9): 69-77.

[8] Cimatti A, Griggio A, Schaafsma B J, Sebastiani R. The MathSAT5 SMT solver. In Proc. the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, March 2013, pp.93-107.

[9] Barrett C, Conway C L, Deters M, Hadarean L, Jovanovi? D, King T, Reynolds A, Tinelli C. CVC4. In Proc. the 23rd International Conference on Computer Aided Verification, July 2011, pp.171-177.

[10] De Moura L, Bjørner N. Z3: An efficient SMT solver. In Proc. the Theory and Practice of Software, and the 14th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, March 29-April 6, 2008, pp.337-340.

[11] Bjørner N, De Moura L. Z310: Applications, enablers, challenges and directions. In Proc. the 6th International Workshop on Constraints in Formal Verification, June 2009.

[12] de Moura L, Bjørner N. Satisfiability modulo theories: An appetizer. In Proc. the 12th Brazilian Symposium on Formal Methods, August 2009, pp.23-36.

[13] Li Y, Albarghouthi A, Kincaid Z, Gurfinkel A, Chechik M. Symbolic optimization with SMT solvers. In Proc. the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2014, pp.607-618.

[14] Sebastiani R, Tomasi S. Optimization in SMT with LA(Q) cost functions. In Proc. the 6th International Joint Conference on Automated Reasoning, June 2012, pp.484-498.

[15] Ma F, Yan J, Zhang J. Solving generalized optimization problems subject to SMT constraints. In Proc. the Joint Int. Conf. Frontiers in Algorithmics and Algorithmic Aspects in Information and Management, May 2012, pp.247-258.

[16] Dantzig G B. Linear Programming and Extensions. Princeton University Press, Princeton, NJ, USA, 1965.

[17] Byrd R H, Gilbert J C, Nocedal J. A trust region method based on interior point techniques for nonlinear programming. Mathematical Programming, 2000, 89(1): 149-185.

[18] Byrd R H, Hribar M E, Nocedal J. An interior point algorithm for large-scale nonlinear programming. SIAM Journal on Optimization, 1999, 9(4): 877-900.

[19] Han S P. A globally convergent method for nonlinear programming. Journal of Optimization Theory and Applications, 1977, 22(3): 297-309.

[20] Powell M J. Algorithms for nonlinear constraints that use lagrangian functions. Mathematical Programming, 1978, 14(1): 224-248.

[21] Min-Allah N, Khan S U, Wang Y. Optimal task execution times for periodic tasks using nonlinear constrained optimization. The Journal of Supercomputing, 2012, 59(3): 1120-1138.

[22] Dutertre B, de Moura L. A fast linear-arithmetic solver for DPLL(T). In Proc. the 18th International Conference on Computer Aided Verification, August 2006, pp.81-94.

[23] Tseitin G S. On the complexity of derivation in propositional calculus. In Automation of Reasoning, Siekmann J H, Wrightson G (eds.), Springer, 1983, pp.466-483.

[24] Kopetz H. Real-Time Systems: Design Principles for Distributed Embedded Applications (2nd edition). Springer, New York, USA, 2011.

[25] Mall R. Real-Time Systems: Theory and Practice (1st edition). Upper Saddle River, NJ, USA: Prentice Hall Press, 2007.

[26] Liu C L, Layland J W. Scheduling algorithms for multiprogramming in a hard-real-time environment. Journal of the ACM, 1973, 20(1): 46-61.

[27] Chung J Y, Liu J W S, Lin K J. Scheduling periodic jobs that allow imprecise results. IEEE Transactions on Computers, 1990, 39(9): 1156-1174.

[28] Liu J W, Lin K J, Shih W K, Yu A C, Chung J Y, Zhao W. Algorithms for scheduling imprecise computations. Computer, 1991, 24(5): 58-68.

[29] Dey J K, Kurose J, Towsley D. On-line scheduling policies for a class of IRIS (increasing reward with increasing service) real-time tasks. IEEE Transactions on Computers, 1996, 45(7): 802-813.

[30] Liu J, Wang Y, Xing J et al. Real-time system design based on logic OR constrained optimization. Journal of Software, 2006, 17(7): 1641-1649. (in Chinese)

[31] Lehoczky J, Sha L, Ding Y. The rate monotonic scheduling algorithm: Exact characterization and average case behavior. In Proc. the Real Time Systems Symposium, December 1989, pp.166-171.

[32] Balinski M L. Integer programming: Methods, uses, computations. Management Science, 1965, 12(3): 253-313.

[33] Jovanovi? D, de Moura L. Solving nonlinear arithmetic. In Proc. the 6th International Joint Conference on Automated Reasoning, June 2012, pp.339-354.
No related articles found!
Full text



[1] Zhang Bo; Zhang Ling;. Statistical Heuristic Search[J]. , 1987, 2(1): 1 -11 .
[2] Meng Liming; Xu Xiaofei; Chang Huiyou; Chen Guangxi; Hu Mingzeng; Li Sheng;. A Tree-Structured Database Machine for Large Relational Database Systems[J]. , 1987, 2(4): 265 -275 .
[3] Lin Qi; Xia Peisu;. The Design and Implementation of a Very Fast Experimental Pipelining Computer[J]. , 1988, 3(1): 1 -6 .
[4] Sun Chengzheng; Tzu Yungui;. A New Method for Describing the AND-OR-Parallel Execution of Logic Programs[J]. , 1988, 3(2): 102 -112 .
[5] Zhang Bo; Zhang Tian; Zhang Jianwei; Zhang Ling;. Motion Planning for Robots with Topological Dimension Reduction Method[J]. , 1990, 5(1): 1 -16 .
[6] Yu Xiangdong;. Some Hard Examples for the Resolution Method[J]. , 1990, 5(3): 302 -304 .
[7] Wang Dingxing; Zheng Weimin; Du Xiaoli; Guo Yike;. On the Execution Mechanisms of Parallel Graph Reduction[J]. , 1990, 5(4): 333 -346 .
[8] Zhou Quan; Wei Daozheng;. A Complete Critical Path Algorithm for Test Generation of Combinational Circuits[J]. , 1991, 6(1): 74 -82 .
[9] Zhao Jinghai; Liu Shenquan;. An Environment for Rapid Prototyping of Interactive Systems[J]. , 1991, 6(2): 135 -144 .
[10] Shang Lujun; Xu Lihui;. Notes on the Design of an Integrated Object-Oriented DBMS Family[J]. , 1991, 6(4): 389 -394 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved