Skip to main content

Circuit Satisfiability and Constraint Satisfaction Around Skolem Arithmetic

  • Conference paper
  • First Online:
Pursuit of the Universal (CiE 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9709))

Included in the following conference series:

Abstract

We study interactions between Skolem Arithmetic and certain classes of Circuit Satisfiability and Constraint Satisfaction Problems (CSPs). We revisit results of Glaßer et al. [16] in the context of CSPs and settle the major open question from that paper, finding a certain satisfiability problem on circuits—involving complement, intersection, union and multiplication—to be decidable. This we prove using the decidability of Skolem Arithmetic. Then we solve a second question left open in [16] by proving a tight upper bound for the similar circuit satisfiability problem involving just intersection, union and multiplication. We continue by studying first-order expansions of Skolem Arithmetic without constants, \((\mathbb {N};\times )\), as CSPs. We find already here a rich landscape of problems with non-trivial instances that are in P as well as those that are NP-complete.

P. Jonsson—was partially supported by the Swedish Research Council (VR) under grant 621-2012-3239.

B. Martin—was supported by EPSRC grant EP/L005654/1.

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

Access this chapter

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.

    Weird. Thus spake Lindemann about Hilbert’s non-constructive methods in the resolution of Gordon’s problem (see [28]).

References

  1. Barto, L., Kozik, M.: Constraint satisfaction problems of bounded width. In: FOCS, pp. 595–603 (2009)

    Google Scholar 

  2. Barto, L., Kozik, M., Niven, T.: The CSP dichotomy holds for digraphs with no sources and no sinks (a positive answer to a conjecture of Bang-Jensen and Hell). SIAM J. Comput. 38(5), 1782–1802 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bès, A.: A tribute to Maurice Boffa. Soc. Math. Belgique, 1–54 (2002)

    Google Scholar 

  4. Bodirsky, M., Jonsson, P., von Oertzen, T.: Essential convexity and complexity of semi-algebraic constraints. Log. Methods Comput. Sci. 8, 4 (2012). Extended abstract titled Semilinear Program Feasibility at ICALP 2010

    Article  MathSciNet  MATH  Google Scholar 

  5. Bodirsky, M., Kára, J.: The complexity of temporal constraint satisfaction problems. J. ACM 57, 2 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bodirsky, M., Martin, B., Mottet, A.: Constraint satisfaction problems over the integers with successor. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9134, pp. 256–267. Springer, Heidelberg (2015)

    Google Scholar 

  7. Bodirsky, M., Pinsker, M.: Schaefer’s theorem for graphs. In: Proceedings of STOC 2011, pp. 655–664 (2011). Preprint of the long version available at arxiv.org/abs/1011.2894

  8. Breunig, H.-G.: The complexity of membership problems for circuits over sets of positive numbers. In: Csuhaj-Varjú, E., Ésik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 125–136. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Bulatov, A.: A dichotomy theorem for constraint satisfaction problems on a 3-element set. J. ACM 53(1), 66–120 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  10. Bulatov, A., Krokhin, A., Jeavons, P.G.: Classifying the complexity of constraints using finite algebras. SIAM J. Comput. 34, 720–742 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  11. Dose, T.: Complexity of constraint satisfaction problems over finite subsets of natural numbers. In: ECCC (2016)

    Google Scholar 

  12. Feder, T., Madelaine, F.R., Stewart, I.A.: Dichotomies for classes of homomorphism problems involving unary functions. Theor. Comput. Sci. 314(1–2), 1–43 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  13. Feder, T., Vardi, M.: The computational structure of monotone monadic SNP and constraint satisfaction: a study through datalog and group theory. SIAM J. Comput. 28, 57–104 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  14. Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics. Springer, Heidelberg (1979)

    MATH  Google Scholar 

  15. Glaßer, C., Herr, K., Reitwießner, C., Travers, S.D., Waldherr, M.: Equivalence problems for circuits over sets of natural numbers. Theor. Comput. Syst. 46(1), 80–103 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  16. Glaßer, C., Reitwießner, C., Travers, S.D., Waldherr, M.: Satisfiability of algebraic circuits over sets of natural numbers. Discrete Appl. Math. 158(13), 1394–1403 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  17. Hell, P., Nešetřil, J.: On the complexity of H-coloring. J. Comb. Theor. Ser. B 48, 92–110 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  18. Jez, A., Okhotin, A.: Complexity of equations over sets of natural numbers. Theor. Comput. Sci. 48(2), 319–342 (2011)

    MathSciNet  MATH  Google Scholar 

  19. Jez, A., Okhotin, A.: Computational completeness of equations over sets of natural numbers. Inform. Comput. 237, 56–94 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  20. Jonsson, P., Lööw, T.: Computational complexity of linear constraints over the integers. Artif. Intell. 195, 44–62 (2013). An extended abstract appeared at IJCAI 2011

    Article  MathSciNet  MATH  Google Scholar 

  21. McKenzie, P., Wagner, K.W.: The complexity of membership problems for circuits over sets of natural numbers. Comput. Complex. 16(3), 211–244 (2007). Extended abstract appeared at STACS 2003

    Article  MathSciNet  MATH  Google Scholar 

  22. Mostowski, A.: On direct products of theories. J. Symb. Log. 17(3), 1–31 (1952)

    Article  MathSciNet  MATH  Google Scholar 

  23. Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)

    MATH  Google Scholar 

  24. Pratt-Hartmann, I., Düntsch, I.: Functions definable by arithmetic circuits. In: Ambos-Spies, K., Löwe, B., Merkle, W. (eds.) CiE 2009. LNCS, vol. 5635, pp. 409–418. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  25. Presburger, M.: Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen. In: welchem die Addition als einzige Operation hervortritt, Comptes Rendus du I congres de Mathématiciens des Pays Slaves, pp. 92–101 (1929)

    Google Scholar 

  26. Schaefer, T.J.: The complexity of satisfiability problems. In: Proceedings of STOC 1978, pp. 216–226 (1978)

    Google Scholar 

  27. Skolem, T.: Über gewisse satzfunktionen in der arithmetik. Skr, Norske Videnskaps-Akademie i Oslo (1930)

    Google Scholar 

  28. Smorynski, C.: The incompleteness theorems. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 821–865. North-Holland, Amsterdam (1977)

    Chapter  Google Scholar 

  29. Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: Proceedings of the 5th Annual ACM Symposium on Theory of Computing, (STOC), pp. 1–9 (1973)

    Google Scholar 

  30. Travers, S.D.: The complexity of membership problems for circuits over sets of integers. Theor. Comput. Sci. 369(1–3), 211–229 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  31. Wagner, K.: The complexity of problems concerning graphs with regularities. In: MFCS, pp. 544–552 (1984)

    Google Scholar 

  32. Yang, K.: Integer circuit evaluation is Pspace-complete. J. Comput. Syst. Sci. 63(2), 288–303 (2001). An extended abstract of appeared at CCC 2000

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Barnaby Martin .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Glaßer, C., Jonsson, P., Martin, B. (2016). Circuit Satisfiability and Constraint Satisfaction Around Skolem Arithmetic. In: Beckmann, A., Bienvenu, L., Jonoska, N. (eds) Pursuit of the Universal. CiE 2016. Lecture Notes in Computer Science(), vol 9709. Springer, Cham. https://doi.org/10.1007/978-3-319-40189-8_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-40189-8_33

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-40188-1

  • Online ISBN: 978-3-319-40189-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics