@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@inproceedings{shoukry-hscc17,
author = {Yasser Shoukry and Pierluigi Nuzzo and Alberto Sangiovanni-Vincentelli and Sanjit A. Seshia and George J. Pappas and Paulo Tabuada},
title = {SMC: Satisfiability Modulo Convex Optimization},
booktitle = {Proceedings of the 10th International Conference on Hybrid Systems: Computation and Control (HSCC)},
month = "April",
year = {2017},
pages = {19--28},
abstract = {We address the problem of determining the satisfiability of
a Boolean combination of convex constraints over the real
numbers, which is common in the context of hybrid system
verification and control. We first show that a special
type of logic formulas, termed monotone Satisfiability Modulo
Convex (SMC) formulas, is the most general class of
formulas over Boolean and nonlinear real predicates that reduce
to convex programs for any satisfying assignment of
the Boolean variables. For this class of formulas, we develop
a new satisfiability modulo convex procedure that uses a
lazy combination of SAT solving and convex programming
to provide a satisfying assignment or determine that the formula
is unsatisfiable. Our approach can then leverage the
efficiency and the formal guarantees of state-of-the-art algorithms
in both the Boolean and convex analysis domains.
A key step in lazy satisfiability solving is the generation of
succinct infeasibility proofs that can support conflict-driven
learning and decrease the number of iterations between the
SAT and the theory solver. For this purpose, we propose
a suite of algorithms that can trade complexity with the
minimality of the generated infeasibility certificates. Remarkably,
we show that a minimal infeasibility certificate
can be generated by simply solving one convex program for
a sub-class of SMC formulas, namely ordered positive unate
SMC formulas, that have additional monotonicity properties.
Perhaps surprisingly, ordered positive unate formulas
appear themselves very frequently in a variety of practical
applications. By exploiting the properties of SMC formulas,
we can then build and demonstrate e.ective and scalable
decision procedures for several problems in hybrid system
verification and control, including secure state estimation
and robotic motion planning.},
}