ABSTRACT. Similar to the satisfiability (SAT) problem, which can be seen to be the archetypical problem for NP, the quantified Boolean formula problem (QBF) is the archetypical problem for PSPACE. Recently, Atserias and Oliva (2014) showed that, unlike for SAT, many of the well-known decompositional parameters (such as treewidth and pathwidth) do not allow efficient algorithms for QBF. The main reason for this seems to be the lack of awareness of these parameters towards the dependencies between variables of a QBF formula. In this paper we extend the ordinary pathwidth to the QBF-setting by introducing prefix pathwidth, which takes into account the dependencies between variables in a QBF, and show that it leads to an efficient algorithm for QBF. We hope that our approach will help to initiate the study of novel tailor-made decompositional parameters for QBF and thereby help to lift the success of these decompositional parameters from SAT to QBF.

ABSTRACT. In this paper, we address the problem of random generation of realistic pseudo-industrial SAT instances. First, we review some existing generators which are based on the notions of scale-free structure and community structure. Then, we propose a new generator based on the notion of \emph{popularity} and \emph{similarity}. This new model generates instances with both scale-free and community structure, solving the drawbacks of the previous generators.

ABSTRACT. Structural properties of CNF formulas are often suggested as a basis for explaining the large variation in solving hardness or as instance features that could be exploited by solvers. Examples include community structure and tree-width of graphs associated with the formulas. We will describe some findings from an experimental exploration of the relevance of these properties to actual performance of CDCL SAT solvers.

ABSTRACT. We present a compilation algorithm for beta-acyclic formulas into polynomial size decision DNNF. The DNNF constructed by this algorithm are not structured and we present a proof that this cannot be improved by showing that beta-acyclic formulas may have exponential size structured DNNF.

ABSTRACT. In my talk I would like to give some insights about recent investigations into the structure of MU, minimally unsatisfiable clause-sets, organised in layers by the deficiency.

ABSTRACT. This is an extended abstract of our ongoing research. We report that the ordering of additions strongly affects the performance of a CNF encoding of cardinality constraints. Then we propose a new encoding that automatically decides a nice ordering by exploiting the underlying graph structure.

ABSTRACT. The complexity of various Constraint Satisfaction Problems (CSP) when parameterized by structural measures (such as treewidth or clique-width) is a very well-investigated area. In this paper, we take a fresh look at such questions from the point of view of approximation, considering four standard CSP predicates: AND, OR, PARITY, and MAJORITY. By providing new or tighter hardness results for the satisfiability versions, as well as approximation algorithms for the corresponding maximization problems, we show that already these basic predicates display a diverse set of behaviors, ranging from being FPT to optimize exactly for quite general parameters (PARITY), to being W-hard but well-approximable (OR, MAJORITY) to being W-hard and inapproximable (AND). Our results indicate the interest in posing the question of approximability during the usual investigation of CSP complexity with regards to the landscape of structural parameters.

ABSTRACT. Propositional satisfiability (SAT) and related problems (like Model Counting, QBF-SAT, and CSP) are in practise often much easier to solve than suggested by their respective theoretical worst-case complexities. This "friendliness" of the real world is often explained by the presence of some kind of "hidden structure" in practical problem instances. In this talk we will review some mathematical concepts that attempt to capture the structure in problem instances and discuss their virtues and limits. We will focus rather on general questions than on  technical details.