Loading...
Please wait, while we are loading the content...
Similar Documents
From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain (2007)
| Content Provider | CiteSeerX |
|---|---|
| Author | Sebastiani, Roberto |
| Abstract | Abstract. In the last two decades we have witnessed an impressive advance in the efficiency of propositional satisfiability techniques (SAT), which has brought large and previously-intractable problems at the reach of state-of-the-art SAT solvers. Most of this success is motivated by the impressive level of efficiency reached by current implementations of the DPLL procedure. Plain propositional logic, however, is not the only application domain for DPLL. In fact, DPLL has also been successfully used as a boolean-reasoning kernel for automated reasoning tools in much more expressive logics. In this talk I overview a 12-year experience on integrating DPLL with logic-specific decision procedures in various domains. In particular, I present and discuss three main achievements which have been obtained in this context: the DPLL-based procedures for modal and description logics, the lazy approach to Satisfiability Modulo Theories, and Delayed Theory Combination. 1 |
| File Format | |
| Publisher Date | 2007-01-01 |
| Publisher Institution | In Proc. Frontiers of Combining Systems, FroCoS’07, volume 4720 of LNCS |
| Access Restriction | Open |
| Subject Keyword | 12-year Experience Logic-specific Decision Procedure Lazy Approach State-of-the-art Sat Solver Impressive Advance Delayed Theory Combination Exploiting Dpll Dpll-based Procedure Expressive Logic Plain Propositional Logic Various Domain Propositional Satisfiability Technique Automated Reasoning Tool Sat Domain Main Achievement Satisfiability Modulo Theory Boolean-reasoning Kernel Impressive Level Previously-intractable Problem Dpll Procedure Current Implementation |
| Content Type | Text |
| Resource Type | Article |
