@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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.},
}