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

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 21, 2018
Accession Number
AD1054419

Entities

People

  • Fernando R. Vale-enriquez

Organizations

  • United States Naval Academy

Tags

Communities of Interest

  • Energy and Power Technologies
  • Human Systems

DTIC Thesaurus Topics

  • Algorithms
  • Collision Avoidance
  • Computational Complexity
  • Computer Programs
  • Computer Science
  • Computers
  • Computing System Architectures
  • Efficiency
  • Elimination
  • Graphs
  • Hybrid Systems
  • Identities
  • Inequalities
  • Numbers
  • Polynomials
  • Real Numbers
  • Trees (Data Structures)

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Operations Research
  • Software Engineering.