Skip to main content
SpringerLink
Log in

Colors Make Theories Hard

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

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

Included in the following conference series:

  • 852 Accesses

Abstract

The satisfiability problem for conjunctions of quantifier-free literals in first-order theories \(\mathcal {T}\) of interest–“\(\mathcal {T}\) -solving” for short–has been deeply investigated for more than three decades from both theoretical and practical perspectives, and it is currently a core issue of state-of-the-art SMT solving. Given some theory \(\mathcal {T}\) of interest, a key theoretical problem is to establish the computational (in)tractability of \(\mathcal {T}\)-solving, or to identify intractable fragments of \(\mathcal {T}\) .

In this paper we investigate this problem from a general perspective, and we present a simple and general criterion for establishing the NP-hardness of \(\mathcal {T}\)-solving, which is based on the novel concept of “colorer” for a theory \(\mathcal {T}\).

As a proof of concept, we show the effectiveness and simplicity of this novel criterion by easily producing very simple proofs of the NP-hardness for many theories of interest for SMT, or of some of their fragments.

This work is supported by SRC under GRC Research Project 2012-TJ-2266 WOLF. I thank Silvio Ghilardi, Alberto Griggio and Stefano Tonetta for fruitful discussions.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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.

    The symbol “|” is used to separate color and node variables from auxiliary ones.

  2. 2.

    Notice that each \(c_{j}\) is implicitly associated with the color \(C_{j}\in \mathcal {C} \) for every \(j\in [1..k]\) and each \(v_{i}\) and \(\underline{{\mathbf y_i}} \) is implicitly associated to the vertex \(V_{i}\in \mathcal {V} \) for every \(i \in [1..n]\).

  3. 3.

    Notice that k is fixed a priori and as such it is a constant value for the input graph k-colorability problem: e.g., depending on \(\mathcal {T}\), we are speaking of reducing graph 3-colorability–or 4-colorability, or even \(2^{64}\)-colorability–to \(\mathcal {T}\)-solving.

  4. 4.

    Notice that \(\mathcal {NLA}(\mathbb {Z})\)-solving is undecidable.

  5. 5.

    Here “\(=\)” is the equality symbol and it is not the \(\mathcal {FPA}_{e,s} \)-specific symbol “==”, see [22].

  6. 6.

    \(\mathcal {S}\) includes the operators \(\{{\{{...}\}),(\cdot \subseteq \cdot ),(\cdot \cup \cdot ),(\cdot \cap \cdot ),(\cdot \setminus \cdot ),(\cdot \mathcal {P} \cdot ),|\cdot |,(\cdot \in \cdot )}\} \), following their standard semantics. We refer the reader to [6, 12] for a precise description of the theory.

  7. 7.

    We use the following notation: “\(A[i] \)” (aka “read(A, i)”) is the value returned by reading the i-th element of the array A, whilst “\(A\langle {i\leftarrow v_i}\rangle \) ” (aka “write(A, i, v)”) is the array resulting from assigning the value v to the i-th element of array A.

  8. 8.

    Whereas (i) and (ii) can be also written as \(l\models _{\mathcal {T}}(v_i=n)\) and \(l\models _{\mathcal {T}}(v_i\ne n)\), (iii) and (iv) cannot be rewritten as \(l\models _{\mathcal {T}}(v_i\ge 0)\) and \(l\models _{\mathcal {T}}(v_i{>} 0)\) because \(\ge \) and \({>}\) are not part of the signature.

References

  1. Barrett, C.W., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512–526. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  2. Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability Modulo Theories, chapter 26, pp. 825–885. IOS Press, Amsterdam (2009)

    Google Scholar 

  3. Berman, L.: The complexity of logical theories. Theor. Comput. Sci. 11, 71 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., van Rossum, P., Schulz, S., Sebastiani, R.: Mathsat: tight integration of sat and mathematical decision procedures. J. Autom. Reasoning 35(1–3), 265–293 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bradley, A., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Heidelberg (2010)

    MATH  Google Scholar 

  6. Bruun, H., Damm, F., Dawes, J., Hansen, B., Larsen, P., Parkin, G., Plat, N., Toetenel, H.: A formal definition of vdm-sl. Technical report, University of Leicester (1998)

    Google Scholar 

  7. Cyrluk, D., Möller, M.O., Rueß, H.: An efficient decision procedure for the theory of fixed-sized bit-vectors. In: Grumberg, O. (ed.) Computer Aided Verification. LNCS, vol. 1254, pp. 60–71. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  8. Fröhlich, A., Kovásznai, G., Biere, A.: More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. In: Bulatov, A.A., Shur, A.M. (eds.) CSR 2013. LNCS, vol. 7913, pp. 378–390. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. Garey, M.R., Johnson, D.S.: Computers and Intractability. Freeman and Company, New York (1979)

    MATH  Google Scholar 

  10. Karmakar, N.: A new polynomial-time algorithm for linear programming. Combinatorica 4(4), 373 (1984)

    Article  MathSciNet  Google Scholar 

  11. Kovásznai, G., Fröhlich, A., Biere, A.: On the complexity of fixed-size bit-vector logics with binary encoded bit-width. In: Proceedings of the SMT (2012)

    Google Scholar 

  12. Kroening, D., Rümmer, P., Weissenbacher, G.: A proposal for a theory of finite sets, lists, and maps for the SMT-LIB standard. In: Proceedings of the SMT Workshop (2007)

    Google Scholar 

  13. Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  14. Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for Boolean algebra with Presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215–230. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 168–183. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)

    Article  MATH  Google Scholar 

  17. Nelson, G., Oppen, D.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  18. Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Oppen, D.: Reasoning about recursively defined data structures. J. ACM 27(3), 403–411 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  20. Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291–302 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  21. Pratt, V.R.: Two Easy Theories Whose Combination is Hard. Technical report, M.I.T. (1977)

    Google Scholar 

  22. Rümmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: Proceedings of the SMT (2010)

    Google Scholar 

  23. Sebastiani, R.: Lazy satisfiability modulo theories. J. Satisfiability Boolean Model. Comput. (JSAT) 3(3–4), 141–224 (2007)

    MathSciNet  MATH  Google Scholar 

  24. Sebastiani, R.: Colors Make Theories hard. Technical Report DISI-16-001, DISI, University of Trento, Extended version. http://disi.unitn.it/rseba/ijcar16extended.pdf

  25. Shostak, R.: An algorithm for reasoning about equality. In: Proceedings of the 7th International Joint Conference on Artificial Intelligence, pp. 526–527 (1977)

    Google Scholar 

  26. Shostak, R.: A pratical decision procedure for arithmetic with function symbols. J. ACM 26(2), 351–360 (1979)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DISI, University of Trento, Trento, Italy

    Roberto Sebastiani

Authors
  1. Roberto Sebastiani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Roberto Sebastiani .

Editor information

Editors and Affiliations

  1. Aix-Marseille University, Marseille, France

    Nicola Olivetti

  2. SRI International, Menlo Park, California, USA

    Ashish Tiwari

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Sebastiani, R. (2016). Colors Make Theories Hard. In: Olivetti, N., Tiwari, A. (eds) Automated Reasoning. IJCAR 2016. Lecture Notes in Computer Science(), vol 9706. Springer, Cham. https://doi.org/10.1007/978-3-319-40229-1_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40229-1_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40228-4

  • Online ISBN: 978-3-319-40229-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation