Today's propositional satisfiability (SAT) solvers are extremely powerful and can be used as an efficient back-end for solving NP-complete problems. However, many fundamental problems in knowledge representation and reasoning are located at the second level of the Polynomial Hierarchy or even higher, and hence polynomial-time transformations to SAT are not possible, unless the hierarchy collapses. Recent research shows that in certain cases one can break through these complexity barriers by fixed-parameter tractable (fpt) reductions which exploit structural aspects of problem instances in terms of problem parameters. In this paper we develop a general theoretical framework that supports the classification of parameterized problems on whether they admit such an fpt-reduction to SAT or not.

Reasoning about temporal knowledge is a fundamental task in the area of artificial intelligence and knowledge representation. A key problem in this area is model checking, and indispensable for the state-of-the-art in solving this problem in large-scale settings is the technique of bounded model checking. We investigate the theoretical possibilities of this technique using parameterized complexity theory. In particular, we provide a complete parameterized complexity classification for the model checking problem for symbolically represented Kripke structures for various fragments of the temporal logics LTL, CTL and CTL*. We argue that a known result from the literature for a restricted fragment of LTL can be seen as an fpt-reduction to SAT, and show that such reductions are not possible for any of the other fragments of the temporal logics that we consider. As a by-product of our investigation, we develop a novel parameterized complexity class that can be seen as a parameterized variant of the Polynomial Hierarchy.

Planning is an important AI task that gives rise to many hard problems. In order to come up with efficient algorithms for this setting, it is important to understand the sources of complexity. For planning problems that are beyond NP, identifying fragments that allow an efficient reduction to SAT can be a feasible approach due to the great performance of modern SAT solvers. In this paper, we use the framework of parameterized complexity theory to obtain a more fine-grained complexity analysis of natural planning problems beyond NP. With this analysis we are able to point out several variants of planning where the structure in the input makes encodings into SAT feasible. We complement these positive results with some hardness results and a new machine characterization for the intractability class exists * for allk-W[P].

We provide a comprehensive analysis of the computational complexity of the outcome determination problem for the most important aggregation rules proposed in the literature on logic-based judgment aggregation. Judgment aggregation is a powerful and flexible framework for studying problems of collective decision making that has attracted interest in a range of disciplines, including Legal Theory, Philosophy, Economics, Political Science, and Artificial Intelligence. The problem of computing the outcome for a given list of individual judgments to be aggregated into a single collective judgment is the most fundamental algorithmic challenge arising in this context. Our analysis applies to several different variants of the basic framework of judgment aggregation that have been discussed in the literature, as well as to a new framework that encompasses all existing such frameworks in terms of expressive power and representational succinctness.

According to Gartner, "to keep pace with the demands of digital transformation initiatives, application development teams will augment their efforts with AI "co-developers" to streamline programming efforts". Gartner predicts that "by 2022, at least 40% of new application development projects will have virtual AI co-developers on their team." Mendix is a digital transformation enabler platform that helps businesses to build web and mobile applications without the need to code – what's called low-code development. The company has recently launched Mendix Assist, which uses machine learning and AI analysis of over 5 million application logic flows to deliver 90% accuracy on next-step suggestions and reduce the cost of development defects by 10x. The platform allows people from across the business with no coding skills to collaborate, build and continuously improve apps at speed and scale.