Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

CalCS: SMT Solving for Non-linear Convex Constraints

Pierluigi Nuzzo, Alberto Alessandro Angelo Puggelli, Sanjit A. Seshia and Alberto L. Sangiovanni-Vincentelli

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2010-100
June 22, 2010

http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-100.pdf

Formal verification of hybrid systems can require reasoning about Boolean combinations of nonlinear arithmetic constraints over the real numbers. In this report, we present a new technique for satisfiability solving of Boolean combinations of nonlinear constraints that are convex. Our approach applies fundamental results from the theory of convex programming to realize a satisfiability modulo theory (SMT) solver. Our solver, CalCS, uses a lazy combination of SAT and a theory solver. A key step in our algorithm is the use of complementary slackness and duality theory to generate succinct infeasibility proofs that support conflict-driven learning. Moreover, whenever non-convex constraints are produced from Boolean reasoning, we provide a procedure that generates conservative approximations of the original set of constraints by using geometric properties of convex sets and supporting hyperplanes. We validate CalCS on several benchmarks including examples of bounded model checking for hybrid automata.


BibTeX citation:

@techreport{Nuzzo:EECS-2010-100,
    Author = {Nuzzo, Pierluigi and Puggelli, Alberto Alessandro Angelo and Seshia, Sanjit A. and Sangiovanni-Vincentelli, Alberto L.},
    Title = {CalCS: SMT Solving  for Non-linear Convex Constraints},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2010},
    Month = {Jun},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-100.html},
    Number = {UCB/EECS-2010-100},
    Abstract = {Formal verification of hybrid systems can require reasoning about Boolean combinations of nonlinear arithmetic constraints over the real numbers. In this report, we present a new technique for satisfiability solving of Boolean combinations of nonlinear constraints that are convex. Our approach applies fundamental results from the theory of convex programming to realize a satisfiability modulo theory (SMT) solver. Our solver, CalCS, uses a lazy combination of SAT and a theory solver. A key step in our algorithm is the use of complementary slackness and duality theory to generate succinct infeasibility proofs that support conflict-driven learning. Moreover, whenever non-convex constraints are produced from Boolean reasoning, we provide a procedure that generates conservative approximations of the original set of constraints by using geometric properties of convex sets and supporting hyperplanes. We validate CalCS on several benchmarks including examples of bounded model checking for hybrid automata.}
}

EndNote citation:

%0 Report
%A Nuzzo, Pierluigi
%A Puggelli, Alberto Alessandro Angelo
%A Seshia, Sanjit A.
%A Sangiovanni-Vincentelli, Alberto L.
%T CalCS: SMT Solving  for Non-linear Convex Constraints
%I EECS Department, University of California, Berkeley
%D 2010
%8 June 22
%@ UCB/EECS-2010-100
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-100.html
%F Nuzzo:EECS-2010-100