Skip to main content
SpringerLink
Log in

A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10900))

Included in the following conference series:

Abstract

We present a combination of the Mixed-Echelon-Hermite transformation and the Double-Bounded reduction for systems of linear mixed arithmetic that preserve satisfiability and can be computed in polynomial time. Together, the two transformations turn any system of linear mixed constraints into a bounded system, i.e., a system for which termination can be achieved easily. Existing approaches for linear mixed arithmetic, e.g., branch-and-bound and cuts from proofs, only explore a finite search space after application of our two transformations. Instead of generating a priori bounds for the variables, e.g., as suggested by Papadimitriou, unbounded variables are eliminated through the two transformations. The transformations orient themselves on the structure of an input system instead of computing a priori (over-)approximations out of the available constants. Experiments provide further evidence to the efficiency of the transformations in practice. We also present a polynomial method for converting certificates of (un)satisfiability from the transformed to the original system.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    All techniques discussed in this paper can be extended to strict inequalities with the help of \(\delta \)-rationals [18]. We will omit the strict inequalities and focus only on non-strict inequalities due to lack of space.

  2. 2.

    A rational solution can be computed in polynomial time [23].

  3. 3.

    We do actually use less efficient, Gaussian-elimination-based transformations in our own implementation [7]. The reason is that these transformations are incrementally efficient. Our experiments show that the transformation cost still remains negligible in practice.

  4. 4.

    Available on http://www.spass-prover.org/spass-iq.

References

  1. Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84–99. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04222-5_5

    Chapter  Google Scholar 

  2. Bareiss, E.H.: Sylvester’s identity and multistep integer-preserving Gaussian elimination. Math. Comput. 22(103), 565–578 (1968)

    MathSciNet  MATH  Google Scholar 

  3. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  4. Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 39–57. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_3

    Chapter  Google Scholar 

  5. Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Mahboubi, A., Mebsout, A., Melquiond, G.: A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 67–81. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_8

    Chapter  Google Scholar 

  6. Boyd, S. Vandenberghe, L.: Convex optimization. In: CUP (2004)

    Google Scholar 

  7. Bromberger, M.: A reduction from unbounded linear mixed arithmetic problems into bounded problems. ArXiv e-Prints, abs/1804.07703 (2018)

    Google Scholar 

  8. Bromberger, M., Sturm, T., Weidenbach, C.: Linear integer arithmetic revisited. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 623–637. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_42

    Chapter  Google Scholar 

  9. Bromberger, M., Weidenbach, C.: Computing a complete basis for equalities implied by a system of LRA constraints. In: SMT 2016 (2016)

    Google Scholar 

  10. Bromberger, M., Weidenbach, C.: Fast cube tests for LIA constraint solving. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 116–132. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40229-1_9

    Chapter  Google Scholar 

  11. Bromberger, M., Weidenbach, C.: New techniques for linear arithmetic: cubes and equalities. Form. Methods Syst. Des. 51(3), 433–461 (2017)

    Article  Google Scholar 

  12. Christ, J., Hoenicke, J.: Cutting the mix. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 37–52. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_3

    Chapter  Google Scholar 

  13. Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31759-0_19

    Chapter  Google Scholar 

  14. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_7

    Chapter  MATH  Google Scholar 

  15. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  16. Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 233–247. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_20

    Chapter  Google Scholar 

  17. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49

    Chapter  Google Scholar 

  18. Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_11

    Chapter  Google Scholar 

  19. Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. Math. Comput. Sci. 6(4), 409–425 (2012)

    Article  MathSciNet  Google Scholar 

  20. Griggio, A.: A practical approach to satisfiability modulo linear integer arithmetic. JSAT 8(1/2), 1–27 (2012)

    MathSciNet  MATH  Google Scholar 

  21. Jovanović, D., de Moura, L.: Cutting to the chase. JAR 51(1), 79–108 (2013)

    Article  MathSciNet  Google Scholar 

  22. Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765–768 (1981)

    Article  MathSciNet  Google Scholar 

  23. Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max Planck Institute for Informatics and Saarland University, Saarland Informatics Campus, Saarbrücken, Germany

    Martin Bromberger

  2. Graduate School of Computer Science, Saarland Informatics Campus, Saarbrücken, Germany

    Martin Bromberger

Authors
  1. Martin Bromberger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Bromberger .

Editor information

Editors and Affiliations

  1. Université de Lorraine, Vandoeuvre-lès-Nancy, France

    Didier Galmiche

  2. Baden-Wuerttemberg Cooperative State University, Stuttgart, Germany

    Stephan Schulz

  3. University of Trento, Trento, Italy

    Roberto Sebastiani

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Bromberger, M. (2018). A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds) Automated Reasoning. IJCAR 2018. Lecture Notes in Computer Science(), vol 10900. Springer, Cham. https://doi.org/10.1007/978-3-319-94205-6_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94205-6_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94204-9

  • Online ISBN: 978-3-319-94205-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation