{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:41:42Z","timestamp":1725910902701},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319677286"},{"type":"electronic","value":"9783319677293"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67729-3_13","type":"book-chapter","created":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T01:04:04Z","timestamp":1505523844000},"page":"213-228","source":"Crossref","is-referenced-by-count":0,"title":["Constructing Cycles in the Simplex Method for\u00a0DPLL(T)"],"prefix":"10.1007","author":[{"given":"Bertram","family":"Felgenhauer","sequence":"first","affiliation":[]},{"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,17]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1287\/opre.1070.0474","volume":"56","author":"D Avis","year":"2008","unstructured":"Avis, D., Kaluzny, B., Titley-P\u00e9loquin, D.: Visualizing and constructing cycles in the simplex method. Oper. Res. 56(2), 512\u2013518 (2008). doi:\n10.1287\/opre.1070.0474","journal-title":"Oper. Res."},{"issue":"3","key":"13_CR2","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1137\/1011060","volume":"11","author":"ML Balinski","year":"1969","unstructured":"Balinski, M.L., Tucker, A.W.: Duality theory of linear programs: a constructive approach with applications. SIAM Rev. 11(3), 347\u2013377 (1969). doi:\n10.1137\/1011060","journal-title":"SIAM Rev."},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22110-1_14"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1002\/nav.3800020406","volume":"2","author":"EML Beale","year":"1955","unstructured":"Beale, E.M.L.: Cycling in the dual simplex algorithm. Naval Res. Logistics Q. 2, 269\u2013275 (1955). doi:\n10.1002\/nav.3800020406","journal-title":"Naval Res. Logistics Q."},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"13_CR6","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1287\/moor.2.2.103","volume":"2","author":"RG Bland","year":"1977","unstructured":"Bland, R.G.: New finite pivoting rules for the simplex method. Math. Oper. Res. 2(2), 103\u2013107 (1977). doi:\n10.1287\/moor.2.2.103","journal-title":"Math. Oper. Res."},{"key":"13_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8","volume-title":"The Calculus of Computation\u2014Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation\u2014Decision Procedures with Applications to Verification. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-74113-8"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). doi:\n10.1007\/978-3-319-08867-9_49"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). doi:\n10.1007\/11817963_11"},{"key":"13_CR10","unstructured":"Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Technical report SRI-CSL-06-01, SRI International (2006)"},{"issue":"1","key":"13_CR11","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BF01593804","volume":"12","author":"D Goldfarb","year":"1977","unstructured":"Goldfarb, D., Reid, J.K.: A practicable steepest-edge simplex algorithm. Math. Program. 12(1), 361\u2013371 (1977). doi:\n10.1007\/BF01593804","journal-title":"Math. Program."},{"issue":"1","key":"13_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01580108","volume":"5","author":"PMJ Harris","year":"1973","unstructured":"Harris, P.M.J.: Pivot selection methods of the Devex LP code. Math. Program. 5(1), 1\u201328 (1973). doi:\n10.1007\/BF01580108","journal-title":"Math. Program."},{"key":"13_CR13","unstructured":"Hoffman, A.J.: Cycling in the simplex algorithm. Technical report, 2974. National Bureau of Standards (1953)"},{"key":"13_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3","volume-title":"Decision Procedures\u2014An Algorithmic Point of View","author":"D Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures\u2014An Algorithmic Point of View. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-74105-3"},{"issue":"1","key":"13_CR15","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1002\/nav.3800160110","volume":"16","author":"K Marshall","year":"1969","unstructured":"Marshall, K., Suurballe, J.: A note on cycling in the simplex method. Naval Res. Logistics Q. 16(1), 121\u2013137 (1969). doi:\n10.1002\/nav.3800160110","journal-title":"Naval Res. Logistics Q."},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1016\/j.ejor.2007.03.026","volume":"187","author":"PQ Pan","year":"2008","unstructured":"Pan, P.Q.: A largest-distance pivot rule for the simplex algorithm. Eur. J. Oper. Res. 187(2), 393\u2013402 (2008). doi:\n10.1016\/j.ejor.2007.03.026","journal-title":"Eur. J. Oper. Res."},{"key":"13_CR17","volume-title":"Linear and Integer Programming","author":"G Sierksma","year":"1996","unstructured":"Sierksma, G.: Linear and Integer Programming, 2nd edn. Marcel Dekker Inc., New York City (1996)","edition":"2"},{"key":"13_CR18","volume-title":"Linear Programming: An Introduction to Finite Improvement Algorithms","author":"D Solow","year":"1984","unstructured":"Solow, D.: Linear Programming: An Introduction to Finite Improvement Algorithms. North-Holland, Amsterdam (1984)"},{"key":"13_CR19","unstructured":"Yudin, D.B., Gol\u2019shtein, E.G.: Linear programming. In: Israel Program of Scientific Translations (1965)"},{"issue":"8","key":"13_CR20","doi-asserted-by":"publisher","first-page":"2247","DOI":"10.1016\/j.cor.2005.02.001","volume":"33","author":"P Z\u00f6rnig","year":"2006","unstructured":"Z\u00f6rnig, P.: Systematic construction of examples for cycling in the simplex method. Comput. Oper. Res. 33(8), 2247\u20132262 (2006). doi:\n10.1016\/j.cor.2005.02.001","journal-title":"Comput. Oper. Res."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67729-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T01:07:49Z","timestamp":1505524069000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67729-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319677286","9783319677293"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67729-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}