Solve, Search, or Prove?
Declarative Mathematical Programming
Explicit math models may be harnessed in current (2020) software applications in several broad ways.
Suppose we start from a paper sketch from some application domain, such as finance or planetary science.
Our sketch describes some relationships, including mathematical equalities and inequalities, and
objective functions to be minimized or maximized.
Any group of such relationships may be treated as a model for use in computer analysis.
Our equalities, inequalities and objective functions are defined over some named terms, which are typed. Typing of each term is fixed by our model.
One practical way to study this model is to encode these relationships in a model language for constrained optimization, such as MiniZinc. From the MiniZinc Handbook introduction:
"MiniZinc is a language for specifying constrained optimization and decision problems over integers and real numbers. A MiniZinc model does not dictate how to solve the problem - the MiniZinc compiler can translate it into different forms suitable for a wide range of solvers, such as Constraint Programming (CP), Mixed Integer Linear Programming (MIP) or Boolean Satisfiability (SAT) solvers."
- MiniZinc Website
- MiniZinc Tutorial in chapter 2 of MiniZinc Handbook
- Available Solvers for FlatZinc intermediate form
- Several good open source options, including Google's OR-Tools
- Medal Winning Solvers from past solver competitions
- More Links and Examples from Hakan K.
Slightly Boring General Thoughts on Modeling MethodologyResults from a constrained optimization study provide insight that leads us to ask more questions, which in turn lead us to refine and restate our model (our "what?"). In parallel, we work to validate and clarify our application goals (our "why?"). We may venture in an idiosyncratic experimental direction by applying agent simulation and visualization techniques, or we may seek to operationalize our model in some data analysis system, which may use huge datasets and machine learning techniques. Separately, to deepen our abstract understanding and consequent leverage, we may further formalize our model as a theory, adapted from existing theories.
Formalization with SMT
SMT-LIB offers an incremental pathway to formalization of our relationship model into a theory.
From Wikipedia page for SMT:
"...the satisfiability modulo theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality."
"SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming." "An SMT instance is a generalization of a Boolean SAT instance in which various sets of variables are replaced by predicates from a variety of underlying theories. "
The SMT community has defined a common language, called SMT-LIB:
- SMT-LIB Website (smtlib.org == smtlib.cs.uiowa.edu)
- Syntax Examples
- Theories i.e. formally defined data types
- Language Reference v 2.6 (PDF) 2017
- List of SMT solvers/provers, both current and discontinued
- CVC4 is a prominent open source prover framework, with modified BSD license and some optional GPL dependencies.
- Z3_prover (wikipedia) has MIT license from Microsoft Research RiSE group
- Z3 Tutorial and Browser Demo
- Z3_project and Z3_wiki (github)
- Formal methods group includes Leonardo de Moura, overlaps with Lean and F*
- SMTInterpol offers Craig Interpolation between theories, is all java, with LGPL license.
- Java code samples, illustrating direct connection to SMT solver
- Alt-Ergo is a widely used SMT solver, with some interesting features but a zany licensing model, which leads me to steer clear so far. "Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat."
Finally, a tremendous resource for many logical languages and solvers is Hakank's Home Page.