LaSh on Thursday, July 15th

09:00‑10:00 Invited Talk
Location: AT LT5
09:00 Ilkka Niemela (Aalto University)
Integrating Answer Set Programming and Satisfiability modulo Theories

In this talk we consider the problem of integrating answer set programming (ASP) and satisfiability modulo theories (SMT). We discuss a characterization of stable models of logic programs based on Clark's completion and simple difference constraints. The characterization leads to a method of translating a ground logic program to a linear size theory in difference logic, i.e. propositional logic extended with leads to a method of translating a ground logic program to a linear size theory in difference logic, i.e. propositional logic extended with difference constraints between two integer variables, such that stable models of the program correspond to satisfying assignments of the resulting theory in difference logic. Many of the state-of-the-art SMT solvers support directly difference logic. This opens up interesting possibilities. On one hand, any solver supporting difference logic can be used immediately without modifications as an ASP solver for computing stable models of a logic program by translating the program to a theory in difference logic. On the other hand, SMT solvers typically support also other extensions of propositional logic such as linear real and integer arithmetic, fixed-size bit vectors, arrays, and uninterpreted functions. This suggests interesting opportunities to extend ASP languages with such constraints and to provide effective solver support for the extensions. Using the translation an extended language including logic program rules and, for example, linear real arithmetic can be translated to an extension of propositional logic supported by current SMT solvers. We discuss the effectiveness of state-of-the-art SMT solvers as ASP solvers and the possibilities of developing extended ASP languages based on SMT solver technology.

10:30‑12:30 Representation and Solving
Location: AT LT5
10:30 Shahab Tasharrofi and Eugenia Ternovska
Built-in Arithmetic in Knowledge Representation Languages

In previous papers, results about capturing the complexity class NP as model expansion task for languages with built-in arithmetic have been demonstrated. The purpose of this paper is to show implications of those results to the practice of KR, and, in particular, to two system languages of ASP (Gringo and Lparse) and IDP system. In addition, we describe a logic which we call PBINT and show that PBINT provides a good basis for an attractive modelling language. We demonstrate that PBINT allows for compact and natural encodings.

10:49 Emanuele Di Rosa and Enrico Giunchiglia
Evaluating approaches for solving Satisfiability problems with Preferences

The ability to effectively reason in the presence of qualitative preferences on literals or formulas is a central issue in Computer Science and Artificial Intelligence. In the last few years, three procedures have been presented in order to reason with propositional satisfiability (SAT) problems in the presence of additional qualitative preferences on literals or formulas: 1) OPTSAT-HS requires a modification of the branching heuristic of the SAT solver in order to guarantee that the first solution is optimal; 2) OPTSAT-BF computes a sequence of solutions, each guaranteed to be better than the previous ones; 3) SAT&PREF is a combination of the previous approaches, where the branching heuristic is modified ---as in the first approach--- by changing the polarity of the returned literal according to the preference, and then the search continues ---as in the second approach--- looking for better solutions. In this paper we propose an experimental evaluation of the three different approaches by considering a wide variety of problems, having both an empty and a non-empty partial order. The results show that, in terms of cpu time, the SAT&PREF procedure performs better than the two previous approaches on average, and especially on the ``hard'' problems. Moreover, the comparison between the SAT&PREF and OPTSAT-BF approaches, in terms of number of iterations to find an optimal solution, shows that the former significantly reduces the number of intermediate solutions generated, both on random and structured benchmarks.

11:08 Sid Mijnders, Boris de Wilde and Marijn J.H. Heule
Symbiosis of Search and Heuristics for Random 3-SAT

When combined properly, search techniques can reveal the full potential of sophisticated branching heuristics.We demonstrate this observation on the well-known class of random 3-SAT formulae. First, a new branching heuristic is presented, which generalizes existing work on this class. Much smaller search trees can be constructed by using this heuristic. Second, we introduce a variant of discrepancy search, called ALDS. Theoretical and practical evidence support that ALDS traverses the search tree in a near-optimal order when combined with the new heuristic. Both techniques, search and heuristic, have been implemented in the look-ahead solver march. The SAT 2009 competition results show that march is by far the strongest complete solver on random k-SAT formulae.

11:27 Mini-break
11:33 Antti Hyvärinen, Tommi Junttila and Ilkka Niemelä
Partitioning SAT Instances for Distributed Solving

