ABSTRACT. Access control is an important area of information security. The first paper in application of parameterized algorithmics in access control was published in 2010 by Qihua Wang and Ninghui Li. In the paper, the authors suggested a parameterization of the Workflow Satisfiability Problem (WSP). In its basic form, WSP is simply the Constraint Satisfaction Problem, which Wang and Li parameterized by the number of steps (= variables in CSP terms). Wang and Li proved that WSP is W[1]-hard and identified a practically important class of constraints for which WSP is FPT. They also conducted computational experiments using an off-the-shelf solver. Unfortunately, in their paper, the theoretical results and practical computation were not linked.

In the last decade, Jason Crampton (Information Security Group, RHUL), the speaker and their co-authors studied theoretical and practical computing aspects initially for WSP with user-independent (UI) non-unary constraints and its variations and then for other access control problems. Several FPT algorithms and lower bounds were obtained, FPT algorithms were implemented and off-the-shelf solvers were used in computational experiments. Among practical computing highlights are FPT algorithms for WSP with UI non-unary constraints performing in practice much better than off-the-shelf solvers, and  the possibility for off-the-shelf solvers to emulate FPT algorithms for WSP and other access control problems (approximately, the runtime exponential growth is wrt the parameter only).This theoretical and practical computing research was highly acknowledged by the access control community: most of the papers were published in top information security journals and some papers received the best paper awards in the annual symposium on access control (SACMAT).

ABSTRACT. In this talk I will discuss two promising applications of parameterized complexity for the natural generalization of Boolean satisfiability to optimization problems: MaxSAT, where the task is to find an assignment that maximizes the total weight of all satisfied clauses. As for most intractable optimization problems, it is rather hard to obtain parallel algorithms for MaxSAT with meaningful theoretical guarantees in the classical complexity theoretic sense. The situation is fundamentally different, however, if we study the \emph{parallel parameterized complexity} of the problem. In the first part of the talk I will give a gentle introduction to the underling framework of \emph{parallel parameterized algorithms} and \emph{parameterized circuit complexity.} Along the line we will motivate the definitions by pointing out on a high-level how to achieve various levels of parallelization for MaxSAT for different parameters within this model~--~in contrast, in a sequential world all these results would simply collapse into the observation that MaxSAT is fixed-parameter tractable parameterized by any of these parameters.

The second application is an observation about the target function that we wish to maximize. The literature almost solely considers the case of positive weights. While the general case of the problem is only restricted slightly by this constraint, many special cases become trivial in the absence of negative weights. I present various versions of the problem that are parameterized intractable if negative weights are present. We will observe that negative weights lead to a new interesting version: Instead of maximizing the sum of weights of satisfied clauses, we can maximize the absolute value of that sum. This turns out to be surprisingly expressive even restricted to monotone formulas in disjunctive normal form with at most two literals per clause. In contrast to the versions without the absolute value, however, we will discuss that these variants are parallel fixed-parameter tractable by providing an easy to compute kernel.

ABSTRACT. This talk will survey parameterized complexity results of the propositional satisfiability problem (SAT). We will cover parameters based on backdoors, decompositions, and hybrid parameters that combine both. After a general overview of results obtained over the last 20 years, we will discuss some recent results based on backdoor depth (ESA 2022) and twin-width (SAT 2022).

ABSTRACT. We discuss parameterized algorithms and an application to exact propositional model counting (MC). (W)MC asks for counting the (weighted) number of satisfying assignments of a propositional formula. The problem is known to be beyond NP and a prototypical representative of the class #P.

Various implementations that solve MC employ a SAT-based solving engine. However, we tackle the problem from a theoretical perspective exploiting bounded treewidth in input instances for which an algorithm that runs single exponential in the treewidth is known. The treewidth of an instance is at most the number of its variables, but often much smaller. While our approach suffers from the theoretical worst case bounds, we illustrate how it can still fruitfully be used in combination with modern hardware that takes advantage of parallelism. Our results are encouraging in the sense that complex reasoning problems can be tackled by parameterized algorithms executed on the GPU or within database systems if instances have small treewidth (<40).

ABSTRACT. The first-order model checking problem for finite graphs asks, given a graph G and a first-order sentence phi as input, to decide whether phi holds on G. While we do not expect that there is an efficient (fpt with respect to the formula size) algorithm which works on the class of all finite graphs, such algorithms have been proven to exist for various structurally well-behaved classes of graphs (graphs of bounded degree, planar graphs, unit interval graphs etc). Identifying graph classes for which an fpt model checking algorithm exists has been an active area of research for the past 25 years.

After the existence of an efficient model checking algorithm was shown for classes of sparse graphs in 2014 by Grohe, Kreutzer and Siebertz, the attention gradually turned to the more general setting of graph classes which can be obtained from sparse graphs via interpretations/transductions. This program has been initiated in 2016, when the existence of an fpt algorithm for the first-order model checking problem was shown for graph classes interpretable in graphs of bounded degree. After this, there followed several results about the structure of graphs interpretable in sparse graphs, but despite the efforts of several groups of researchers, no positive algorithmic result has been achieved until very recently. In the talk we will review the current status and recent developments regarding this problem, and in particular we will present a fixed-parameter tractable algorithm for the first-order model checking on interpretations of graph classes with bounded local treewidth (notably, this includes interpretations of planar graphs).

ABSTRACT. Argumentation frameworks (AFs) are a core formalism in the field of formal argumentation. As most standard computational tasks regarding AFs are hard for the first or second level of the Polynomial Hierarchy, a variety of algorithmic approaches to achieve manageable runtimes have been considered in the past. Among them, the backdoor-approach and the treewidth-approach turned out to yield fixed-parameter tractable fragments. However, many applications yield high parameter values for these methods, often rendering them infeasible in practice. We introduce the backdoor-treewidth approach for abstract argumentation, combining the best of both worlds with a guaranteed parameter value that does not exceed the minimum of the backdoor- and treewidth-parameter. In particular, we formally define backdoor-treewidth and establish fixed-parameter tractability for standard reasoning tasks of abstract argumentation. Moreover, we provide systems to find and exploit backdoors of small width, and conduct systematic experiments evaluating the new parameter.