Abstract:
The workflow satisfiability problem is concerned with determining whether it is possible to find an allocation of authorized users to the steps in a workflow in such a way that all constraints are satisfied. The problem is NP-hard in general, but is known to be fixed-parameter tractable for certain classes of constraints. The known results on fixed-parameter tractability rely on the symmetry (in some sense) of the constraints. In this paper, we provide the first results that establish fixed-parameter tractability of the satisfiability problem when the constraints are asymmetric. In particular, we introduce the notion of seniority constraints, in which the execution of steps is determined, in part, by the relative seniority of the users that perform them. Our results require new techniques, which make use of tree decompositions of the graph of the binary relation defining the constraint. Finally, we establish a lower bound for the hardness of the workflow satisfiability problem.

Abstract:
We investigate the parameterized computational complexity of the satisfiability problem for modal logic and attempt to pinpoint relevant structural parameters which cause the problem's combinatorial explosion, beyond the number of propositional variables v. To this end we study the modality depth, a natural measure which has appeared in the literature, and show that, even though modal satisfiability parameterized by v and the modality depth is FPT, the running time's dependence on the parameters is a tower of exponentials (unless P=NP). To overcome this limitation we propose several possible alternative parameters, namely diamond dimension, box dimension and modal width. We show fixed-parameter tractability results using these measures where the exponential dependence on the parameters is much milder than in the case of modality depth thus leading to FPT algorithms for modal satisfiability with much more reasonable running times.

Abstract:
We study the data complexity of model-checking for logics with team semantics. For dependence and independence logic, we completely characterize the tractability/intractability frontier of data complexity of both quantifier-free and quantified formulas. For inclusion logic formulas, we reduce the model-checking problem to the satisfiability problem of so-called Dual-Horn propositional formulas. Via this reduction, we give an alternative proof for the recent result showing that the data complexity of inclusion logic is in PTIME.

Abstract:
These notes contain, among others, a proof that the average running time of an easy solution to the satisfiability problem for propositional calculus is, under some reasonable assumptions, linear (with constant 2) in the size of the input. Moreover, some suggestions are made about criteria for tractability of complex algorithms. In particular, it is argued that the distribution of probability on the whole input space of an algorithm constitutes an non-negligible factor in estimating whether the algorithm is tractable or not.

Abstract:
A special case of the satisfiability problem, in which the clauses have a hierarchical structure, is shown to be solvable in linear time, assuming that the clauses have been represented in a convenient way.

Abstract:
Boolean satisfiability problems are an important benchmark for questions about complexity, algorithms, heuristics and threshold phenomena. Recent work on heuristics, and the satisfiability threshold has centered around the structure and connectivity of the solution space. Motivated by this work, we study structural and connectivity-related properties of the space of solutions of Boolean satisfiability problems and establish various dichotomies in Schaefer's framework. On the structural side, we obtain dichotomies for the kinds of subgraphs of the hypercube that can be induced by the solutions of Boolean formulas, as well as for the diameter of the connected components of the solution space. On the computational side, we establish dichotomy theorems for the complexity of the connectivity and st-connectivity questions for the graph of solutions of Boolean formulas. Our results assert that the intractable side of the computational dichotomies is PSPACE-complete, while the tractable side - which includes but is not limited to all problems with polynomial time algorithms for satisfiability - is in P for the st-connectivity question, and in coNP for the connectivity question. The diameter of components can be exponential for the PSPACE-complete cases, whereas in all other cases it is linear; thus, small diameter and tractability of the connectivity problems are remarkably aligned. The crux of our results is an expressibility theorem showing that in the tractable cases, the subgraphs induced by the solution space possess certain good structural properties, whereas in the intractable cases, the subgraphs can be arbitrary.

Abstract:
In the theory of tractability of multivariate problems one usually studies problems with finite smoothness. Then we want to know which $s$-variate problems can be approximated to within $\varepsilon$ by using, say, polynomially many in $s$ and $\varepsilon^{-1}$ function values or arbitrary linear functionals. There is a recent stream of work for multivariate analytic problems for which we want to answer the usual tractability questions with $\varepsilon^{-1}$ replaced by $1+\log \varepsilon^{-1}$. In this vein of research, multivariate integration and approximation have been studied over Korobov spaces with exponentially fast decaying Fourier coefficients. This is work of J. Dick, G. Larcher, and the authors. There is a natural need to analyze more general analytic problems defined over more general spaces and obtain tractability results in terms of $s$ and $1+\log \varepsilon^{-1}$. The goal of this paper is to survey the existing results, present some new results, and propose further questions for the study of tractability of multivariate analytic questions.

Abstract:
We study elementary modal logics, i.e. modal logic considered over first-order definable classes of frames. The classical semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. Many decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and for finite satisfiability [11, 12, 16, 17]. In this paper, we show that there is a reason why we must deal with both kinds of satisfiability separately – we prove that there is a universal first-order formula that defines an elementary modal logic with decidable (global) satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.

Abstract:
The problem of estimating the proportion of satisfiable instances of a given CSP (constraint satisfaction problem) can be tackled through weighting. It consists in putting onto each solution a non-negative real value based on its neighborhood in a way that the total weight is at least 1 for each satisfiable instance. We define in this paper a general weighting scheme for the estimation of satisfiability of general CSPs. First we give some sufficient conditions for a weighting system to be correct. Then we show that this scheme allows for an improvement on the upper bound on the existence of non-trivial cores in 3-SAT obtained by Maneva and Sinclair (2008) to 4.419. Another more common way of estimating satisfiability is ordering. This consists in putting a total order on the domain, which induces an orientation between neighboring solutions in a way that prevents circuits from appearing, and then counting only minimal elements. We compare ordering and weighting under various conditions.