SMC: Satisfiability Modulo Convex Programming
SMC: Satisfiability Modulo Convex Programming
复制标题
SMC：可满足性模凸规划
DOI：
10.1109/jproc.2018.2849003
复制
发表时间：
2018
影响因子：
20.6
通讯作者：
Tabuada, Paulo
中科院分区：
文献类型：
--
作者：
Shoukry, Yasser;Nuzzo, Pierluigi;Sangiovanni-Vincentelli, Alberto L.;Seshia, Sanjit A.;Pappas, George J.;Tabuada, Paulo
网络物理系统（CPS）的设计需要能够有效推理离散模型之间交互的方法和工具，例如，表示“网络”组件的行为，以及物理过程的连续模型。布尔方法，如可满足性（SAT）解决是成功地解决大型组合搜索问题的设计和验证的硬件和软件组件。另一方面，控制、通信、信号处理和机器学习中的问题通常依赖于凸规划作为强大的解决引擎。然而，尽管这些办法有其长处，但这两种办法都不能孤立地适用于国别方案。在本文中，我们提出了一个新的可满足性模凸规划（SMC）的框架，集成了SAT求解和凸优化，有效地原因布尔和凸约束在同一时间。利用布尔和非线性真实的谓词上的一类逻辑公式的性质，称之为单调可满足模凸公式，其可满足性可以通过有限个凸规划来检验.懒惰的可满足性模理论（SMT）的范式，我们开发了一个新的决策过程单调SMC公式，协调SAT解决和凸规划提供一个令人满意的分配或确定该公式是不可满足的。我们的协调方案中的一个关键步骤是高效地生成简洁的不可行性证明，以支持冲突驱动的学习和加速搜索。我们展示了我们的方法在不同的CPS设计问题，包括航天器对接使命控制，机器人运动规划，安全状态估计。我们表明，SMC可以处理更复杂的问题的情况下，比国家的最先进的替代技术的基础上SMT解决和混合整数凸规划。
The design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of “cyber” components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step in our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming.
登录
查看更多内容
DOI：
10.1007/978-3-642-12002-2_8
发表时间：
2010-03
期刊：
--
影响因子：
--
作者：
A. Cimatti;Anders Franzén;A. Griggio;R. Sebastiani;Cristian Stenico
通讯作者：
A. Cimatti;Anders Franzén;A. Griggio;R. Sebastiani;Cristian Stenico
混合控制与估计的航天器基准问题
DOI：
10.1109/cdc.2016.7798765
发表时间：
2016
期刊：
2016 IEEE 55th Conference on Decision and Control (CDC)
影响因子：
--
作者：
Christopher Jewison;R. Erwin
通讯作者：
R. Erwin
影响因子：
20.6
作者：
S. Seshia
通讯作者：
S. Seshia
线性系统和安全线性时间时序逻辑的规范引导控制器综合
影响因子：
6.8
作者：
M. Rungger;M. Mazo;P. Tabuada
通讯作者：
P. Tabuada
基于惰性 SMT 的可扩展运动规划
DOI：
10.1109/cdc.2016.7799298
发表时间：
2016
期刊：
2016 IEEE 55th Conference on Decision and Control (CDC)
影响因子：
--
作者：
Yasser Shoukry;P. Nuzzo;I. Saha;A. Sangiovanni;S. Seshia;George Pappas;P. Tabuada
通讯作者：
P. Tabuada