ABSTRACT. When solving a combinatorial problem, the formulation or model of the problem is critical to the efficiency of the solver. Automating the modelling process has long been of interest because of the expertise and time required to produce an effective model of a given problem. I describe a method to automatically produce constraint models from a problem specification written in the abstract constraint specification language Essence. The approach is to incrementally refine the specification into a concrete model by applying a chosen refinement rule at each step. Any non-trivial specification may be refined in multiple ways, creating a space of models from which to choose.

The handling of symmetries is a particularly important aspect of automated modelling. Many combinatorial optimisation problems contain symmetry, which can lead to redundant search. If a partial assignment is shown to be invalid, we are wasting time if we ever consider a symmetric equivalent of it. A particularly important class of symmetries are those introduced by the constraint modelling process: modelling symmetries. I show how modelling symmetries may be broken automatically as they enter a model during refinement, obviating the need for an expensive symmetry detection step following model formulation.

This approach is implemented in a system called Conjure. The models produced by Conjure are compared to hand-written constraint models from the literature that are known to be effective. Empirical results confirm that Conjure can reproduce successfully the kernels of the constraint models of several benchmark problems found in the literature.

ABSTRACT. Linear constraints on infinite trees arise in object-oriented resource analysis, when inferring resource types for programs similar to (a fragment of) Java. These types encode the heap space usage of programs, and one can calculate an upper bound on it using the constraint solutions. I will explain the logic and the meaning of the constraints with examples and briefly describe their role in program analysis. I then focus on the decision procedures for both list and tree constraints. After presenting the ideas for the list case, I will generalize them to trees and point out the difficulties that appear there and how they are treated.

ABSTRACT. A well-known algorithmic meta-theorem states that every graph property expressible by a monadic second-order (MSO in short) sentence possibly using edge set quantifications can be checked in linear time for graphs of bounded tree- width; furthermore, every graph property expressible by an MSO sentence not using edge set quantifications can be checked in linear time for graphs of bounded clique-width given by an appropriate algebraic term. The standard proofs construct from the sentences and the given bounds on tree-width or clique-width automata intended to run on tree-decompositions or clique-width terms. However, they have so many states that these constructions are not usable in practice. This is unavoidable by Frick and Grohe. To overcome this difficulty in cases that are not "toy examples", we have introduced fly-automata that do not store states and transitions but compute them whenever needed. They have been implemented and tested, in particular for checking colorability and so-called acyclic colorability. A subset of the implemented functionalities will be demonstated by using a web interface in the first part of the lecture.

ABSTRACT. In this talk, we first give an overview on solving #SAT using parameterized algorithms that exploit small treewidth. The problem #SAT asks to output the number of solutions of a Boolean formula. If the treewidth of a graph representation of the given formula is fixed, one can solve #SAT efficiently by means of a dynamic programming algorithm on tree decompositions.

However, finding an optimal tree decomposition is itself an NP-hard problem. Existing methods for finding tree decompositions of small width either (a) yield optimal tree decompositions but are applicable only to small instances or (b) are based on greedy heuristics which often yield tree decompositions that are far from optimal. We propose a new method that combines (a) and (b), where a heuristically obtained tree decomposition is improved locally. We sketch results of an experimental evaluation of our new method.

Further, we present a novel architecture of dynamic programming for efficient parallel execution on the GPU. We provide thorough experiments and compare the runtime of our system with state-of-the-art solvers. Our results are encouraging if instances have treewidth at most 30, which is the case for the majority of counting benchmark instances.

ABSTRACT. We present a new decision procedure for the logic WS1S. It originates from the classical approach, which first builds an automaton accepting all models of a formula and then tests whether its language is empty. The main novelty is to test the emptiness on the fly, while constructing a symbolic, term-based representation of the automaton, and prune the constructed state space from parts irrelevant to the test. The pruning is done by a generalization of two techniques used in antichain-based language inclusion and universality checking of finite automata: subsumption and early termination. The richer structure of the WS1S decision problem allows us, however, to elaborate on these techniques in novel ways. Our experiments show that the proposed approach can in many cases significantly outperform the classical decision procedure (implemented in the MONA tool) as well as recently proposed alternatives.

