ABSTRACT. Critical software should be verified. But how to handle the situation when a proof of functional correctness could not be established? In this case, an assessment of the software is required to estimate the risk of using the software.

In this talk, we present our work on the quantification of C program reliability. Our formal approach measures the reliability of a program in terms of its adherence to a provided functional specification. Our implementation can handle bounded C programs precisely where the functionality is specified through assumptions and assertions in the source code. Following a preparatory program transformation, we use a combination of techniques for software bounded model checking and model counting to obtain quantitative results. This approach allows us to count and categorize the possible runs of the software, permitting the computation of the software's reliability as the share of failing program runs. We evaluated our implementation on a representative set of 24 (deterministic and non-deterministic) C programs and showed differences in performance between an exact and an approximate model counter. The evaluation also led to the publication of a total of 123 benchmark instances for projected model counting.

After summarizing the results of our paper, we briefly present future pathways to increase the efficiency and applicability of our approach.

ABSTRACT. We present an extensive study of methods for exactly solving stochastic constraint (optimisation) problems (SCPs). Each of these methods combines weighted model counting (WMC) with constraint satisfaction and optimisation. They use knowledge compilation to address the model counting problem; subsequently, either a constraint programming (CP) solver or mixed integer programming (MIP) solver is used to solve the overall SCP. We first explore a method that is generic and decomposes constraints on probability distributions into a multitude of smaller, local constraints. For the second method, we show that many probability distributions in real-world SCPs have a monotonic property, and how to exploit that property to develop a global constraint. We discuss theoretical (dis)advantages of each method, with a focus on methods that employ ordered binary decision diagrams (OBDDs) to encode the probability distributions, and then evaluate their performances experimentally. To configure the space of parameters of these approaches, we propose to use the framework of programming by optimisation (PbO). The results show that a CP-based pipeline obtains the best performance on well-known data mining and frequent itemset mining problems.

ABSTRACT. Answer set programming (ASP) is a popular declarative programming paradigm with a wide range of applications in artificial intelligence. Oftentimes, when modeling an AI problem with ASP, and in particular when we are interested beyond simple search for optimal solutions, an actual solution, differences between solutions, or number of solutions of the ASP program matter. For example, when a user aims to identify a specific answer set according to her needs, or requires the total number of diverging solutions to comprehend probabilistic applications such as reasoning in medical domains. Then, there are only certain problem specific and handcrafted encoding techniques available to navigate the solution space of ASP programs, which is oftentimes not enough. In this paper, we propose a formal and general framework for interactive navigation toward desired subsets of answer sets analogous to faceted browsing. Our approach enables the user to explore the solution space by consciously zooming in or out of sub-spaces of solutions at a certain configurable pace. We illustrate that weighted faceted navigation is computationally hard. Finally, we provide an implementation of our approach that demonstrates the feasibility of our framework for incomprehensible solution spaces.

ABSTRACT. In many synthesis problems, it can be essential to generate implementations which not only satisfy functional constraints but are also randomized to improve variety, robustness, or unpredictability. The recently-proposed framework of control improvisation (CI) provides techniques for the correct-by-construction synthesis of randomized systems subject to hard and soft constraints. However, prior work on CI has focused on qualitative specifications, whereas in robotic planning and other areas we often have quantitative quality metrics which can be traded against each other. For example, a designer of a patrolling security robot might want to know by how much the average patrol time needs to be increased in order to ensure that a particular aspect of the robot's route is sufficiently diverse and hence unpredictable. In this paper, we enable this type of application by generalizing the CI problem to support quantitative soft constraints which bound the expected value of a given cost function, and randomness constraints which enforce diversity of the generated traces with respect to a given label function. We establish the basic theory of labelled quantitative CI problems, and develop efficient algorithms for solving them when the specifications are encoded by finite automata. We also provide an approximate improvisation algorithm based on constraint solving for any specifications encodable as Boolean formulas. We demonstrate the utility of our problem formulation and algorithms with experiments applying them to generate diverse near-optimal plans for robotic planning problems.