In this paper we study the problem of solving hard propositional satisfiability problem (SAT) instances in a computing grid where communication between parallel running computations is limited. One approach to distributed solving in such an environment is to iteratively partition the instance into computationally easier sub-instances and solve them in parallel. This paper studies different methods for partitioning SAT instances. The methods are compared in a controlled environment and used in a real grid environment for solving several hard SAT instances.

11:52 Broes De Cat and Marc Denecker
DPLL(Agg): an efficient SMT module for aggregates.

The use of aggregates often allow for a compact and natural encoding of many real-life problems. FO(Agg) is an extension of first order logic (FO) with aggregates. In this paper, we present algorithms for a satisfiability checking module for aggregate expressions in the context of the DPLL(T) architecture. We consider among others cardinality, sum and maximum aggregates. The module can be used in all DPLL-based SAT, SMT and ASP solvers. The algorithms have a low complexity. We report on the incorporation of the algorithms in Minisat and the IDP-system and on an experimental evaluation.

12:11 Daniel Le Berre and Pascal Rapicault
Dependency Management for the Eclipse Ecosystem: An Update

One of the strength of Eclipse, the well-known open platform for software development, is its extensibility made possible by the built- in pluggability mechanisms. However those pluggability mechanisms only reveal their full potential when extensions created by others are made easy to distribute and obtain. The purpose of Eclipse p2 project is to build a platform addressing the challenges of distribution and obtention of Eclipse and its extensions, which poses the same dependency management issues than for component based systems. This paper focuses on the dependency management aspect of p2. It describes the boolean optimization encoding used in the next version of Eclipse to be released publicly in June 2010. It focusses on the changes that appeared in the approach taken since its introduction two years ago.

14:00‑15:00 Contributed Talks on Grounding
Location: AT LT5
14:00 Tomi Janhunen
Modular Construction of Ground Logic Programs using LPCAT

In this paper, we view declarative problem solving from the perspective of answer set programming (ASP). The idea is to solve any given problem by formalizing it as a logic program whose answer sets capture the solutions of the problem. In practice such sets are computed using a special-purpose search engine, viz.~an answer set solver, and a ground program obtained by instantiating term variables appearing in the rules of the program. Due to a potential blow-up in the number of rules, the generation of the ground program can become a bottleneck. Since modular program development is gaining more attention in ASP, the objective of this paper to apply modules in the construction of ground logic programs. Our specific goal is to demonstrate that a tool that links together ground program modules can be effective and highly useful when ground programs are generated. In this paper, we provide a formal account of ground program modules and present a link editor, LPCAT, which is designed to be used with SMODELS-compatible grounders and answer set solvers. We study the efficiency of our approach using a benchmark that yields millions of ground rules. Moreover, we illustrate the potential of ground program modules in program transformations.

14:20 Amir Aavani, Xiongnan (Newman) Wu, Eugenia Ternovska and David Mitchell
Grounding Formulas with Complex Terms

Grounding is the creation of a variable-free first-order formula equivalent to a given specification for a combinatorial search problem. Efficient grounding algorithms would help in solving such problems effectively and make advanced solver technology (such as SAT) accessible to a wider variety of users. One promising method for grounding is based on the relational algebra from the field of Database research. We describe the extension of this method to ground formulas of first-order logic extended with arithmetic and aggregate operators. The method allows choice of particular CNF representations of complex constraints to be parameterized easily. We have implemented the methods we describe, and demonstrated that they can be effective in practice.

14:40 Johan Wittocx and Marc Denecker
Grounding FO(ID) with Bounds

Grounding is the task of reducing a given first-order theory T and finite domain to an equivalent propositional theory. It is used as preprocessing step in many logic-based reasoning systems. In this paper, we present a method to improve grounding for FO(ID), the extension of first-order logic with inductive definitions. The method consists of computing bounds for subformulas of T, indicating for which part of the given domain, the truth value of their subformula is the same in every model of T. Bounds can be used to efficiently produce compact groundings. We present both theoretical results and experiments to support this claim.

15:30‑17:00 Invited Talks on Grounding
Location: AT LT5
15:30 Emina Torlak.
Kodkod: A Constraint Solver for Relational Logic
15:50 Gelsomina Catalano, Nicola Leone, and Simona Perri
The Intelligent Grounder of DLV
16:10 Martin Gebser, Roland Kaminski and Torsten Schaub.
The Life of Gringo
16:30 Discussion and Questions