| LaSh06 | Search and Logic: Answer Set Programming and SAT Seattle, August 16, 2006 |
LaSh on Wednesday, August 16th
Session 1: Opening and Invited Talk (08:50‑09:50)
| 08:50‑09:00 |
Opening Remarks
|
| 09:00‑09:50 | Mirek Truszczynski (University of Kentucky) Knowledge representation languages --- a programmer's interface to satisfiability [pdf] ... |
Session 2: Contributed Talks (09:50‑10:30)
| 09:50‑10:10 | Enrico Giunchiglia
(University of Genova) Yuliya Lierler (Institut fur Informatik, Erlangen-Nurnberg-Universitat) Marco Maratea (Department of Mathematics, University of Calabria) Armando Tacchella (DIST - University of Genova) Experiments with SAT-based Answer Set Programming Answer Set Programming (ASP) emerged in the late 1990s as a new logic programming paradigm which has been successfully applied in various application domains. Propositional satisfiability (SAT) is one of the most studied problems in Computer Science. ASP and SAT are closely related: Recent works have studied their relation, and efficient SAT-based ASP solvers (like ASSAT and Cmodels) exist. In this paper we report about (i) the extension of the basic procedures in {\cmodels} in order to incorporate the most popular SAT reasoning strategies, and (ii) an extensive comparative analysis involving also other state-of-the-art answer set solvers. The experimental analysis points out, besides the fact that Cmodels is highly competitive, that the reasoning strategies that work best on ``small but hard'' problems are ineffective on ``big but easy'' problems and vice-versa. |
| 10:10‑10:30 | Maarten Mariën (K.U.Leuven) Johan Wittocx (K.U. Leuven) Marc Denecker (K.U.Leuven) The IDP framework for declarative problem solving We present a framework for declarative problem solving, called the IDP framework. Based on the model expansion problem for ID-Logic, it is a widely applicable computational paradigm. We provide examples to support this claim, and derive a general methodology of modelling in IDP. Also, we compare this methodology to that of another important declarative framework, namely Answer Set Programming. Finally, we report on an implementation of IDP. |
Break (10:30‑11:00)
Session 3: Tutorials (11:00‑12:30)
Lunch break (12:30‑14:00)
Session 4: Invited Talk (14:00‑14:50)
| 14:00‑14:50 | Henry Kautz (University of Washington) Deconstructing Planning as Satisfiability [ppt] ... |
Session 5: Contributed Talks (14:50‑15:30)
| 14:50‑15:10 | Martin Gebser
(University of Potsdam) Torsten Schaub (University of Potsdam) Characterizing ASP Inferences by Unit Propagation Model-based reasoning has become an attractive tool for automatic problem solving. In particular, the area of satisfiability checking (SAT) has undergone impressive computational progress over the last decade. Modern SAT solvers are able to handle huge problems evolving from various industrial applications, such as model checking, hardware and software verification, logistics, and planning. Answer set programming (ASP) can be regarded as the nonmonotone counterpart of SAT. In ASP, problems are encoded as sets of rules, called logic programs. ASP solvers, like dlv, nomore++, and smodels, are then used to compute the answer sets or stable models of a program, corresponding to solutions of the original problem. Beyond being model-based, computational approaches to SAT and ASP have many aspects in common. In fact, the basic algorithms of ASP solvers are very similar to the Davis-Logemann-Loveland procedure (DLL) for SAT. The major difference lies in the inference rules, which are more sophisticated for ASP. In this paper, we provide a generic framework, based on CSP concepts, that allows us to view ASP inferences as forms of unit propagation. We develop fully declarative characterizations of ASP solvers nomore++ and smodels in terms of constraints. Thereby, we shed new light on ASP solving techniques, considered before as very different from SAT and CSP approaches. |
| 15:10‑15:30 | John Schlipf
(University of Cincinnati) Ryan Flannery (University of Cincinnati) Unfounded Sets and Autarkies We identify a new relationship between classical and non-monotonic logic; specifically, we relate autarkies for CNF formulas [Monien and Speckenmeier] to unfounded sets for logic normal logic programs [Van Gelder, Ross, Schlipf]. Using a natural way to construct a logic program P_C from a CNF formula C, we show that that the all-negative autarkies for C are exactly the unfounded sets of P_C. In CNF satisfiability there is no preference for setting variables true or false. Thus polarities of some variables may be flipped in a CNF formula C, giving different logic programs P_C and thus different unfounded sets. Seeking autarkies has been pursued in CNF satisfiability engines; we were inspired by Sean Weaver's adding of ``safe'' constraints: new constraints known not to destroy consistency. By using unfounded sets as above, we have a different, and generally more aggressive, way of seeking autarkies. Our hope is that this approach can also give a way to use failed stochastic local searches for satisfying truth assignments to find autarkies. |
Break (15:30‑16:00)
Session 6: Contributed Talks (16:00‑17:20)
| 16:00‑16:20 | Murray Patterson
(Simon Fraser University) Yongmei Liu (Simon Fraser University) Eugenia Ternovska (Simon Fraser University) Arvind Gupta (Simon Fraser University) Grounding for Model Expansion in $k$-Guarded Formulas In~\cite{Mitchell/Ternovska:2005:LCC,Mitchell/Ternovska:2005:AAAI}, the authors propose a constraint programming framework based on classical logic extended with inductive definitions. They formulate a search problem as the problem of model expansion (MX), which is model checking for $\exists$SO where the goal is to find a witness for $\exists$. Their long-term goal is to produce practical tools to solve combinatorial search problems, especially those in $\NP$. In this framework, the problem is encoded in a logic, an instance of the problem is represented by a finite structure, and a solver generates solutions to the problem. This approach relies on propositionalisation of high-level specifications, and on the efficiency of modern SAT solvers. Here, we propose an efficient algorithm which combines grounding with partial evaluation. Since the MX framework is based on classical logic, we are able to take advantage of known results for the so-called guarded fragments and their generalizations. In the case of $k$-guarded formulas under a natural restriction, the algorithm performs much better than naive grounding by relying on connections between $k$-guarded formulas and tree decompositions. |
| 16:20‑16:40 | Johannes Oetsch (Technische Universitaet Wien) Martina Seidl (Technische Universitaet Wien) Hans Tompits (Vienna University of Technology) Stefan Woltran (Technische Universitaet Wien) ccT: A Tool for Checking Advanced Correspondence Problems in Answer-Set Programming In previous work, a general framework for specifying correspondences between logic programs under the answer-set semantics has been defined. The framework allows to define different notions of equivalence, including well-known notions like strong equivalence as well as refined ones based on the projection of answer sets, where not all parts of an answer set are of relevance (like, e.g., removal of auxiliary letters). In the general case, deciding the correspondence of two programs lies on the fourth level of the polynomial hierarchy and therefore this task can (presumably) not be efficiently reduced to answer-set programming. In this paper, we describe an implementation to verify program correspondences in this general framework. The system, called ccT, relies on linear-time constructible reductions to quantified propositional logic using extant solvers for the latter language as back-end inference engines. We provide some preliminary performance evaluation which shed light on some crucial design issues. |
| 16:40‑17:00 | Lengning Liu
(University of Kentucky) Mirek Truszczynski (University of Kentucky) Solving Optimization Problems with Boolean Combinations of Pseudo-boolean Constraints (a preliminary report) We study the optimization problems where the constraints are boolean combinations of pseudo-boolean constraints and the objective function is a linear function with integer coefficients and 0-1 variables. We call such optimization problems PL(PB) optimization problems. PL(PB) optimization problems generalize the well known pseudo-boolean optimization problems where each constraint is a single pseudo-boolean constraint. We propose a method that solves PL(PB) optimization problems via a stochastic local search PL(PB) solver called wsat(plpb). Our method iteratively queries wsat(plpb) to improve the value of the objective functions. In addition to the linear search, which most methods that solve pseudo-boolean optimization problems use, our method provides an option that uses a combination of linear and binary search, which guarantees that exactly two unsatisfiable instances need to be decided during the search. We perform experimental study on our implementation. We compare our method to existing pseudo-boolean optimizers on a set of instances. Transformation is needed as those optimizers do not accept boolean combinations of pseudo-boolean constraints. The result shows that, except for one instance, our method is uniformly better than existing methods on the rest of the instances. |
Session 7: Panel and Discussion (17:20‑18:00)
| 17:20‑18:00 |
Panel: J. Franco, V. Marek, D. Mitchell, I. Niemela, E. Ternovska (Chair)
|
