A randomized satisfiability procedure for arithmetic and uninterpreted function symbols
| Autor: | George C. Necula, Sumit Gulwani |
|---|---|
| Rok vydání: | 2005 |
| Předmět: |
Randomized algorithm
Satisfiability procedure Linear arithmetic 020207 software engineering 0102 computer and information sciences 02 engineering and technology Uninterpreted function Symbolic computation 01 natural sciences Satisfiability Theoretical Computer Science Computer Science Applications Set (abstract data type) Uninterpreted function symbols Computational Theory and Mathematics 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Probability distribution Arithmetic Difference-map algorithm Algorithm Random variable Mathematics Information Systems |
| Zdroj: | CADE |
| ISSN: | 0890-5401 |
| DOI: | 10.1016/j.ic.2004.10.006 |
| Popis: | 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 algorithm can also be easily adapted to produce proofs for its output. 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect