View: session overviewtalk overviewside by side with other conferences
08:45  LaSh and QUANTIFY Openings SPEAKER: Lash 
09:00  Instantiationbased reasoning, EPR encodings and all that SPEAKER: Konstantin Korovin ABSTRACT. Instantiationbased reasoning aims to combine the expressivity of firstorder logic with the efficiency of propositional and SMT reasoning. Most instantiation based methods are complete for firstorder logic and are especially efficient for the effectively propositional fragment (EPR). It turns out that many problems such as model checking, bitvector reasoning, finite model finding and QBF solving can be succinctly encoded into the EPR fragment. In this talk I will discuss recent developments in instantiationbased reasoning, EPR based encodings and related challenges.

10:45  Metalevel Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development SPEAKER: Joachim Jansen ABSTRACT. Declarative systems aim at solving tasks by running inference engines on a specification, to free its users from having to specify how a task should be tackled. In order to provide such functionality, declarative systems themselves apply complex reasoning techniques, and, as a consequence, the development of such systems can be laborious work. In this paper, we demonstrate that the declarative approach can be applied to develop such systems, by tackling the tasks solved inside a declarative system declaratively. In order to do this, in many cases a metalevel representation of those specifications is required. Furthermore, by using the language of the system for the metalevel representation, it opens the door to bootstrapping: an inference engine can be implemented using the inference it performs itself. One such declarative system is the IDP knowledge base system, based on the language FO(.)IDP, a rich extension of firstorder logic. In this paper, we discuss how FO(.)IDP can support metalevel representations in general and which language constructs make those representations even more natural. Afterwards, we show how metaFO(.)IDP can be applied to bootstrap its model expansion inference engine. We discuss the advantages of this approach: the resulting program is easier to understand, easier to maintain and more flexible. 
11:15  Logical Machinery of Heuristics (Preliminary Report) SPEAKER: Shahab Tasharrofi ABSTRACT. This paper is a preliminary report on a new declarative language that allows the programmer to specify heuristics (problemspecific inference methods) about the problem that is being solved. The heuristics that are defined in our language control and/or change the behavior of the underlying solver. In this way, we are able to attain problemspecific solvers that benefit from both the stateoftheart general inference methods available in generalpurpose solvers, and the problemspecific reasoning methods that are applicable only to this specific problem. 
11:45  Modeling High School Timetabling as PartialWeighted maxSAT SPEAKER: Emir Demirović ABSTRACT. High School Timetabling (HSTT) is a well known and wide spread problem. The problem consists of coordinating resources (e.g. teachers, rooms), time slots and events (e.g. lectures) with respect to various constraints. Unfortunately, HSTT is hard to solve and just finding a feasible solution for simple variants of HSTT has been proven to be NPcomplete. In addition, timetabling requirements vary from country to country and because of this many variations of HSTT exist. Recently, researchers have proposed a general HSTT problem formulation in an attempt to standardize the problem from different countries and school systems. In this paper, for the first time we provide a new detailed modeling of the general HSTT as SAT, in which all constraints are treated as hard constraints. In order to take into account soft constraints, we extend the previous model to Partial Weighted maxSAT. In addition, we present experimental results and compare to other approaches, using both artificial and realworld instances, all of which were taken from the Third International Timetabling Competition 2011 benchmark repository. Our approach gives competitive results and in some cases outperforms the winning algorithm from the competition. 
12:15  Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability SPEAKER: Matti Järvisalo ABSTRACT. Bayesian network structure learning is the wellknown computationally hard problem of finding a directed acyclic graph structure that optimally describes given data. A learned structure can then be used for probabilistic inference. While exact inference in Bayesian networks is in general NPhard, it is tractable in networks with low treewidth. This provides good motivations for developing algorithms for the NPhard problem of learning optimal bounded treewidth Bayesian networks (BTWBNSL). In this work, we develop a novel scorebased approach to BTWBNSL, based on casting BTWBNSL as weighted partial Maximum satisfiability. We demonstrate empirically that the approach scales notably better than a recent exact dynamic programming algorithm for BTWBNSL. Submitted to LaSh’14 for presentation only. Conference version of this paper appears as Jeremias Berg, Matti Järvisalo, and Brandon Malone. Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability. In Proceedings of the 17th International Conference on Artificial Intelligence and Statistics (AISTATS 2014), volume 33 of JMLR Workshop and Conference Proceedings, pages 8695. JMLR, 2014. 
12:45  Depart for Workshop Lunch SPEAKER: Lash ABSTRACT. The LaSh workshop lunch is included in the registration fee. Contact the workshop organizers if you are not registered by wish to join the lunch. 
14:30  Laziness is next to Godliness SPEAKER: Peter Stuckey ABSTRACT. Solving combinatorial optimization problems is hard. There are many 
15:30  Lazy Model Expansion: Interleaving Grounding with Search SPEAKER: Bart Bogaerts ABSTRACT. Finding satisfying assignments for the variables involved in a set of constraints can be cast as a (bounded) model generation problem: search for (bounded) models of a theory in some logic. The state oftheart approach for bounded model generation for rich knowledge representation languages, like Answer Set Programming (ASP), FO(·) and the CSP modeling language Zinc, is groundandsolve: reduce the theory to a ground or propositional one and apply a search algorithm to the resulting theory. An important bottleneck is the blowup of the size of the theory caused by the reduction phase. Lazily grounding the theory during search is a way to overcome this bottleneck. We present a theoret ical framework and an implementation in the context of the FO(·) knowledge representation language. Instead of grounding all parts of a theory, justifications are derived for some parts of it. Given a partial assignment for the grounded part of the theory and valid justifications for the formulas of the nongrounded part, the justifications provide a recipe to construct a complete assignment that satisfies the non grounded part. When a justification for a particular formula becomes invalid during search, a new one is derived; if that fails, the formula is split in a part to be grounded and a part that can be justified. The theoretical framework captures existing approaches for tackling the grounding bottleneck such as lazy clause generation and grounding onthefly, and presents a generalization of the 2watched literal scheme. We present an algorithm for lazy model expansion and integrate it in a model generator for FO(ID), a language extending firstorder logic with inductive definitions. The algorithm is implemented as part of the stateoftheart FO(ID) KnowledgeBase System IDP. Experimental results illustrate the power and generality of the approach.

16:30  The DFLAT System for Dynamic Programming on Tree Decompositions SPEAKER: Stefan Woltran ABSTRACT. Complex reasoning problems over large amounts of data pose a great challenge for computer science. To overcome the obstacle of high computational complexity, exploiting structure by means of tree decompositions has proved to be effective in many cases. However, the implementation of suitable efficient algorithms is often tedious. DFLAT is a software system that combines the logic programming language Answer Set Programming with problem solving on tree decompositions and can serve as a rapid prototyping tool for such algorithms. Since we initially proposed DFLAT, we have made major changes to the system, improving its range of applicability and its usability. In this paper, we present the system resulting from these efforts. 
17:10  CrossTranslating Answer Set Programs SPEAKER: Tomi Janhunen ABSTRACT. Answer set programming (ASP) is a declarative programming paradigm where computation takes place in two phases. The rules of a logic program are first instantiated after which the answer sets of the resulting ground program are computed. There are two mainstream approaches to the search for answer sets: either by using native answer set solvers or by translating ground rules into other kinds of constraints and using other offtheshelf solver technology to perform the search. Over the years, we have developed a number of translations from ASP to Boolean satisfiability (SAT), difference logic, bitvector logic, and mixed integer programming. If a target formalism does not support extended rule types, they have to be normalized before translation. Our latest translation of ASP into SAT modulo acyclicity enables a crosscompilation architecture where the backend formalism is determined by the last translation step generating Clark’s completion extended by acyclicity constraints. In this invited talk, I describe the resulting crosstranslation framework for ASP and discuss lessons learned from the tenyear development of the framework.
