NDLI: SMC: Satisfiability Modulo Convex Optimization

Please wait, while we are loading the content...

Forward Inner-Approximated Reachability of Non-Linear Continuous Systems

Forward Stochastic Reachability Analysis for Uncontrolled Linear Systems using Fourier Transforms

Optimal Data Rate for State Estimation of Switched Nonlinear Systems

Robust Abstractions for Control Synthesis: Completeness via Robustness for Linear-Time Properties

Convex and Combinatorial Optimization for Dynamic Robots in the Real World

Coupling Policy Iterations with Piecewise Quadratic Lyapunov Functions

Dynamic Periodic Event-Triggered Control for Linear Systems

A Small Gain Theorem for Parametric Assume-Guarantee Contracts

Piecewise - Differentiable Trajectory Outcomes in Mechanical Systems Subject to Unilateral Constraints

On the Polytope Escape Problem for Continuous Linear Dynamical Systems

Controller Synthesis for Reward Collecting Markov Processes in Continuous Space

Path-Complete Graphs and Common Lyapunov Functions

Formal Synthesis of Stabilizing Controllers for Switched Systems

Robust Model Checking of Timed Automata under Clock Drifts

On a Class of Maximal Invariance Inducing Control Strategies for Large Collections of Switched Systems

Relaxed Decidability and the Robust Semantics of Metric Temporal Logic

Structural Analysis of Multi-Mode DAE Systems

SMC: Satisfiability Modulo Convex Optimization

Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable Precision

Invariance Feedback Entropy of Nondeterministic Control Systems

Convex Interpolation Control with Formal Guarantees for Disturbed and Constrained Nonlinear Systems

Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants

Sampling-based Approximate Optimal Control Under Temporal Logic Constraints

Bipedal Robotic Running with DURUS-2D: Bridging the Gap between Theory and Experiment

Sapo: Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems

Statistical Verification of the Toyota Powertrain Control Verification Benchmark

Scheduling of Embedded Controllers Under Timing Contracts

HyLAA: A Tool for Computing Simulation-Equivalent Reachability for Linear Systems

Abnormal Data Classification Using Time-Frequency Temporal Logic

SMC: Satisfiability Modulo Convex Optimization

Content Provider	ACM Digital Library
Author	Sangiovanni-Vincentelli, Alberto L. Tabuada, Paulo Pappas, George J. Nuzzo, Pierluigi Shoukry, Yasser Seshia, Sanjit A.
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 optimization 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 monotone SMC formulas, we can then build and demonstrate effective and scalable decision procedures for problems in hybrid system verification and control, including secure state estimation and robotic motion planning.
Starting Page	19
Ending Page	28
Page Count	10
File Format	PDF
ISBN	9781450345903
DOI	10.1145/3049797.3049819
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2017-04-13
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Satisfiability modulo convex optimization Satisfiability modulo theories Convex programming
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Satisfiability Modulo Theories (2008)

An Introduction to Satisfiability Modulo Theories

Modulo theories solver opensmt [2]. Satisfiability modulo theories.

Symbolic optimization with SMT solvers

Smten with satisfiability-based search

Synthesis modulo recursive functions

Satisfiability modulo theories.

Finding inductive invariants using satisfiability modulo theories and convex optimization

SMC: Satisfiability Modulo Convex Programming

SMC: Satisfiability Modulo Convex Optimization

Similar Documents

Satisfiability Modulo Theories (2008)

An Introduction to Satisfiability Modulo Theories

Modulo theories solver opensmt [2]. Satisfiability modulo theories.

Symbolic optimization with SMT solvers

Smten with satisfiability-based search

Synthesis modulo recursive functions

Satisfiability modulo theories.

Finding inductive invariants using satisfiability modulo theories and convex optimization

SMC: Satisfiability Modulo Convex Programming

SMC: Satisfiability Modulo Convex Optimization