### A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols

### 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 existing deterministic symbolic algorithms.