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."

Slightly Boring General Thoughts on Modeling Methodology

Results 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:

Finally, a tremendous resource for many logical languages and solvers is Hakank's Home Page.

Popular posts from this blog

Composed stochastic proof : joint distribution monad as dependent type

Domain types based on probability monads

Explainable models : Asset Allocation example (part 01)