-
Solving Quantified Boolean Formulas with Few Existential Variables
Authors:
Leif Eriksson,
Victor Lagerkvist,
George Osipov,
Sebastian Ordyniak,
Fahad Panolan,
Mateusz Rychlicki
Abstract:
The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness. Many problems of central interest in AI are in general not included in NP, e.g., planning, model checking, and non-monotonic reasoning, and for such problems QBF has successfully been used as a modelling tool. However, solvers for QBF are not as advanced as state…
▽ More
The quantified Boolean formula (QBF) problem is an important decision problem generally viewed as the archetype for PSPACE-completeness. Many problems of central interest in AI are in general not included in NP, e.g., planning, model checking, and non-monotonic reasoning, and for such problems QBF has successfully been used as a modelling tool. However, solvers for QBF are not as advanced as state of the art SAT solvers, which has prevented QBF from becoming a universal modelling language for PSPACE-complete problems. A theoretical explanation is that QBF (as well as many other PSPACE-complete problems) lacks natural parameters} guaranteeing fixed-parameter tractability (FPT).
In this paper we tackle this problem and consider a simple but overlooked parameter: the number of existentially quantified variables. This natural parameter is virtually unexplored in the literature which one might find surprising given the general scarcity of FPT algorithms for QBF. Via this parameterization we then develop a novel FPT algorithm applicable to QBF instances in conjunctive normal form (CNF) of bounded clause length. We complement this by a W[1]-hardness result for QBF in CNF of unbounded clause length as well as sharper lower bounds for the bounded arity case under the (strong) exponential-time hypothesis.
△ Less
Submitted 10 May, 2024;
originally announced May 2024.
-
The ACROBAT 2022 Challenge: Automatic Registration Of Breast Cancer Tissue
Authors:
Philippe Weitz,
Masi Valkonen,
Leslie Solorzano,
Circe Carr,
Kimmo Kartasalo,
Constance Boissin,
Sonja Koivukoski,
Aino Kuusela,
Dusan Rasic,
Yanbo Feng,
Sandra Sinius Pouplier,
Abhinav Sharma,
Kajsa Ledesma Eriksson,
Stephanie Robertson,
Christian Marzahl,
Chandler D. Gatenbee,
Alexander R. A. Anderson,
Marek Wodzinski,
Artur Jurgas,
Niccolò Marini,
Manfredo Atzori,
Henning Müller,
Daniel Budelmann,
Nick Weiss,
Stefan Heldmann
, et al. (16 additional authors not shown)
Abstract:
The alignment of tissue between histopathological whole-slide-images (WSI) is crucial for research and clinical applications. Advances in computing, deep learning, and availability of large WSI datasets have revolutionised WSI analysis. Therefore, the current state-of-the-art in WSI registration is unclear. To address this, we conducted the ACROBAT challenge, based on the largest WSI registration…
▽ More
The alignment of tissue between histopathological whole-slide-images (WSI) is crucial for research and clinical applications. Advances in computing, deep learning, and availability of large WSI datasets have revolutionised WSI analysis. Therefore, the current state-of-the-art in WSI registration is unclear. To address this, we conducted the ACROBAT challenge, based on the largest WSI registration dataset to date, including 4,212 WSIs from 1,152 breast cancer patients. The challenge objective was to align WSIs of tissue that was stained with routine diagnostic immunohistochemistry to its H&E-stained counterpart. We compare the performance of eight WSI registration algorithms, including an investigation of the impact of different WSI properties and clinical covariates. We find that conceptually distinct WSI registration methods can lead to highly accurate registration performances and identify covariates that impact performances across methods. These results establish the current state-of-the-art in WSI registration and guide researchers in selecting and develo** methods.
△ Less
Submitted 29 May, 2023;
originally announced May 2023.
-
Improved Algorithms for Allen's Interval Algebra by Dynamic Programming with Sublinear Partitioning
Authors:
Leif Eriksson,
Victor Lagerkvist
Abstract:
Allen's interval algebra is one of the most well-known calculi in qualitative temporal reasoning with numerous applications in artificial intelligence. Recently, there has been a surge of improvements in the fine-grained complexity of NP-hard reasoning tasks, improving the running time from the naive $2^{O(n^2)}$ to $O^*((1.0615n)^{n})$, with even faster algorithms for unit intervals a bounded num…
▽ More
Allen's interval algebra is one of the most well-known calculi in qualitative temporal reasoning with numerous applications in artificial intelligence. Recently, there has been a surge of improvements in the fine-grained complexity of NP-hard reasoning tasks, improving the running time from the naive $2^{O(n^2)}$ to $O^*((1.0615n)^{n})$, with even faster algorithms for unit intervals a bounded number of overlap** intervals (the $O^*(\cdot)$ notation suppresses polynomial factors). Despite these improvements the best known lower bound is still only $2^{o(n)}$ (under the exponential-time hypothesis) and major improvements in either direction seemingly require fundamental advances in computational complexity. In this paper we propose a novel framework for solving NP-hard qualitative reasoning problems which we refer to as dynamic programming with sublinear partitioning. Using this technique we obtain a major improvement of $O^*((\frac{cn}{\log{n}})^{n})$ for Allen's interval algebra. To demonstrate that the technique is applicable to more domains we apply it to a problem in qualitative spatial reasoning, the cardinal direction point algebra, and solve it in $O^*((\frac{cn}{\log{n}})^{2n/3})$ time. Hence, not only do we significantly advance the state-of-the-art for NP-hard qualitative reasoning problems, but obtain a novel algorithmic technique that is likely applicable to many problems where $2^{O(n)}$ time algorithms are unlikely.
△ Less
Submitted 25 May, 2023;
originally announced May 2023.
-
A Fast Algorithm for Consistency Checking Partially Ordered Time
Authors:
Leif Eriksson,
Victor Lagerkvist
Abstract:
Partially ordered models of time occur naturally in applications where agents or processes cannot perfectly communicate with each other, and can be traced back to the seminal work of Lamport. In this paper we consider the problem of deciding if a (likely incomplete) description of a system of events is consistent, the network consistency problem for the point algebra of partially ordered time (POT…
▽ More
Partially ordered models of time occur naturally in applications where agents or processes cannot perfectly communicate with each other, and can be traced back to the seminal work of Lamport. In this paper we consider the problem of deciding if a (likely incomplete) description of a system of events is consistent, the network consistency problem for the point algebra of partially ordered time (POT). While the classical complexity of this problem has been fully settled, comparably little is known of the fine-grained complexity of POT except that it can be solved in $O^*((0.368n)^n)$ time by enumerating ordered partitions. We construct a much faster algorithm with a run-time bounded by $O^*((0.26n)^n)$. This is achieved by a sophisticated enumeration of structures similar to total orders, which are then greedily expanded toward a solution. While similar ideas have been explored earlier for related problems it turns out that the analysis for POT is non-trivial and requires significant new ideas.
△ Less
Submitted 25 May, 2023;
originally announced May 2023.
-
ACROBAT -- a multi-stain breast cancer histological whole-slide-image data set from routine diagnostics for computational pathology
Authors:
Philippe Weitz,
Masi Valkonen,
Leslie Solorzano,
Circe Carr,
Kimmo Kartasalo,
Constance Boissin,
Sonja Koivukoski,
Aino Kuusela,
Dusan Rasic,
Yanbo Feng,
Sandra Kristiane Sinius Pouplier,
Abhinav Sharma,
Kajsa Ledesma Eriksson,
Leena Latonen,
Anne-Vibeke Laenkholm,
Johan Hartman,
Pekka Ruusuvuori,
Mattias Rantalainen
Abstract:
The analysis of FFPE tissue sections stained with haematoxylin and eosin (H&E) or immunohistochemistry (IHC) is an essential part of the pathologic assessment of surgically resected breast cancer specimens. IHC staining has been broadly adopted into diagnostic guidelines and routine workflows to manually assess status and scoring of several established biomarkers, including ER, PGR, HER2 and KI67.…
▽ More
The analysis of FFPE tissue sections stained with haematoxylin and eosin (H&E) or immunohistochemistry (IHC) is an essential part of the pathologic assessment of surgically resected breast cancer specimens. IHC staining has been broadly adopted into diagnostic guidelines and routine workflows to manually assess status and scoring of several established biomarkers, including ER, PGR, HER2 and KI67. However, this is a task that can also be facilitated by computational pathology image analysis methods. The research in computational pathology has recently made numerous substantial advances, often based on publicly available whole slide image (WSI) data sets. However, the field is still considerably limited by the sparsity of public data sets. In particular, there are no large, high quality publicly available data sets with WSIs of matching IHC and H&E-stained tissue sections. Here, we publish the currently largest publicly available data set of WSIs of tissue sections from surgical resection specimens from female primary breast cancer patients with matched WSIs of corresponding H&E and IHC-stained tissue, consisting of 4,212 WSIs from 1,153 patients. The primary purpose of the data set was to facilitate the ACROBAT WSI registration challenge, aiming at accurately aligning H&E and IHC images. For research in the area of image registration, automatic quantitative feedback on registration algorithm performance remains available through the ACROBAT challenge website, based on more than 37,000 manually annotated landmark pairs from 13 annotators. Beyond registration, this data set has the potential to enable many different avenues of computational pathology research, including stain-guided learning, virtual staining, unsupervised pre-training, artefact detection and stain-independent models.
△ Less
Submitted 24 November, 2022;
originally announced November 2022.
-
A Multivariate Complexity Analysis of Qualitative Reasoning Problems
Authors:
Leif Eriksson,
Victor Lagerkvist
Abstract:
Qualitative reasoning is an important subfield of artificial intelligence where one describes relationships with qualitative, rather than numerical, relations. Many such reasoning tasks, e.g., Allen's interval algebra, can be solved in $2^{O(n \cdot \log n)}$ time, but single-exponential running times $2^{O(n)}$ are currently far out of reach. In this paper we consider single-exponential algorithm…
▽ More
Qualitative reasoning is an important subfield of artificial intelligence where one describes relationships with qualitative, rather than numerical, relations. Many such reasoning tasks, e.g., Allen's interval algebra, can be solved in $2^{O(n \cdot \log n)}$ time, but single-exponential running times $2^{O(n)}$ are currently far out of reach. In this paper we consider single-exponential algorithms via a multivariate analysis consisting of a fine-grained parameter $n$ (e.g., the number of variables) and a coarse-grained parameter $k$ expected to be relatively small. We introduce the classes FPE and XE of problems solvable in $f(k) \cdot 2^{O(n)}$, respectively $f(k)^n$, time, and prove several fundamental properties of these classes. We proceed by studying temporal reasoning problems and (1) show that the Partially Ordered Time problem of effective width $k$ is solvable in $16^{kn}$ time and is thus included in XE, and (2) that the network consistency problem for Allen's interval algebra with no interval overlap** with more than $k$ others is solvable in $(2nk)^{2k} \cdot 2^{n}$ time and is included in FPE. Our multivariate approach is in no way limited to these to specific problems and may be a generally useful approach for obtaining single-exponential algorithms.
△ Less
Submitted 30 September, 2022;
originally announced September 2022.
-
Modal Logics for Nominal Transition Systems
Authors:
Joachim Parrow,
Johannes Borgström,
Lars-Henrik Eriksson,
Ramūnas Forsberg Gutkovas,
Tjark Weber
Abstract:
We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely suppor…
▽ More
We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle.
△ Less
Submitted 27 January, 2021; v1 submitted 4 April, 2019;
originally announced April 2019.
