SMC: Satisfiability Modulo Convex Optimization

Yasser Shoukry, Pierluigi Nuzzo, Alberto Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, and Paulo Tabuada. SMC: Satisfiability Modulo Convex Optimization. In Proceedings of the 10th International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 19–28, April 2017.

Download

[pdf] 

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.

BibTeX

@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.},
}