Constraint answer set programming integrates answer set programming with constraint processing. System EZSMT is a constraint answer set programming tool that utilizes satisfiability modulo theory solvers for search, while providing the benefits of a high-level declarative programming paradigm. EZSMT extends the language of logic programs under answer set semantics with new modeling capabilities. The truly unique feature of this system is its ability to process linear as well as nonlinear constraints simultaneously containing integer and real variables. In the talk we will introduce the kinds of programs one writes in the language of EZSMT and present details on how the solver EZSMT is designed and implemented. We will conclude with the thorough experimental analysis comparing the performance of EZSMT on difficult combinatorial search problems with a variety of systems from distinct automated reasoning communities.
Program Display Configuration
Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Viennachange