Abstract
Logics that can reason about sets and their cardinality bounds are useful in program analysis, program verification, databases, and knowledge bases. This paper presents a class of constraints on sets and their cardinalities for which the satisfiability and the entailment problems are computable in polynomial time. Our class of constraints, based on tree-shaped formulas, is unique in being simultaneously tractable and able to express 1) that a set is a union of other sets, 2) that sets are disjoint, and 3) that a set has cardinality within a given range. As the main result we present a polynomial-time algorithm for checking entailment of our constraints.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aiken, A., et al.: The complexity of set constraints. In: Meinke, K., Börger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol. 832, Springer, Heidelberg (1994)
Baader, F., Brandt, S., Lutz, C.: Pushing the \(\mathcal{EL}\) envelope. In: Proc. 19th Int. Joint Conf. on Artificial Intelligence IJCAI-05 (2005)
Baader, F., et al. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)
Bachmair, L., Ganzinger, H., Waldmann, U.: Set constraints are the monadic class. In: Logic in Computer Science, pp. 75–83 (1993)
Cantone, D., Omodeo, E., Policriti, A.: Set Theory for Computing. Springer, Heidelberg (2001)
Courcelle, B.: The monadic second-order logic of graphs III: tree-decompositions, minor and complexity issues. ITA 26, 257–286 (1992)
Dechter, R.: Constraint Processing. Morgan Kaufmann, San Francisco (2003)
Donini, F.M., et al.: The complexity of concept languages. Information and Computation 134(1), 1–58 (1997)
Drossopoulou, S., et al.: More Dynamic Object Re-classification: FickleII. ACM Trans. Programming Languages and Systems 24(2), 153–191 (2002)
Feferman, S., Vaught, R.L.: The first order properties of products of algebraic systems. Fundamenta Mathematicae 47, 57–103 (1959)
Fowler, M.: UML Distilled, 2nd edn. Addison-Wesley, Reading (2000)
Givan, R., Mcallester, D.: Polynomial-time computation via local inference relations. ACM Trans. Comput. Logic 3(4), 521–541 (2002)
Grädel, E.: Domino games with an application to the complexity of boolean algebras with bounded quantifier alternations. In: Cori, R., Wirsing, M. (eds.) STACS 1988. LNCS, vol. 294, pp. 98–107. Springer, Heidelberg (1988)
Jackson, D.: Software Abstractions: Logic, Language, & Analysis. MIT Press, Cambridge (2006)
Kozen, D.: Complexity of boolean algebras. Theoretical Computer Science 10, 221–247 (1980)
Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)
Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: Annual ACM Symp. on Principles of Programming Languages (POPL) (2002)
Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean Algebra with Presburger Arithmetic. J. of Automated Reasoning (2006), http://dx.doi.org/10.1007/s10817-006-9042-1
Kuncak, V., Rinard, M.: The first-order theory of sets with cardinality constraints is decidable. Technical Report 958, MIT CSAIL (July 2004)
Lam, P., Kuncak, V., Rinard, M.: Generalized Typestate Checking for Data Structure Consistency. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 430–447. Springer, Heidelberg (2005)
Loewenheim, L.: Über Mögligkeiten im Relativkalkül. Math. Annalen 76, 228–251 (1915)
Marnette, B., Kuncak, V., Rinard, M.: On algorithms and complexity for sets with cardinality constraints. Technical report, MIT CSAIL (August 2005)
Riis Nielson, H., Nielson, F., Seidl, H.: Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 20–35. Springer, Heidelberg (2002)
Revesz, P.: Quantifier-elimination for the first-order theory of boolean algebras with linear cardinality constraints. In: Benczúr, A.A., Demetrovics, J., Gottlob, G. (eds.) ADBIS 2004. LNCS, vol. 3255, Springer, Heidelberg (2004)
Robertson, N., Seymour, P.D.: Graph minors. II. algorithmic aspects of tree-width. J. Algorithms 7(3), 309–322 (1986)
Schmolze, J.G., Lipkis, T.A.: Classification in the KL-ONE knowledge representation system. In: IJCAI, pp. 330–332 (1983)
Yannakakis, M.: Algorithms for acyclic database schemes. In: VLDB, pp. 82–94 (1981)
Zarba, C.G.: Combining sets with cardinals. J. of Automated Reasoning 34(1) (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Marnette, B., Kuncak, V., Rinard, M. (2007). Polynomial Constraints for Sets with Cardinality Bounds. In: Seidl, H. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2007. Lecture Notes in Computer Science, vol 4423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71389-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-71389-0_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71388-3
Online ISBN: 978-3-540-71389-0
eBook Packages: Computer ScienceComputer Science (R0)