ABSTRACT. Weighted model counting (WMC) is an extension of propositional model counting with applications to probabilistic inference and other areas of artificial intelligence. In recent experiments, WMC algorithms are shown to perform similarly overall but with significant differences on specific subsets of benchmarks. A good understanding of the differences in the performance of algorithms requires identifying key characteristics that favour some algorithms over others. In this paper, we introduce a random model for WMC instances with a parameter that influences primal treewidth—the parameter most commonly used to characterise the difficulty of an instance. We then use this model to experimentally compare the performance of WMC algorithms c2d, Cachet, d4, DPMC, and miniC2D on random instances. We show that the easy-hard-easy pattern is different for algorithms based on dynamic programming and algebraic decision diagrams (ADDs) than for all other solvers. We also show how all WMC algorithms scale exponentially with respect to primal treewidth and how this scalability varies across algorithms and densities. Finally, we demonstrate how the performance of ADD-based algorithms changes depending on how much determinism or redundancy there is in the numerical values of weights.

ABSTRACT. In this talk I will present an overview of recent advances on two fundamental problems in graphical causal analysis. In contrast to logical inference – where we reason about what is certainly true – we reason in statistical inference about what is likely to be true. Causal knowledge is usually represented in the form of directed acyclic graphs that allow an intuitive and mathematical-sound formalism. Since these graphs are a priory unknown, the first task is to learn them from data – in particular, one has to decide whether there is a causal explanation at all. The standard approach due to Verma and Pearl for this task works in two phases: First, a partially directed graph is learned using independent tests on the data; Second, the partially directed graph is extended (or oriented) to a Markov equivalent directed acyclic graph (DAG). While the first stage is well understood, the second part was open for a long time – it was believed that it may be possible to orient a graph in time O(n+m), but the best upper bound was just O(n⁴). In this talk I will sketch recent work with Wienöbst and Liśkiewicz, in which we settled the time complexity of the problem and proved that it is actually Θ(n³) under reasonable complexity-theoretic assumptions.

Since statistical properties of the data are maintained by a number of different DAGs, the sketched process does not unambiguously identify the underling DAG, but just a member of the class of Markov equivalent DAGs. It is therefore important to understand this equivalence class rather than a single DAG alone and, hence, the second fundamental problem is to determine the size of a Markov equivalence class. Since the size of the equivalence class can be exponential in the number of vertices, previous strategies based on exhaustive search, recursive partitioning, or dynamic programming on a tree decomposition all required exponential time. In the second part of the talk I present the high-level idea of a novel polynomial-time algorithm that solves the counting problem using the tree decomposition combined with various structural properties of chordal graphs – avoiding the traditional dynamic program on such decompositions.

ABSTRACT. This talk would be a follow-up to my paper at SEA 2022 with essentially the same title. I would report some developments on my part since the submission of the work to SEA. I would try to make the presentation as informative as possible for potential users of treewidth algorithms. I also hope to get feedbacks from the audience on what features of treewidth solvers are desirable from the uses' point of view.

ABSTRACT. In this talk, we consider counting and projected model counting of extensions in abstract argumentation for various semantics.

When asking for projected counts we are interested in counting the number of extensions of a given argumentation framework while multiple extensions that are identical when restricted to the projected arguments count as only one projected extension.

We establish classical complexity results and parameterized complexity results when the problems are parameterized by treewidth of the undirected argumentation graph. In particular, we show a complexity dichotomies for counting credulous extensions (#.coNP vs. #.P) as well as for the projected variant lifting the complexity by one level (#.NP vs. #.\Sigma^P_2).

To obtain upper bounds for counting projected extensions, we introduce novel algorithms that exploit small treewidth of the undirected argumentation graph of the input instance by dynamic programming (DP). Our algorithms run in time double or triple exponential in the treewidth depending on the considered semantics.

Finally, we take the exponential time hypothesis (ETH) into account and establish tight lower bounds of bounded treewidth algorithms for counting extensions and projected extension.

This talk present joint work with Johannes Fichte and Markus Hecher that was published at AAAI 2019 and presents also some recent advancements on preferred semantics.

ABSTRACT. The propositional model counting problem (#SAT) is known to be fixed-parameter-tractable (FPT) when parameterized by the width k of a given tree decomposition of the incidence graph. The running time of the fastest known FPT algorithm contains the exponential factor of 4^k . We improve this factor to 2^k by utilizing fast algorithms for computing the zeta transform and covering product of functions representing partial model counts, thereby achieving the same running time as FPT algorithms that are parameterized by the less general treewidth of the primal graph. Our new algorithm is asymptotically optimal unless the Strong Exponential Time Hypothesis (SETH) fails.

ABSTRACT. First-order model counting (FOMC) is a computational problem that asks to count the models of a sentence in first-order logic. Despite being around for more than a decade, practical FOMC algorithms are still unable to compute functions as simple as a factorial. We argue that the capabilities of FOMC algorithms are severely limited by their inability to express arbitrary recursive computations. To enable arbitrary recursion, we relax the restrictions that typically accompany domain recursion and generalise circuits used to express a solution to an FOMC problem to graphs that may contain cycles. To this end, we enhance the most well-established (weighted) FOMC algorithm ForcLift with new compilation rules and an algorithm to check whether a recursive call is feasible. These improvements allow us to find efficient solutions to counting fundamental structures such as injections and bijections.

ABSTRACT. Knowledge compilation concerns with the compilation of representation languages to target languages supporting a wide range of tractable operations arising from diverse areas of computer science. Tractable target compilation languages are usually achieved by restrictions on the internal nodes ($\land$ or $\lor$) of the NNF. Recently, a new representation language CCDD, which introduces new restrictions on conjunction nodes to capture equivalent literals, was proposed. We show that CCDDsupports uniform sampling in polytime. We present algorithms and a compiler to compile propositional formulas expressed in CNF into CCDD. Experiments over a large set of benchmarks show that our compilation times are better with smaller representations than state-of-art Decision-DNNF, SDD and OBDDC[AND] compilers. We apply our techniques to uniform sampling, and develop a uniform sampler on CNF. Our empirical evaluation demonstrates that our uniform sampler can solve 780 instances while the prior state of the art solved only 648 instances, representing a significant improvement of 132 instances.

ABSTRACT. Given a formula F, the problem of uniform sampling seeks to sample solutions of F uniformly at random. Uniform sampling is a fundamental problem with a wide variety of applications. The computational intractability of uniform sampling has led to the development of several samplers that are heuristics and are not accompanied by theoretical analysis of their distribution. Recently, Chakraborty and Meel (2019) designed the first scalable sampling tester, Barbarik, based on a grey-box sampling technique for testing if the distribution, according to which the given sampler is sampling, is close to the uniform or far from uniform. While the theoretical analysis of Barbarik provides only unconditional soundness guarantees, the empirical evaluation of Barbarik did show its success in determining that some of the off-the-shelf samplers were far from a uniform sampler.

The availability of Barbarik has the potential to spur the development of samplers and testing techniques such that developers can design sampling methods that can be accepted by Barbarik even though these samplers may not be amenable to a detailed mathematical analysis. In this paper, we present the realization of this aforementioned promise. Based on the flexibility offered by CryptoMiniSat, we design a sampler CMSGen that promises the achievement of the sweet spot of the quality of distributions and runtime performance. In particular, CMSGen achieves significant runtime performance improvement over the existing samplers. We conduct two case studies, and demonstrate that the usage of CMSGen leads to significant runtime improvements in the context of combinatorial testing and functional synthesis.