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

A Simple Partially Embedded Planarity Test Based on Vertex-Addition 8

学校读者我要写书评

暂无评论

A Simple Partially Embedded Planarity Test Based on Vertex-A...

8th SIAM Symposium on Simplicity of algorithms, SOSA 2025

作者： Fink, Simon D. Rutter, Ignaz Sandhya, T.P. Algorithms and Complexity Group Technische Universität Wien Austria Faculty of Informatics and Mathematics University of Passau Germany Stockholm University Department of Mathematics Sweden

ISBN: (纸本)9781611978315

In the Partially Embedded Planarity problem, we are given a graph G together with a topological drawing of a subgraph H of G. The task is to decide whether the drawing can be extended to a drawing of the whole graph such that no two edges cross. Angelini et al. gave a linear-time algorithm for solving this problem in 2010 [1, 2]. While their paper constitutes a significant result, the algorithm described therein is highly complex: it uses several layers of decompositions according to connectivity of both G and H, its description spans more than 30 pages, and can hardly be considered implementable. We give an independent linear-time algorithm that works along the well-known vertex-addition planarity test by Booth and Lueker [5, 6]. We modify the PC-tree as underlying data structure used for representing all planar drawing possibilities in a natural way to also respect the restrictions given by the prescribed drawing of the subgraph H. The testing algorithm and its proof of correctness only require small adaptations from the comparatively much simpler generic planarity test, of which several implementations exist. If the test succeeds, an embedding can be constructed using the same approaches that are used for the generic planarity test. Copyright © 2025 by SIAM.

关键词： Trees (mathematics)

Extracting Problem Structure with LLMs for Optimized SAT Local Search

学校读者我要写书评

暂无评论

arXiv 2025年

作者： Schidler, André Szeider, Stefan Algorithms and Complexity Group TU Wien Vienna Austria

Local search preprocessing makes Conflict-Driven Clause Learning (CDCL) solvers faster by providing high-quality starting points and modern SAT solvers have incorporated this technique into their preprocessing steps. However, these tools rely on basic strategies that miss the structural patterns in problems. We present a method that applies Large Language Models (LLMs) to analyze Python-based encoding code. This reveals hidden structural patterns in how problems convert into SAT. Our method automatically generates specialized local search algorithms that find these patterns and use them to create strong initial assignments. This works for any problem instance from the same encoding type. Our tests show encouraging results, achieving faster solving times compared to baseline preprocessing systems. Copyright © 2025, The Authors. All rights reserved.

关键词： Encoding (symbols)

Smart Cubing for Graph Search: A Comparative Study

学校读者我要写书评

暂无评论

arXiv 2025年

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

Parallel solving via cube-and-conquer is a key method for scaling SAT solvers to hard instances. While cube-and-conquer has proven successful for pure SAT problems, notably the Pythagorean triples conjecture, its application to SAT solvers extended with propagators presents unique challenges, as these propagators learn constraints dynamically during the search. We study this problem using SAT Modulo Symmetries (SMS) as our primary test case, where a symmetry-breaking propagator reduces the search space by learning constraints that eliminate isomorphic graphs. Through extensive experimentation comprising over 10,000 CPU hours, we systematically evaluate different cube-and-conquer variants on three well-studied combinatorial problems. Our methodology combines prerun phases to collect learned constraints, various cubing strategies, and parameter tuning via algorithm configuration and LLM-generated design suggestions. The comprehensive empirical evaluation provides new insights into effective cubing strategies for propagator-based SAT solving, with our best method achieving speedups of 2-3x from improved cubing and parameter tuning, providing an additional 1.5-2x improvement on harder instances. Copyright © 2025, The Authors. All rights reserved.

关键词： Geometry

Compilation and Fast Model Counting beyond CNF

学校读者我要写书评

暂无评论

arXiv 2025年

作者： de Colnet, Alexis Szeider, Stefan Zhang, Tianwei Algorithms and Complexity Group TU Wien Vienna Austria

Circuits in deterministic decomposable negation normal form (d-DNNF) are representations of Boolean functions that enable linear-time model counting. This paper strengthens our theoretical knowledge of what classes of functions can be efficiently transformed, or compiled, into d-DNNF. Our main contribution is the fixed-parameter tractable (FPT) compilation of conjunctions of specific constraints parameterized by incidence treewidth. This subsumes the known result for CNF. The constraints in question are all functions representable by constant-width ordered binary decision diagrams (OBDDs) for all variable orderings. For instance, this includes parity constraints and cardinality constraints with constant threshold. The running time of the FPT compilation is singly exponential in the incidence treewidth but hides large constants in the exponent. To balance that, we give a more efficient FPT algorithm for model counting that applies to a sub-family of the constraints and does not require compilation. © 2025, CC BY.

关键词： Boolean functions

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

The complexity of Extending Fair Allocations of Indivisible Goods

学校读者我要写书评

暂无评论

arXiv 2025年

作者： Deligkas, Argyrios Eiben, Eduard Ganian, Robert Goldsmith, Tiger-Lily Ioannidis, Stavros D. Department of Computer Science Royal Holloway University of London United Kingdom Algorithms and Complexity group TU Wien Austria

We initiate the study of computing envy-free allocations of indivisible items in the extension setting, i.e., when some part of the allocation is fixed and the task is to allocate the remaining items. Given the known NP-hardness of the problem, we investigate whether—and under which conditions—one can obtain fixed-parameter algorithms for computing a solution in settings where most of the allocation is already fixed. Our results provide a broad complexity-theoretic classification of the problem which includes: (a) fixed-parameter algorithms tailored to settings with few distinct types of agents or items;(b) lower bounds which exclude the generalization of these positive results to more general settings. We conclude by showing that—unlike when computing allocations from scratch—the non-algorithmic question of whether more relaxed EFX allocations exist can be completely resolved in the extension *** Codes 91B32 Copyright © 2025, The Authors. All rights reserved.

关键词：

A Minor-Testing Approach for Coordinated Motion Planning with Sliding Robots

学校读者我要写书评

暂无评论

arXiv 2025年

作者： Eiben, Eduard Ganian, Robert Kanj, Iyad Sridharan, Ramanujan M. Department of Computer Science Royal Holloway University of London Egham United Kingdom Algorithms and Complexity Group TU Wien Vienna Austria School of Computing DePaul University Chicago United States Department of Computer Science University of Warwick United Kingdom

We study a variant of the Coordinated Motion Planning problem on undirected graphs, referred to herein as the Coordinated Sliding-Motion Planning (CSMP) problem. In this variant, we are given an undirected graph G, k robots R1, . . ., Rk positioned on distinct vertices of G, p ≤ k distinct destination vertices for robots R1, . . ., Rp, and ∈ . The problem is to decide if there is a serial schedule of at most moves (i.e., of makespan ) such that at the end of the schedule each robot with a destination reaches it, where a robot’s move is a free path (unoccupied by any robots) from its current position to an unoccupied vertex. The problem is known to be NP-hard even on full grids. It has been studied in several contexts, including coin movement and reconfiguration problems, with respect to feasibility, complexity, and approximation. Geometric variants of the problem, in which congruent geometric-shape robots (e.g., unit disk/squares) slide or translate in the Euclidean plane, have also been studied extensively. We investigate the parameterized complexity of CSMP with respect to two parameters: the number k of robots and the makespan . As our first result, we present a fixed-parameter algorithm for CSMP parameterized by k. For our second result, we present a fixed-parameter algorithm parameterized by for the special case of CSMP in which only a single robot has a destination and the graph is planar, which we prove to be NP-complete. A crucial new ingredient for both of our results is that the solution admits a succinct representation as a small labeled topological minor of the input graph. © 2025, CC BY-NC-ND.

关键词： Undirected graphs

Splitting Plane Graphs to Outerplanarity

学校读者我要写书评

暂无评论

Journal of Graph algorithms and Applications 2024年第3期28卷 31-48页

作者： 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. Additionally, we show upper and lower bounds for certain families of maximal planar graphs. Finally, we provide a SAT formulation for the problem, and evaluate it on a small benchmark. © 2024, Brown University. All rights reserved.

关键词： Polynomial approximation