View: session overviewtalk overview

14:00 | Cohomology in Constraint Satisfaction and Structure Isomorphism ABSTRACT. CSP and SI are among the most well-studied computational problems in Computer Science. While neither problem is thought to be in PTIME, much work is done on PTIME approximations to both problems. Two such historically important approximations are the k-consistency algorithm for CSP and the k-Weisfeiler-Leman algorithm for SI, both of which are based on propagating local partial solutions. The limitations of these algorithms are well-known – k-consistency can solve precisely those CSPs of bounded width and k-Weisfeiler-Leman can only distinguish structures which differ on properties definable in C^k. In this paper, we introduce a novel sheaf-theoretic approach to CSP and SI and their approximations. We show that both problems can be viewed as deciding the existence of global sections of presheaves, H_k(A,B) and I_k(A,B) and that the success of the k-consistency and k-Weisfeiler-Leman algorithms correspond to the existence of certain efficiently computable subpresheaves of these. Furthermore, building on work of Abramsky and others in quantum foundations, we show how to use Čech cohomology in H_k(A,B) and I_k(A,B) to detect obstructions to the existence of the desired global sections and derive new efficient cohomological algorithms extending k consistency and k-Weisfeiler-Leman. We show that cohomological k-consistency can solve systems of equations over all finite rings and that cohomological Weisfeiler-Leman can distinguish positive and negative instances of the Cai-Fürer-Immerman property over several important classes of structures. |

