Abstract
We present a new randomized algorithm for checking the satisfiability of a conjunction of literals in the combined theory of linear equalities and uninterpreted functions. The key idea of the algorithm is to process the literals incrementally and to maintain at all times a set of random variable assignments that satisfy the literals seen so far. We prove that this algorithm is complete (i.e., it identifies all unsatisfiable conjunctions) and is probabilistically sound (i.e., the probability that it fails to identify satisfiable conjunctions is very small). The algorithm has the ability to retract assumptions incrementally with almost no additional space overhead. The key advantage of the algorithm is its simplicity. We also show experimentally that the randomized algorithm has performance competitive with the existing deterministic symbolic algorithms.
This research was supported in part by the National Science Foundation Career Grant No. CCR-9875171, and ITR Grants No. CCR-0085949 and No. CCR-0081588, and gifts from Microsoft Research. The information presented here does not necessarily reflect the position or the policy of the Government and no official endorsement should be inferred.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ackermann, W.: Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1954)
Bachmair, L., Tiwari, A.: Abstract congruence closure and specializations. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 64–78. Springer, Heidelberg (2000)
Filliâtre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated Canonization and Solving. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 246–249. Springer, Heidelberg (2001)
Gulwani, S., Necula, G.C.: Discovering affine equalities using random interpretation. In: The 30th Annual ACM Symposium on Principles of Programming Languages, pp. 74–84. ACM Press, New York (2003)
Gulwani, S., Necula, G.C.: A randomized satisfiability procedure for arithmetic and uninterpreted function symbols. Technical Report UCB-CS-03-1241. University of California, Berkeley (2003)
Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press, Cambridge (1995)
Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Ruess, H., Shankar, N.: Deconstructing Shostak. In: 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), Washington - Brussels - Tokyo, pp. 19–28. IEEE, Los Alamitos (2001)
Shostak, R.E.: Deciding combinations of theories. Journal of the ACM 31(1), 1–12 (1984)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gulwani, S., Necula, G.C. (2003). A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive