检索结果-内蒙古大学图书馆

Co-Certificate Learning with SAT Modulo Symmetries

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Kirchweger, Markus Peitl, Tomáš Szeider, Stefan Algorithms and Complexity Group TU Wien Vienna Austria

We present a new SAT-based method for generating all graphs up to isomorphism that satisfy a given co-NP property. Our method extends the SAT Modulo Symmetry (SMS) framework with a technique that we call co-certificate learning. If SMS generates a candidate graph that violates the given co-NP property, we obtain a certificate for this violation, i.e., ‘co-certificate’ for the co-NP property. The co-certificate gives rise to a clause that the SAT solver, serving as SMS’s backend, learns as part of its CDCL procedure. We demonstrate that SMS plus co-certificate learning is a powerful method that allows us to improve the best-known lower bound on the size of Kochen-Specker vector systems, a problem that is central to the foundations of quantum mechanics and has been studied for over half a century. Our approach is orders of magnitude faster and scales significantly better than a recently proposed SAT-based method. Copyright © 2023, The Authors. All rights reserved.

关键词： Quantum theory

Block Crossings in One-Sided Tanglegrams

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Dobler, Alexander Nöllenburg, Martin Algorithms and Complexity Group TU Wien Vienna Austria

Tanglegrams are drawings of two rooted binary phylogenetic trees and a matching between their leaf sets. The trees are drawn crossing-free on opposite sides with their leaf sets facing each other on two vertical lines. Instead of minimizing the number of pairwise edge crossings, we consider the problem of minimizing the number of block crossings, that is, two bundles of lines crossing each other locally. With one tree fixed, the leaves of the second tree can be permuted according to its tree structure. We give a complete picture of the algorithmic complexity of minimizing block crossings in one-sided tanglegrams by showing NP-completeness, constant-factor approximations, and a fixed-parameter algorithm. We also state first results for non-binary trees. © 2023, CC BY.

关键词： Binary trees

SAT modulo symmetries for graph generation 27

学校读者我要写书评

暂无评论

SAT modulo symmetries for graph generation

27th International Conference on Principles and Practice of Constraint Programming, CP 2021

作者： Kirchweger, Markus Szeider, Stefan Algorithms and Complexity Group TU Wien Austria

ISBN: (纸本)9783959772112

We propose a novel constraint-based approach to graph generation. Our approach utilizes the interaction between a CDCL SAT solver and a special symmetry propagator where the SAT solver runs on an encoding of the desired graph property. The symmetry propagator checks partially generated graphs for minimality w.r.t. a lexicographic ordering during the solving process. This approach has several advantages over a static symmetry breaking: (i) symmetries are detected early in the generation process, (ii) symmetry breaking is seamlessly integrated into the CDCL procedure, and (iii) the propagator can perform a complete symmetry breaking without causing a prohibitively large initial encoding. We instantiate our approach by generating extremal graphs with certain restrictions in terms of girth and diameter. With our approach, we could confirm the Simon-Murty Conjecture (1979) on diameter-2-critical graphs for graphs up to 18 vertices. © Markus Kirchweger and Stefan Szeider.

关键词： Encoding (symbols)

The k-Opt Algorithm for the Traveling Salesman Problem Has Exponential Running Time for k ≥ 5 51

学校读者我要写书评

暂无评论

The k-Opt Algorithm for the Traveling Salesman Problem Has E...

51st International Colloquium on Automata, Languages, and Programming, ICALP 2024

作者： Heimann, Sophia Hoang, Hung P. Hougardy, Stefan Research Institute for Discrete Mathematics University of Bonn Germany Algorithms and Complexity Group Faculty of Informatics TU Wien Austria Research Institute for Discrete Mathematics and Hausdorff Center for Mathematics University of Bonn Germany

ISBN: (纸本)9783959773225

The k-Opt algorithm is a local search algorithm for the Traveling Salesman Problem. Starting with an initial tour, it iteratively replaces at most k edges in the tour with the same number of edges to obtain a better tour. Krentel (FOCS 1989) showed that the Traveling Salesman Problem with the k-Opt neighborhood is complete for the class PLS (polynomial time local search) and that the k-Opt algorithm can have exponential running time for any pivot rule. However, his proof requires k 1000 and has a substantial gap. We show the two properties above for a much smaller value of k, addressing an open question by Monien, Dumrauf, and Tscheuschner (ICALP 2010). In particular, we prove the PLS-completeness for k ≥ 17 and the exponential running time for k ≥ 5. © Sophia Heimann, Hung P. Hoang, and Stefan Hougardy.

关键词： Traveling salesman problem

Splitting Plane Graphs to Outerplanarity

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Gronemann, Martin Nöllenburg, Martin Villedieu, Anaïs Algorithms and Complexity Group TU Wien Vienna Austria

Vertex splitting replaces a vertex by two copies and partitions its incident edges amongst the copies. This problem has been studied as a graph editing operation to achieve desired properties with as few splits as possible, most often planarity, for which the problem is NP-hard. Here we study how to minimize the number of splits to turn a plane graph into an outerplane one. We tackle this problem by establishing a direct connection between splitting a plane graph to outerplanarity, finding a connected face cover, and finding a feedback vertex set in its dual. We prove NP-completeness for plane biconnected graphs, while we show that a polynomial-time algorithm exists for maximal planar graphs. Finally, we provide upper and lower bounds for certain families of maximal planar graphs. © 2023, CC BY.

关键词： Polynomial approximation

***: Compressing Linear Set Diagrams

学校读者我要写书评

暂无评论

arXiv 2023年

作者： Wallinger, Markus Dobler, Alexander Nöllenburg, Martin Algorithms and Complexity Group TU Wien Vienna Austria

Linear diagrams are used to visualize set systems by depicting set memberships as horizontal line segments in a matrix, where each set is represented as a row and each element as a column. Each such line segment of a set is shown in a contiguous horizontal range of cells of the matrix indicating that the corresponding elements in the columns belong to the set. As each set occupies its own row in the matrix, the total height of the resulting visualization is as large as the number of sets in the instance. Such a linear diagram can be visually sparse and intersecting sets containing the same element might be represented by distant rows. To alleviate such undesirable effects, we present ***, a new approach that achieves a more space-efficient representation of linear diagrams. First, we minimize the total number of gaps in the horizontal segments by reordering columns, a criterion that has been shown to increase readability in linear diagrams. The main difference of *** to linear diagrams is that multiple non-intersecting sets can be positioned in the same row of the matrix. Furthermore, we present several different rendering variations for a matrix-based representation that utilize the proposed row compression. We implemented the different steps of our approach in a visualization pipeline using integer-linear programming, and suitable heuristics aiming at sufficiently fast computations in practice. We conducted both a quantitative evaluation and a small-scale user experiment to compare the effects of compressing linear diagrams. © 2023, CC BY.

关键词： Matrix algebra

Constrained Boundary Labeling

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Depian, Thomas Nöllenburg, Martin Terziadis, Soeren Wallinger, Markus Algorithms and Complexity Group TU Wien Austria Algorithms cluster TU Eindhoven Netherlands Technical University of Munich Germany

Boundary labeling is a technique in computational geometry used to label dense sets of feature points in an illustration. It involves placing labels along an axis-aligned bounding box and connecting each label with its corresponding feature point using non-crossing leader lines. Although boundary labeling is well-studied, semantic constraints on the labels have not been investigated thoroughly. In this paper, we introduce grouping and ordering constraints in boundary labeling: grouping constraints enforce that all labels in a group are placed consecutively on the boundary, and ordering constraints enforce a partial order over the labels. We show that it is NP-hard to find a labeling for arbitrarily sized labels with unrestricted positions along one side of the boundary. However, we obtain polynomial-time algorithms if we restrict this problem either to uniform-height labels or to a finite set of candidate positions. Finally, we show that finding a labeling on two opposite sides of the boundary is NP-complete, even for uniform-height labels and finite label positions. © 2024, CC BY.

关键词： Computational geometry

Breaking Symmetries in Quantified Graph Search: A Comparative Study

学校读者我要写书评

暂无评论

arXiv 2025年

作者： Janota, Mikoláš Kirchweger, Markus Peitl, Tomáš Szeider, Stefan Czech Technical University in Prague Czech Republic Algorithms and Complexity Group TU Wien Austria

Graph generation and enumeration problems often require handling equivalent graphs—those that differ only in vertex labeling. We study how to extend SAT Modulo Symmetries (SMS), a framework for eliminating such redundant graphs, to handle more complex constraints. While SMS was originally designed for constraints in propositional logic (in NP), we now extend it to handle quantified Boolean formulas (QBF), allowing for more expressive specifications like non-3-colorability (a coNP-complete property). We develop two approaches: a static QBF encoding and a dynamic method integrating SMS into QBF solvers. Our analysis reveals that while specialized approaches can be faster, QBF-based methods offer easier implementation and formal verification capabilities. © 2025, CC BY-NC-ND.

关键词： Formal verification

The Computational complexity of Positive Non-Clashing Teaching in Graphs

学校读者我要写书评

暂无评论

arXiv 2025年

作者： Ganian, Robert Khazaliya, Liana Inerney, Fionn Mc Rocton, Mathis Algorithms and Complexity Group TU Wien Austria Telefónica Scientific Research Barcelona Spain

We study the classical and parameterized complexity of computing the positive non-clashing teaching dimension of a set of concepts, that is, the smallest number of examples per concept required to successfully teach an intelligent learner under the considered, previously established model. For any class of concepts, it is known that this problem can be effortlessly transferred to the setting of balls in a graph G. We establish (1) the NP-hardness of the problem even when restricted to instances with positive non-clashing teaching dimension k = 2 and where all balls in the graph are present, (2) near-tight running time upper and lower bounds for the problem on general graphs, (3) fixed-parameter tractability when parameterized by the vertex integrity of G, and (4) a lower bound excluding fixed-parameter tractability when parameterized by the feedback vertex number and pathwidth of G, even when combined with k. Our results provide a nearly complete understanding of the complexity landscape of computing the positive non-clashing teaching dimension and answer open questions from the literature. Copyright © 2025, The Authors. All rights reserved.

关键词： Graph theory