{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T03:49:13Z","timestamp":1649216953068},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"5","content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2016,9]]},"DOI":"10.1007\/s11390-016-1675-x","type":"journal-article","created":{"date-parts":[[2016,9,5]],"date-time":"2016-09-05T02:14:38Z","timestamp":1473041678000},"page":"987-1011","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["An Efficient Approach for Solving Optimization over Linear Arithmetic Constraints"],"prefix":"10.1007","volume":"31","author":[{"given":"Li","family":"Chen","sequence":"first","affiliation":[]},{"given":"Jing-Zheng","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Yin-Run","family":"Lv","sequence":"additional","affiliation":[]},{"given":"Yong-Ji","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,9]]},"reference":[{"key":"1675_CR1","unstructured":"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."},{"issue":"2","key":"1675_CR2","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson G, Oppen D C. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS), 1979, 1(2): 245-257.","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"1675_CR3","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/10720246_8"},{"key":"1675_CR4","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-45620-1_17"},{"issue":"2","key":"1675_CR5","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A Armando","year":"2003","unstructured":"Armando A, Ranise S, Rusinowitch M. A rewriting approach to satisfiability procedures. Information and Computation, 2003, 183(2): 140-164.","journal-title":"Information and Computation"},{"issue":"6","key":"1675_CR6","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"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.","journal-title":"Journal of the ACM"},{"issue":"9","key":"1675_CR7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L Moura De","year":"2011","unstructured":"De Moura L, Bj\u00f8rner N. Satisfiability modulo theories: Introduction and applications. Communications of the ACM, 2011, 54(9): 69-77.","journal-title":"Communications of the ACM"},{"key":"1675_CR8","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"1675_CR9","doi-asserted-by":"crossref","unstructured":"Barrett C, Conway C L, Deters M, Hadarean L, Jovanovi\u00b4c D, King T, Reynolds A, Tinelli C. CVC4. In Proc. the 23rd International Conference on Computer Aided Verification, July 2011, pp.171-177.","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"1675_CR10","doi-asserted-by":"crossref","unstructured":"De Moura L, Bj\u00f8rner 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.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"1675_CR11","unstructured":"Bj\u00f8rner N, De Moura L. Z310: Applications, enablers, challenges and directions. In Proc. the 6th International Workshop on Constraints in Formal Verification, June 2009."},{"key":"1675_CR12","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N. Satisfiability modulo theories: An appetizer. In Proc. the 12th Brazilian Symposium on Formal Methods, August 2009, pp.23-36.","DOI":"10.1007\/978-3-642-10452-7_3"},{"key":"1675_CR13","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1145\/2535838.2535857"},{"key":"1675_CR14","doi-asserted-by":"crossref","unstructured":"Sebastiani R, Tomasi S. Optimization in SMT with \u2112 A \u211a $$ \\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.","DOI":"10.1007\/978-3-642-31365-3_38"},{"key":"1675_CR15","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/978-3-642-29700-7_23"},{"key":"1675_CR16","unstructured":"Dantzig G B. Linear Programming and Extensions. Princeton University Press, Princeton, NJ, USA, 1965."},{"issue":"1","key":"1675_CR17","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/PL00011391","volume":"89","author":"RH Byrd","year":"2000","unstructured":"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.","journal-title":"Mathematical Programming"},{"issue":"4","key":"1675_CR18","doi-asserted-by":"crossref","first-page":"877","DOI":"10.1137\/S1052623497325107","volume":"9","author":"RH Byrd","year":"1999","unstructured":"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.","journal-title":"SIAM Journal on Optimization"},{"issue":"3","key":"1675_CR19","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00932858","volume":"22","author":"SP Han","year":"1977","unstructured":"Han S P. A globally convergent method for nonlinear programming. Journal of Optimization Theory and Applications, 1977, 22(3): 297-309.","journal-title":"Journal of Optimization Theory and Applications"},{"issue":"1","key":"1675_CR20","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/BF01588967","volume":"14","author":"MJ Powell","year":"1978","unstructured":"Powell M J. Algorithms for nonlinear constraints that use lagrangian functions. Mathematical Programming, 1978, 14(1): 224-248.","journal-title":"Mathematical Programming"},{"issue":"3","key":"1675_CR21","doi-asserted-by":"crossref","first-page":"1120","DOI":"10.1007\/s11227-010-0506-z","volume":"59","author":"N Min-Allah","year":"2012","unstructured":"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.","journal-title":"The Journal of Supercomputing"},{"key":"1675_CR22","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/11817963_11"},{"key":"1675_CR23","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"1675_CR24","doi-asserted-by":"crossref","unstructured":"Kopetz H. Real-Time Systems: Design Principles for Distributed Embedded Applications (2nd edition). Springer, New York, USA, 2011.","DOI":"10.1007\/978-1-4419-8237-7"},{"key":"1675_CR25","unstructured":"Mall R. Real-Time Systems: Theory and Practice (1st edition). Upper Saddle River, NJ, USA: Prentice Hall Press, 2007."},{"issue":"1","key":"1675_CR26","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/321738.321743","volume":"20","author":"CL Liu","year":"1973","unstructured":"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.","journal-title":"Journal of the ACM"},{"issue":"9","key":"1675_CR27","doi-asserted-by":"crossref","first-page":"1156","DOI":"10.1109\/12.57057","volume":"39","author":"JY Chung","year":"1990","unstructured":"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.","journal-title":"IEEE Transactions on Computers"},{"issue":"5","key":"1675_CR28","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1109\/2.76287","volume":"24","author":"JW Liu","year":"1991","unstructured":"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.","journal-title":"Computer"},{"issue":"7","key":"1675_CR29","doi-asserted-by":"crossref","first-page":"802","DOI":"10.1109\/12.508319","volume":"45","author":"JK Dey","year":"1996","unstructured":"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.","journal-title":"IEEE Transactions on Computers"},{"issue":"7","key":"1675_CR30","doi-asserted-by":"crossref","first-page":"1641","DOI":"10.1360\/jos171641","volume":"17","author":"J Liu","year":"2006","unstructured":"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)","journal-title":"Journal of Software"},{"key":"1675_CR31","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1109\/REAL.1989.63567"},{"issue":"3","key":"1675_CR32","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1287\/mnsc.12.3.253","volume":"12","author":"ML Balinski","year":"1965","unstructured":"Balinski M L. Integer programming: Methods, uses, computations. Management Science, 1965, 12(3): 253-313.","journal-title":"Management Science"},{"key":"1675_CR33","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107 D, de Moura L. Solving nonlinear arithmetic. In Proc. the 6th International Joint Conference on Automated Reasoning, June 2012, pp.339-354.","DOI":"10.1007\/978-3-642-31365-3_27"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-016-1675-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T02:03:38Z","timestamp":1568340218000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-016-1675-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":33,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,9]]}},"alternative-id":["1675"],"URL":"https:\/\/doi.org\/10.1007\/s11390-016-1675-x","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9]]}}}