Chapter 26. Approximate Model Counting

Model counting, or counting solutions of a set of constraints, is a fundamental problem in Computer Science with diverse applications. Since exact counting is computationally hard (#P complete), approximate counting techniques have received much attention over the past few decades. In this chapter, we focus on counting models of propositional formulas, and discuss in detail universal-hashing based approximate counting, which has emerged as the predominant paradigm for state-of-the-art approximate model counters. These counters are randomized algorithms that exploit properties of universal hash functions to provide rigorous approximation guarantees, while piggybacking on impressive advances in propositional satisfiability solving to scale up to problem instances with a million variables. We elaborate on various choices in designing such approximate counters and the implications of these choices. We also discuss variants of approximate model counting, such as DNF counting and weighted counting.

Solving Sum-of-Costs Multi-Agent Pathfinding with Answer-Set Programming

Solving a Multi-Agent Pathfinding (MAPF) problem involves finding non-conflicting paths that lead a number of agents to their goal location. In the sum-of-costs variant of MAPF, one is also required to minimize the total number of moves performed by agents before stopping at the goal. Not surprisingly, since MAPF is combinatorial, a number of compilations to Satisfiability solving (SAT) and Answer Set Programming (ASP) exist. In this paper, we propose the first family of compilations to ASP that solve sum-of-costs MAPF over 4-connected grids. Unlike existing compilations to ASP that we are aware of, our encoding is the first that, after grounding, produces a number of clauses that is linear on the number of agents. In addition, the representation of the optimization objective is also carefully written, such that its size after grounding does not depend on the size of the grid. In our experimental evaluation, we show that our approach outperforms search- and SAT-based sum-of-costs MAPF solvers when grids are congested with agents.

A MaxSAT-Based Framework for Group Testing

The success of MaxSAT (maximum satisfiability) solving in recent years has motivated researchers to apply MaxSAT solvers in diverse discrete combinatorial optimization problems. Group testing has been studied as a combinatorial optimization problem, where the goal is to find defective items among a set of items by performing sets of tests on items. In this paper, we propose a MaxSAT-based framework, called MGT, that solves group testing, in particular, the decoding phase of non-adaptive group testing. We extend this approach to the noisy variant of group testing, and propose a compact MaxSAT-based encoding that guarantees an optimal solution. Our extensive experimental results show that MGT can solve group testing instances of 10000 items with 3% defectivity, which no prior work can handle to the best of our knowledge. Furthermore, MGT has better accuracy than the LP-based approach. We also discover an interesting phase transition behavior in the runtime, which reveals the easy-hard-easy nature of group testing.

Pitfalls and Best Practices in Algorithm Configuration

Good parameter settings are crucial to achieve high performance in many areas of artificial intelligence (AI), such as propositional satisfiability solving, AI planning, scheduling, and machine learning (in particular deep learning). Automated algorithm configuration methods have recently received much attention in the AI community since they replace tedious, irreproducible and error-prone manual parameter tuning and can lead to new state-of-the-art performance. However, practical applications of algorithm configuration are prone to several (often subtle) pitfalls in the experimental design that can render the procedure ineffective. We identify several common issues and propose best practices for avoiding them. As one possibility for automatically handling as many of these as possible, we also propose a tool called GenericWrapper4AC.

Interactive and automated proofs for graph transformations

This article explores methods to provide computer support for reasoning about graph transformations. We first define a general framework for representing graphs, graph morphisms and single graph rewriting steps. This setup allows for interactively reasoning about graph transformations. In order to achieve a higher degree of automation, we identify fragments of the graph description language in which we can reduce reasoning about global graph properties to reasoning about local properties, involving only a bounded number of nodes, which can be decided by Boolean satisfiability solving or even by deterministic computation of low complexity.

Multi-agent Epistemic Planning with Common Knowledge

In the past decade, multi-agent epistemic planning has received much attention from both dynamic logic and planning communities. Common knowledge is an essential part of multi-agent modal logics, and plays an important role in coordination and interaction of multiple agents. However, existing implementations of multi-agent epistemic planning provide very limited support for common knowledge, basically static propositional common knowledge. Our work aims to extend an existing multi-agent epistemic planning framework based on higher-order belief change with the capability to deal with common knowledge. We propose a novel normal form for multi-agent KD45 logic with common knowledge. We propose satisfiability solving, revision and update algorithms for this normal form. Based on our algorithms, we implemented a multi-agent epistemic planner with common knowledge called MEPC. Our planner successfully generated solutions for several domains that demonstrate the typical usage of common knowledge.