• Home
• Tutorial
• Examples
• Downloads

Satisfiability Modulo Convex programming

The central difficulty in analyzing and designing cyber-physical systems is the very different nature of the technical tools used to analyze continuous/physical dynamics (e.g., real analysis) and discrete/cyber dynamics (e.g., combinatorics). In complex, high-dimensional systems, a vast discrete/continuous space must be searched under constraints that are often nonlinear. Developing efficient techniques to perform this task is, therefore, crucial to substantially enhance our ability to design and analyze cyber-physical systems.

Constraint Programming (CP) and Mixed Integer Programming (MIP) have emerged over the years as means for addressing many of the challenges posed by cyber-physical systems. Rooted in Satisfiability (SAT) solving and, more recently, Satisfiability Modulo Theory (SMT) solving, CP relies on logic-based methods such as domain reduction and constraint propagation to accelerate the search. Modern SAT and SMT solvers can efficiently find satisfying valuations of very large propositional formulas with complex Boolean structure, including combinations of atoms from various decidable theories, such as lists, arrays, bit vectors, linear integer arithmetic, and linear real arithmetic. However, while SMT solving for generic nonlinear theories over the reals is undecidable in general, algorithms and tools that can address useful fragments of these theories with solid guarantees of correctness and scalability have only recently started to appear.

MIP-based approaches encode, instead, a Boolean combination of nonlinear constraints into a conjunction of mixed integer constraints and solve it by leveraging numerical algorithms based on branch-and-bound and cutting-plane methods. When applied to mixed integer convex constraints, optimization-based techniques tend to be efficient if the Boolean structure of the problem is simple. Moreover, convex programming is extensively used as the core engine in a variety of applications, ranging from control design to communications, from electronic design to data analysis and modeling. However, encoding some logic operations, such as disjunction and implication, into mixed integer constraints usually requires approximations and heuristic techniques, such as the well-known "big-M" method, which may eventually affect the correctness of the solution.

Monotone SMC Formulas

quantifier-free formulas in conjunctive normal form, with atomic propositions ranging over propositional variables and convex constraints. Formally: \begin{align*} formula & ::= \{clause \ \wedge\} ^* clause \notag \\ clause & ::= (\{literal \ \vee\} ^* literal) \ | \ pB\_predicate \notag\\ literal & ::= bool\_var \ |\ \neg bool\_var \ | \ \top \ | \ \bot \ | \ conv\_constraint \ \\ conv\_constraint & ::= equation\ |\ inequality \notag \\ equation & ::= af\!fine\_function = \ 0 \notag \\ inequality & ::= convex\_function \ relation \ 0 \notag \\ relation & ::= \ <\ | \ \leq \notag \end{align*} Monotone SMC Formulas are the most general class of formulas over Boolean and nonlinear real arithmetic predicates that can be solved via a finite number of convex programs. SatEX is a novel new procedure that uses a lazy combination of SAT solving and convex programming to provide a satisfying assignment for monotone SMC formula or determine that the formula is unsatisfiable.

References:

(1) "SMC: Satisfiability Modulo Convex Optimization"

Yasser Shoukry, Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, and Paulo Tabuada, HSCC 2017.

Acknowledgment:

This work was partially sponsored by:

• TerraSwarm Research Center, one of six centers administered by the STARnet phase of the Focus Center Research Program (FCRP) a Semiconductor Research Corporation program sponsored by MARCO and DARPA,
• NSF project "ExCAPE: Expeditions in Computer Augmented Program Engineering"
• NSF project "CPS: Frontier: Collaborative Research: Correct-by-Design Control Software Synthesis for Highly Dynamic Systems" (award 1239085),

The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of NSF, DARPA or the U.S. Government.

latest news

2 Feb. 2017
SatEX is submitted for repetability evaluation at HSCC 2017

12 Dec. 2016
Our paper is accepted for publication at HSCC 2017.