ABSTRACT. ESSENCE is a formal language for specifying combinatorial (decision or optimisation) problems at a high level of abstraction. It is the result of our attempt to design a formal language that enables abstract problem specifications that are similar to rigorous specifications that use a mixture of natural language and discrete mathematics, such as those that appear in Garey and Johnson's catalog of NP-complete problems. This talk presents the design of ESSENCE - focusing on its abstraction features - the motivation behind it and why it can be useful to the wider LaSh community.

ABSTRACT. Dynamic Programming solves optimization problems over an exponential search space in polynomial time. Bellman's Principle of Optimality is its mathematical prerequisite. Recursion and tabulation of intermediates are its essential ingredients to achieve efficiency. While these basic principles are well- understood, still such algorithms are intricate to develop and hopeless to debug. An optimal solution to a dynamic programming (DP) problem is identified by its optimal score. Recording the function calls which compute a score value gives us an uninterpreted term that can be understood as data structure representing the solution – and the algebra of all such terms (optimal or not) represents the search space for the given problem input. With ICOREs, we describe the search universe of a DP problem by a language of abstract terms. A set of rewrite rules relates the solutions to the problem input for which they constitute the search space. An evaluation algebra collapses solutions into their associated scores. A choice function operates on scores to identify optimal solutions. The issues of search, scoring and optimization are prefectly separated. These four constituents specify a DP problem in a perfectly declarative way. All we need now is a compiler to construct code that computes the inverse of the rewrite relation (starting from the input), evaluates and tabulates partial solutions, and applies Bellman's optimization rule along the way.

ABSTRACT. Courcelle’s Theorem states that every problem definable in Monadic Second- Order logic can be solved in linear time on structures of bounded treewidth, for example, by constructing a tree automaton that recognizes or rejects a tree decomposition of the structure. Existing, optimized software like the MONA tool can be used to build the corresponding tree automata, which for bounded treewidth are of constant size. Unfortunately, the constants involved can become extremely large – every quantifier alternation requires a power set construction for the automaton. Here, the required space can become a problem in practical applications. In this paper, we present a novel, direct approach based on model checking games, which avoids the expensive power set construction. Experiments with an implementation are promising, and we can solve problems on graphs where the automata-theoretic approach fails in practice.

ABSTRACT. We describe a formalism for combining heterogeneous components -- web services, knowledge bases, declarative specifications such as Integer Linear Programs, Constraint Satisfaction Problems, Answer Set Programs etc.. The formalism is a family of logics, where atomic modules -- formally, classes of structures -- are combined using operations of extended Relational algebra, or, equivalently, first-order logic with a least fixed point construct. Inputs and outputs of atomic modules indicate directionality of the information flows. As a result of this small addition, an interesting modal logic, similar to Dynamic Logic, is obtained. Many binary operations, including those studied in the calculi of binary relations and the standard constructs of imperative programming become definable. We study the properties of this logic and identify an efficient fragment where the main computational task is solvable in deterministic polynomial time.

ABSTRACT. Weak monadic second-order logic of one successor (WS1S) is a simple and natural formalism for specifying regular properties. WS1S is decidable, although the decision procedure's complexity is non-elementary. Typically, decision procedures for WS1S exploit the logic-automaton connection, i.e., they escape the simple and natural formalism by translating formulas into equally expressive but less concise regular structures such as finite automata. In this talk, I will present a decision procedure for WS1S that stays within the logical world by directly operating on formulas. The key operation is the derivative of a formula, modeled after Brzozowski's derivatives of regular expressions. The presented decision procedure has been formalized and proved correct in the interactive proof assistant Isabelle.