Pierluigi Nuzzo and Alberto Alessandro Angelo Puggelli and 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://www2.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},
    Year= {2010},
    Month= {Jun},
    Url= {http://www2.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://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-100.html
%F Nuzzo:EECS-2010-100