14:25 | Bounded Degree Nonnegative Counting CSP ABSTRACT. Constraint satisfaction problems (CSP) encompass an enormous variety of computational problems. In particular, all partition functions from statistical physics, such as spin systems, are special cases of counting CSP (#CSP). We prove a complete complexity classification for every counting problem in #CSP with nonnegative valued constraint functions that is valid when every variable occurs a bounded number of times in all constraints. We show that, depending on the set of constraint functions F, every problem in the complexity class #CSP(F) defined by F is either polynomial time computable for all instances without the bounded occurrence restriction, or is #P-hard even when restricted to bounded degree input instances. The constant bound in the degree depends on F. The dichotomy criterion on F is decidable. As a second contribution, we prove a slightly modified but more streamlined decision procedure for tractability. This enables us to fully classify a family of directed weighted graph homomorphism problems. This family contains both P-time tractable problems and #P-hard problems. To our best knowledge, this is the first family of such problems explicitly classified that are not acyclic, thereby the Lov\'asz-goodness criterion of Dyer-Goldberg-Paterson cannot be applied. |

14:50 | Higher-Order Quantified Boolean Satisfiability PRESENTER: Alessio Mansutti ABSTRACT. The Boolean satisfiability problem plays a central role in computational complexity and is often used as a starting point for showing NP lower bounds. Generalisations such as Succinct SAT, where a Boolean formula is succinctly represented as a Boolean circuit, have been studied in the literature in order to lift the Boolean satisfiability problem to higher complexity classes such as NEXPTIME. While in theory iterating this approach yields complete problems for k-NEXPTIME for all $k>0$, using such iterations of Succinct SAT is at best tedious when it comes to proving lower bounds. The main contribution of this paper is to show that the Boolean satisfiability problem has another canonical generalisation in terms of higher-order Boolean functions that is arguably more suitable for showing lower bounds beyond NP. We introduce a family of problems HOSAT(k,d), $k\ge 0$, $d\ge 1$ in which variables are interpreted as Boolean functions of order at most $k$ and there are $d$ alternations between functions of order exactly $k$. We show that the unbounded HOSAT problem is $\tower$-complete, and that HOSAT(k,d) is complete for the weak k-EXPTIME hierarchy with $d$ alternations for fixed $k,d \geq 1$. We illustrate the usefulness of HOSAT by characterising the complexity of weak Presburger arithmetic, the first-order theory of the integers with addition and equality but without order. It has been a long-standing open problem whether weak Presburger arithmetic has the same complexity as standard Presburger arithmetic. We answer this question affirmatively, even for the negation-free fragment and the Horn fragment of weak Presburger arithmetic. |

15:15 | CNF Encodings of Parity ABSTRACT. The minimum number of clauses in a~CNF representation of the parity function $x_1 \oplus x_2 \oplus \dotsb \oplus x_n$ is $2^{n-1}$. One can obtain a~more compact CNF encoding by~using non-deterministic variables (also known as~guess or~auxiliary variables). In~this paper, we prove the following lower bounds, that almost match known upper bounds, on~the number~$m$ of~clauses and the maximum width~$k$ of clauses: 1)~if there are at~most $s$~auxiliary variables, then $m \ge \Omega\left(2^{n/(s+1)}/n\right)$ and $k \ge n/(s+1)$; 2)~the minimum number of clauses is at~least~$3n$. We~derive the first two bounds from the Satisfiability Coding Lemma due to~Paturi, Pudl{\'{a}}k, and Zane. |

14:00 | Comonadic semantics for hybrid logic ABSTRACT. Hybrid logic is a widely-studied extension of basic modal logic, which corresponds to the bounded fragment of first-order logic. We study it from two novel perspectives: (1) We apply the recently introduced paradigm of comonadic semantics, which provides a new set of tools drawing on ideas from categorical semantics which can be applied to finite model theory, descriptive complexity and combinatorics. (2) We give a novel semantic characterization of hybrid logic in terms of invariance under disjoint extensions, a minimal form of locality. A notable feature of this result is that we give a uniform proof, valid for both the finite and infinite cases. |

14:25 | Higher-order causal theories are models of BV-logic ABSTRACT. The Caus[-] construction takes a compact closed category of basic processes and yields a *-autonomous category of higher-order processes obeying certain signalling/causality constraints, as dictated by the type system in the resulting category. This paper looks at instances where the base category C satisfies additional properties yielding an affine-linear structure on Caus[C] and a substantially richer internal logic. While the original construction only gave multiplicative linear logic, here we additionally obtain additives and a non-commutative, self-dual sequential product yielding a model of Guglielmi's BV logic. Furthermore, we obtain a natural interpretation for the sequential product as "A can signal to B, but not vice-versa", which sits as expected between the non-signalling tensor and the fully-signalling (i.e. unconstrained) par. Fixing matrices of positive numbers for C recovers the BV category structure of probabilistic coherence spaces identified by Blute, Panangaden, and Slavnov, restricted to normalised maps. On the other hand, fixing the category of completely positive maps gives an entirely new model of BV consisting of higher order quantum channels, encompassing recent work in the study of quantum and indefinite causal structures. |

14:50 | Towards a Model Theory of Ordered Logics: Expressivity and Interpolation PRESENTER: Bartosz Bednarczyk ABSTRACT. We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory, however, is poorly understood. Our paper aims to provide some insight into it. We start by providing suitable notions of bisimulation for ordered logics. We next employ bisimulations to compare the relative expressive power of ordered logics, and to characterise our logics as bisimulation-invariant fragments of FO à la van Benthem. Afterwards, we study the Craig Interpolation Property (CIP). We refute yet another claim from the infamous work by Purdy, by showing that the fluted and forward fragments do not enjoy CIP. We complement this result by showing that the ordered fragment and the guarded ordered logics enjoy CIP. These positive results rely on novel and quite intricate model constructions, which take full advantage of the ``forwardness'' of our logics. |

15:15 | Generalized Bundled Fragments of First-order Modal Logic ABSTRACT. When we bundle quantifiers and modalities together (as in $\exists x \Box$, $\Diamond \forall x$ etc.) in first-order modal logic (FOML), we get new logical operators whose combinations produce interesting \textit{bundled} fragments of FOML. It is well-known that finding decidable fragments of \FOML is hard, but existing work shows that certain bundled fragments are decidable [Padmanabha et al 2018], without any restriction on the arity of predicates, the number of variables, or the modal scope. In this paper, we explore generalized bundles such as $\forall x\forall y \Box, \forall x\exists y \Diamond$ etc., and map the terrain with regard to decidability, presenting both decidability and undecidability results. In particular, we propose the loosely bundled fragment which is decidable over increasing domains and encompasses all known decidable bundled fragments. |

Consists of a general introduction, a talk by Tuukka Korhonen on "Finding Optimal Tree Decompositions", and a talk by Jasper Slusallek on “Algorithms and Lower Bounds for Finding (Exact-Weight) Subgraphs of Bounded Treewidth”.