Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization

Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization. Cimatti, A., Griggio, A., Irfan, A., Roveri, M., & Sebastiani, R. In Beyersdorff, O. & Wintersteiger, C. M., editors, Theory and Applications of Satisfiability Testing – SAT 2018, volume 10929, pages 383–398, Cham, 2018. Springer International Publishing. Series Title: Lecture Notes in Computer Science

Paper doi abstract bibtex

Incremental linearization is a conceptually simple, yet eﬀective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its eﬀectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.

@inproceedings{beyersdorff_experimenting_2018,
	address = {Cham},
	title = {Experimenting on {Solving} {Nonlinear} {Integer} {Arithmetic} with {Incremental} {Linearization}},
	volume = {10929},
	isbn = {978-3-319-94143-1 978-3-319-94144-8},
	url = {http://link.springer.com/10.1007/978-3-319-94144-8_23},
	doi = {10.1007/978-3-319-94144-8_23},
	abstract = {Incremental linearization is a conceptually simple, yet eﬀective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its eﬀectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.},
	language = {en},
	urldate = {2023-03-30},
	booktitle = {Theory and {Applications} of {Satisfiability} {Testing} – {SAT} 2018},
	publisher = {Springer International Publishing},
	author = {Cimatti, Alessandro and Griggio, Alberto and Irfan, Ahmed and Roveri, Marco and Sebastiani, Roberto},
	editor = {Beyersdorff, Olaf and Wintersteiger, Christoph M.},
	year = {2018},
	note = {Series Title: Lecture Notes in Computer Science},
	pages = {383--398},
}

Downloads: 0

{"_id":"5PWinbzu4zRqDjJok","bibbaseid":"cimatti-griggio-irfan-roveri-sebastiani-experimentingonsolvingnonlinearintegerarithmeticwithincrementallinearization-2018","author_short":["Cimatti, A.","Griggio, A.","Irfan, A.","Roveri, M.","Sebastiani, R."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"Cham","title":"Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization","volume":"10929","isbn":"978-3-319-94143-1 978-3-319-94144-8","url":"http://link.springer.com/10.1007/978-3-319-94144-8_23","doi":"10.1007/978-3-319-94144-8_23","abstract":"Incremental linearization is a conceptually simple, yet eﬀective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its eﬀectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.","language":"en","urldate":"2023-03-30","booktitle":"Theory and Applications of Satisfiability Testing – SAT 2018","publisher":"Springer International Publishing","author":[{"propositions":[],"lastnames":["Cimatti"],"firstnames":["Alessandro"],"suffixes":[]},{"propositions":[],"lastnames":["Griggio"],"firstnames":["Alberto"],"suffixes":[]},{"propositions":[],"lastnames":["Irfan"],"firstnames":["Ahmed"],"suffixes":[]},{"propositions":[],"lastnames":["Roveri"],"firstnames":["Marco"],"suffixes":[]},{"propositions":[],"lastnames":["Sebastiani"],"firstnames":["Roberto"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Beyersdorff"],"firstnames":["Olaf"],"suffixes":[]},{"propositions":[],"lastnames":["Wintersteiger"],"firstnames":["Christoph","M."],"suffixes":[]}],"year":"2018","note":"Series Title: Lecture Notes in Computer Science","pages":"383–398","bibtex":"@inproceedings{beyersdorff_experimenting_2018,\n\taddress = {Cham},\n\ttitle = {Experimenting on {Solving} {Nonlinear} {Integer} {Arithmetic} with {Incremental} {Linearization}},\n\tvolume = {10929},\n\tisbn = {978-3-319-94143-1 978-3-319-94144-8},\n\turl = {http://link.springer.com/10.1007/978-3-319-94144-8_23},\n\tdoi = {10.1007/978-3-319-94144-8_23},\n\tabstract = {Incremental linearization is a conceptually simple, yet eﬀective, technique that we have recently proposed for solving SMT problems over nonlinear real arithmetic constraints. In this paper, we show how the same approach can be applied successfully also to the harder case of nonlinear integer arithmetic problems. We describe in detail our implementation of the basic ideas inside the MathSAT SMT solver, and evaluate its eﬀectiveness with an extensive experimental analysis over all nonlinear integer benchmarks in SMT-LIB. Our results show that MathSAT is very competitive with (and often outperforms) state-of-the-art SMT solvers based on alternative techniques.},\n\tlanguage = {en},\n\turldate = {2023-03-30},\n\tbooktitle = {Theory and {Applications} of {Satisfiability} {Testing} – {SAT} 2018},\n\tpublisher = {Springer International Publishing},\n\tauthor = {Cimatti, Alessandro and Griggio, Alberto and Irfan, Ahmed and Roveri, Marco and Sebastiani, Roberto},\n\teditor = {Beyersdorff, Olaf and Wintersteiger, Christoph M.},\n\tyear = {2018},\n\tnote = {Series Title: Lecture Notes in Computer Science},\n\tpages = {383--398},\n}\n\n\n\n\n\n\n\n","author_short":["Cimatti, A.","Griggio, A.","Irfan, A.","Roveri, M.","Sebastiani, R."],"editor_short":["Beyersdorff, O.","Wintersteiger, C. M."],"key":"beyersdorff_experimenting_2018","id":"beyersdorff_experimenting_2018","bibbaseid":"cimatti-griggio-irfan-roveri-sebastiani-experimentingonsolvingnonlinearintegerarithmeticwithincrementallinearization-2018","role":"author","urls":{"Paper":"http://link.springer.com/10.1007/978-3-319-94144-8_23"},"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/matteocarde","dataSources":["SzPGZamk2BCyHJTQr","BLJPWpPi3hneTGaPF"],"keywords":[],"search_terms":["experimenting","solving","nonlinear","integer","arithmetic","incremental","linearization","cimatti","griggio","irfan","roveri","sebastiani"],"title":"Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization","year":2018}