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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
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.
Nelson G, Oppen D C. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 1979, 1(2): 245-257.
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.
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.
Armando A, Ranise S, Rusinowitch M. A rewriting approach to satisfiability procedures. Information and Computation, 2003, 183(2): 140-164.
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.
De Moura L, Bjørner N. Satisfiability modulo theories: Introduction and applications. Communications of the ACM, 2011, 54(9): 69-77.
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.
Barrett C, Conway C L, Deters M, Hadarean L, Jovanovi´c D, King T, Reynolds A, Tinelli C. CVC4. In Proc. the 23rd International Conference on Computer Aided Verification, July 2011, pp.171-177.
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.
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.
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.
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.
Sebastiani R, Tomasi S. Optimization in SMT with \( \mathrm{\mathcal{L}}\mathcal{A}\left(\mathbb{Q}\right) \) cost functions. In Proc. the 6th International Joint Conference on Automated Reasoning, June 2012, pp.484-498.
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.
Dantzig G B. Linear Programming and Extensions. Princeton University Press, Princeton, NJ, USA, 1965.
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.
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.
Han S P. A globally convergent method for nonlinear programming. Journal of Optimization Theory and Applications, 1977, 22(3): 297-309.
Powell M J. Algorithms for nonlinear constraints that use lagrangian functions. Mathematical Programming, 1978, 14(1): 224-248.
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.
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.
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.
Kopetz H. Real-Time Systems: Design Principles for Distributed Embedded Applications (2nd edition). Springer, New York, USA, 2011.
Mall R. Real-Time Systems: Theory and Practice (1st edition). Upper Saddle River, NJ, USA: Prentice Hall Press, 2007.
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.
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.
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.
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.
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)
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.
Balinski M L. Integer programming: Methods, uses, computations. Management Science, 1965, 12(3): 253-313.
Jovanović D, de Moura L. Solving nonlinear arithmetic. In Proc. the 6th International Joint Conference on Automated Reasoning, June 2012, pp.339-354.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Chen, L., Wu, JZ., Lv, YR. et al. An Efficient Approach for Solving Optimization over Linear Arithmetic Constraints. J. Comput. Sci. Technol. 31, 987–1011 (2016). https://doi.org/10.1007/s11390-016-1675-x
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11390-016-1675-x