Creating a Fast SMT Solver for the Theory of Real Non-Linear Constraints

The satisfiability problem asks whether some given logical formula, for any valid combination of input, can ever evaluate to true. Satisfiability Modulo Theory SMT Solvers are specialized software tools which answer the satisfiability problem for a formula in some theory, such as the theory of real numbers. SMT Solvers are the core of many important tools and fields, such as automated theorem proving, hybrid systems design, formal verification of software, and security design tools. Tools which use SMT Solvers have been shown to be highly effective, but the difficulty of satisfiability solving in certain relevant theories limits the usefulness of SMT Solvers in industry. SMT Solvers use a model which incorporates two different pieces of software, a satisfiability solver and a theory solver. A solver is used to do solving on the logical structure of a problem, and generates a list of logical assumptions which satisfies the structure of the problem.