A benders decomposition approach to deciding modular linear integer arithmetic

Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

1 Citation (Scopus)

Abstract

Verification tasks frequently require deciding systems of linear constraints over modular (machine) arithmetic. Existing approaches for reasoning over modular arithmetic use bit-vector solvers, or else approximate machine integers with mathematical integers and use arithmetic solvers. Neither is ideal; the first is sound but inefficient, and the second is efficient but unsound. We describe a linear encoding which correctly describes modular arithmetic semantics, yielding an optimistic but sound approach. Our method abstracts the problem with linear arithmetic, but progressively refines the abstraction when modular semantics is violated. This preserves soundness while exploiting the mostly integer nature of the constraint problem. We present a prototype implementation, which gives encouraging experimental results.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2017
Subtitle of host publication20th International Conference Melbourne, VIC, Australia, August 28 – September 1, 2017 Proceedings
EditorsSerge Gaspers, Toby Walsh
Place of PublicationCham Switzerland
PublisherSpringer
Pages380-397
Number of pages18
ISBN (Electronic)9783319662633
ISBN (Print)9783319662626
DOIs
Publication statusPublished - 2017
Externally publishedYes
EventInternational Conference on Theory and Applications of Satisfiability Testing 2017 - Melbourne, Australia
Duration: 28 Aug 20171 Sep 2017
Conference number: 20th
http://sat2017.gitlab.io/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10491
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2017
Abbreviated titleSAT 2017
CountryAustralia
CityMelbourne
Period28/08/171/09/17
Internet address

Cite this

Kafle, B., Gange, G., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2017). A benders decomposition approach to deciding modular linear integer arithmetic. In S. Gaspers, & T. Walsh (Eds.), Theory and Applications of Satisfiability Testing – SAT 2017: 20th International Conference Melbourne, VIC, Australia, August 28 – September 1, 2017 Proceedings (pp. 380-397). (Lecture Notes in Computer Science ; Vol. 10491 ). Cham Switzerland: Springer. https://doi.org/10.1007/978-3-319-66263-3_24
Kafle, Bishoksan ; Gange, Graeme ; Schachte, Peter ; Søndergaard, Harald ; Stuckey, Peter J. / A benders decomposition approach to deciding modular linear integer arithmetic. Theory and Applications of Satisfiability Testing – SAT 2017: 20th International Conference Melbourne, VIC, Australia, August 28 – September 1, 2017 Proceedings. editor / Serge Gaspers ; Toby Walsh. Cham Switzerland : Springer, 2017. pp. 380-397 (Lecture Notes in Computer Science ).
@inproceedings{60ace1fe8b754cf2aac7f91207d5b7e3,
title = "A benders decomposition approach to deciding modular linear integer arithmetic",
abstract = "Verification tasks frequently require deciding systems of linear constraints over modular (machine) arithmetic. Existing approaches for reasoning over modular arithmetic use bit-vector solvers, or else approximate machine integers with mathematical integers and use arithmetic solvers. Neither is ideal; the first is sound but inefficient, and the second is efficient but unsound. We describe a linear encoding which correctly describes modular arithmetic semantics, yielding an optimistic but sound approach. Our method abstracts the problem with linear arithmetic, but progressively refines the abstraction when modular semantics is violated. This preserves soundness while exploiting the mostly integer nature of the constraint problem. We present a prototype implementation, which gives encouraging experimental results.",
author = "Bishoksan Kafle and Graeme Gange and Peter Schachte and Harald S{\o}ndergaard and Stuckey, {Peter J.}",
year = "2017",
doi = "10.1007/978-3-319-66263-3_24",
language = "English",
isbn = "9783319662626",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "380--397",
editor = "Serge Gaspers and Toby Walsh",
booktitle = "Theory and Applications of Satisfiability Testing – SAT 2017",

}

Kafle, B, Gange, G, Schachte, P, Søndergaard, H & Stuckey, PJ 2017, A benders decomposition approach to deciding modular linear integer arithmetic. in S Gaspers & T Walsh (eds), Theory and Applications of Satisfiability Testing – SAT 2017: 20th International Conference Melbourne, VIC, Australia, August 28 – September 1, 2017 Proceedings. Lecture Notes in Computer Science , vol. 10491 , Springer, Cham Switzerland, pp. 380-397, International Conference on Theory and Applications of Satisfiability Testing 2017, Melbourne, Australia, 28/08/17. https://doi.org/10.1007/978-3-319-66263-3_24

A benders decomposition approach to deciding modular linear integer arithmetic. / Kafle, Bishoksan; Gange, Graeme; Schachte, Peter; Søndergaard, Harald; Stuckey, Peter J.

Theory and Applications of Satisfiability Testing – SAT 2017: 20th International Conference Melbourne, VIC, Australia, August 28 – September 1, 2017 Proceedings. ed. / Serge Gaspers; Toby Walsh. Cham Switzerland : Springer, 2017. p. 380-397 (Lecture Notes in Computer Science ; Vol. 10491 ).

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

TY - GEN

T1 - A benders decomposition approach to deciding modular linear integer arithmetic

AU - Kafle, Bishoksan

AU - Gange, Graeme

AU - Schachte, Peter

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

PY - 2017

Y1 - 2017

N2 - Verification tasks frequently require deciding systems of linear constraints over modular (machine) arithmetic. Existing approaches for reasoning over modular arithmetic use bit-vector solvers, or else approximate machine integers with mathematical integers and use arithmetic solvers. Neither is ideal; the first is sound but inefficient, and the second is efficient but unsound. We describe a linear encoding which correctly describes modular arithmetic semantics, yielding an optimistic but sound approach. Our method abstracts the problem with linear arithmetic, but progressively refines the abstraction when modular semantics is violated. This preserves soundness while exploiting the mostly integer nature of the constraint problem. We present a prototype implementation, which gives encouraging experimental results.

AB - Verification tasks frequently require deciding systems of linear constraints over modular (machine) arithmetic. Existing approaches for reasoning over modular arithmetic use bit-vector solvers, or else approximate machine integers with mathematical integers and use arithmetic solvers. Neither is ideal; the first is sound but inefficient, and the second is efficient but unsound. We describe a linear encoding which correctly describes modular arithmetic semantics, yielding an optimistic but sound approach. Our method abstracts the problem with linear arithmetic, but progressively refines the abstraction when modular semantics is violated. This preserves soundness while exploiting the mostly integer nature of the constraint problem. We present a prototype implementation, which gives encouraging experimental results.

UR - http://www.scopus.com/inward/record.url?scp=85028710332&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-66263-3_24

DO - 10.1007/978-3-319-66263-3_24

M3 - Conference Paper

AN - SCOPUS:85028710332

SN - 9783319662626

T3 - Lecture Notes in Computer Science

SP - 380

EP - 397

BT - Theory and Applications of Satisfiability Testing – SAT 2017

A2 - Gaspers, Serge

A2 - Walsh, Toby

PB - Springer

CY - Cham Switzerland

ER -

Kafle B, Gange G, Schachte P, Søndergaard H, Stuckey PJ. A benders decomposition approach to deciding modular linear integer arithmetic. In Gaspers S, Walsh T, editors, Theory and Applications of Satisfiability Testing – SAT 2017: 20th International Conference Melbourne, VIC, Australia, August 28 – September 1, 2017 Proceedings. Cham Switzerland: Springer. 2017. p. 380-397. (Lecture Notes in Computer Science ). https://doi.org/10.1007/978-3-319-66263-3_24