A randomized satisfiability procedure for arithmetic and uninterpreted function symbols

DOI10.1016/J.IC.2004.10.006MaRDI QIDQ2486581zbMATH OpenOpenAlexFDO

Authors Sumit Gulwani, George C. Necula

Publication date 5 August 2005

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2004.10.006

zbMATH Keywords

Linear arithmeticRandomized algorithmSatisfiability procedureUninterpreted function symbols

Mathematics Subject Classification ID

Randomized algorithms (68W20)

Recommendations

• A randomized satisfiability procedure for arithmetic and uninterpreted function symbols.
• Solving the satisfiability problem by using randomized approach
• scientific article; zbMATH DE number 2084740
• Probabilistic performance of a heurisic for the satisfiability problem
• An exact and a randomized approach for the satisfiability problem

Cites work

• Computer Aided Verification
• Deciding Combinations of Theories
• Discovering affine equalities using random interpretation
• scientific article; zbMATH DE number 1798183 (Why is no real title available?)
• scientific article; zbMATH DE number 819814 (Why is no real title available?)
• Simplification by Cooperating Decision Procedures
• Solvable cases of the decision problem

Cited in

(1)

• A randomized satisfiability procedure for arithmetic and uninterpreted function symbols.

Describes a project that uses

Uses Software

• CVC Lite

This page was built for publication: A randomized satisfiability procedure for arithmetic and uninterpreted function symbols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2486581)