Picture (c) Michael Morak
University of Nebraska at Omaha
Abstract: Constraint answer set programming integrates ASP with constraint processing enabling powerful declarative encodings of complex combinatorial search problems. System EZSMT is an extensible constraint answer set programming framework that advances the translational approach to CASP solving. It utilizes satisfiability modulo theory solvers for search, while providing the benefits of a high-level declarative programming paradigm. In other words, it can be seen as a tool that simplifies the use of SMT solvers by enabling it with logic programming interface. In addition, EZSMT extends the language of logic programs under answer set semantics with new modeling capabilities. Indeed, the unique feature of this system is its ability to process linear constraints simultaneously containing integer and real variables. The system provides a robust platform for future extensions and theoretical exploration within the CASP domain. In particular, it builds upon the developments in the CLINGO 5 series that promotes the extensibility philosophy. The CLINGO 5 system provides means to elaborate the specifications for new kinds of constructs to be incorporated for processing within its grounding tool GRINGO. EZSMT takes advantage of this feature. In the talk we will discuss theoretical and practical underpinnings of the framework as well as present some benchmark information positioning the system among its peers.
University of Potsdam
Abstract: TBA