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

Small unsatisfiable k-CNFs with bounded literal occurrence

学校读者我要写书评

暂无评论

arXiv 2024年

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

We obtain the smallest unsatisfiable formulas in subclasses of k-CNF (exactly k distinct literals per clause) with bounded variable or literal occurrences. Smaller unsatisfiable formulas of this type translate into stronger inapproximability results for MaxSAT in the considered formula class. Our results cover subclasses of 3-CNF and 4-CNF;in all subclasses of 3-CNF we considered we were able to determine the smallest size of an unsatisfiable formula;in the case of 4-CNF with at most 5 occurrences per variable we decreased the size of the smallest known unsatisfiable formula. Our methods combine theoretical arguments and symmetry-breaking exhaustive search based on SAT Modulo Symmetries (SMS), a recent framework for isomorph-free SAT-based graph generation. To this end, and as a standalone result of independent interest, we show how to encode formulas as graphs efficiently for SMS. Copyright © 2024, The Authors. All rights reserved.

关键词： Formal logic

Crossing-optimal extension of simple drawings 48

学校读者我要写书评

暂无评论

Crossing-optimal extension of simple drawings

48th International Colloquium on Automata, Languages, and Programming, ICALP 2021

作者： Ganian, Robert Hamm, Thekla Klute, Fabian Parada, Irene Vogtenhuber, Birgit Algorithms and Complexity Group TU Wien Austria Deptartment of Information and Computing Sciences Utrecht University Netherlands TU Eindhoven Netherlands Graz University of Technology Austria

ISBN: (纸本)9783959771955

In extension problems of partial graph drawings one is given an incomplete drawing of an input graph G and is asked to complete the drawing while maintaining certain properties. A prominent area where such problems arise is that of crossing minimization. For plane drawings and various relaxations of these, there is a number of tractability as well as lower-bound results exploring the computational complexity of crossing-sensitive drawing extension problems. In contrast, comparatively few results are known on extension problems for the fundamental and broad class of simple drawings, that is, drawings in which each pair of edges intersects in at most one point. In fact, the extension problem of simple drawings has only recently been shown to be NP-hard even for inserting a single edge. In this paper we present tractability results for the crossing-sensitive extension problem of simple drawings. In particular, we show that the problem of inserting edges into a simple drawing is fixed-parameter tractable when parameterized by the number of edges to insert and an upper bound on newly created crossings. Using the same proof techniques, we are also able to answer several closely related variants of this problem, among others the extension problem for k-plane drawings. Moreover, using a different approach, we provide a single-exponential fixed-parameter algorithm for the case in which we are only trying to insert a single edge into the drawing. © 2021 Robert Ganian, Thekla Hamm, Fabian Klute, Irene Parada, and Birgit Vogtenhuber.

关键词： Drawing (graphics)

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

Generating Streamlining Constraints with Large Language Models

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Voboril, Florentina Ramaswamy, Vaidyanathan Peruvemba Szeider, Stefan Algorithms and Complexity Group TU Wien Vienna Austria

Streamlining constraints (or streamliners, for short) narrow the search space, enhancing the speed and feasibility of solving complex constraint satisfaction problems. Traditionally, streamliners were crafted manually or generated through systematically combined atomic constraints with high-effort offline testing. Our approach utilizes the creativity of Large Language Models (LLMs) to propose effective streamliners for problems specified in the MiniZinc constraint programming language and integrates feedback to the LLM with quick empirical tests for validation. Evaluated across seven diverse constraint satisfaction problems, our method achieves substantial runtime reductions. We compare the results to obfuscated and disguised variants of the problem to see whether the results depend on LLM memorization. We also analyze whether longer off-line runs improve the quality of streamliners and whether the LLM can propose good combinations of streamliners. Copyright © 2024, The Authors. All rights reserved.

关键词： Constraint satisfaction problems

MCP-Solver: Integrating Language Models with Constraint Programming Systems

学校读者我要写书评

暂无评论

arXiv 2024年

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

While Large Language Models (LLMs) perform exceptionally well at natural language tasks, they often struggle with precise formal reasoning and the rigorous specification of problems. We present MCP-Solver, a prototype implementation of the Model Context Protocol that demonstrates the potential for systematic integration between LLMs and constraint programming systems. Our implementation provides interfaces for the creation, editing, and validation of a constraint model. Through an item-based editing approach with integrated validation, the system ensures model consistency at every modification step and enables structured iterative refinement. The system handles concurrent solving sessions and maintains a persistent knowledge base of modeling insights. Initial experiments suggest that this integration can effectively combine LLMs’ natural language understanding with constraint-solving capabilities. Our open-source implementation is proof of concept for integrating formal reasoning systems with LLMs through standardized protocols. While further research is needed to establish comprehensive formal guarantees, this work takes a first step toward principled integration of natural language processing with constraint-based reasoning. Copyright © 2024, The Authors. All rights reserved.

关键词： Constraint programming

On structural parameterizations of the edge disjoint paths problem

学校读者我要写书评

暂无评论

arXiv 2017年

作者： Ganian, Robert Ordyniak, Sebastian Ramanujan, M.S. Algorithms and Complexity group TU Wien Vienna Austria

In this paper we revisit the classical Edge Disjoint Paths (EDP) problem, where one is given an undirected graph G and a set of terminal pairs P and asks whether G contains a set of pairwise edge-disjoint paths connecting every terminal pair in P. Our focus lies on structural parameterizations for the problem that allow for efficient (polynomial-time or fpt) algorithms. As our first result, we answer an open question stated in Fleszar, Mnich, and Spoerhase (2016), by showing that the problem can be solved in polynomial time if the input graph has a feedback vertex set of size one. We also show that EDP parameterized by the treewidth and the maximum degree of the input graph is fixed-parameter tractable. Having developed two novel algorithms for EDP using structural restrictions on the input graph, we then turn our attention towards the augmented graph, i.e., the graph obtained from the input graph after adding one edge between every terminal pair. In constrast to the input graph, where EDP is known to remain NP-hard even for treewidth two, a result by Zhou et al. (2000) shows that EDP can be solved in non-uniform polynomial time if the augmented graph has constant treewidth;we note that the possible improvement of this result to an fpt-algorithm has remained open since then. We show that this is highly unlikely by establishing the W[1]-hardness of the problem parameterized by the treewidth (and even feedback vertex set) of the augmented graph. Finally, we develop an fpt-algorithm for EDP by exploiting a novel structural parameter of the augmented graph. Copyright © 2017, The Authors. All rights reserved.

关键词： Parameterization

The Parameterized complexity of Extending Stack Layouts

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Depian, Thomas Fink, Simon D. Ganian, Robert Nöllenburg, Martin Algorithms and Complexity Group TU Wien Vienna Austria

An -page stack layout (also known as an -page book embedding) of a graph is a linear order of the vertex set together with a partition of the edge set into stacks (or pages), such that the endpoints of no two edges on the same stack alternate. We study the problem of extending a given partial -page stack layout into a complete one, which can be seen as a natural generalization of the classical NP-hard problem of computing a stack layout of an input graph from scratch. Given the inherent intractability of the problem, we focus on identifying tractable fragments through the refined lens of parameterized complexity analysis. Our results paint a detailed and surprisingly rich complexitytheoretic landscape of the problem which includes the identification of paraNP-hard, W[1]-hard and XP-tractable, as well as fixed-parameter tractable fragments of stack layout extension via a natural sequence of parameterizations. © 2024, CC BY.

关键词： Graph embeddings

Mixed Linear Layouts: complexity, Heuristics, and Experiments

学校读者我要写书评

暂无评论

arXiv 2019年

作者： de Col, Philipp Klute, Fabian Nöllenburg, Martin Algorithms and Complexity Group TU Wien Vienna Austria

A k-page linear graph layout of a graph G = (V, E) draws all vertices along a line and each edge in one of k disjoint halfplanes called pages, which are bounded by . We consider two types of pages. In a stack page no two edges should cross and in a queue page no edge should be nested by another edge. A crossing (nesting) in a stack (queue) page is called a conflict. The algorithmic problem is twofold and requires to compute (i) a vertex ordering and (ii) a page assignment of the edges such that the resulting layout is either conflict-free or conflict-minimal. While linear layouts with only stack or only queue pages are well-studied, mixed s-stack q-queue layouts for s, q ≥ 1 have received less attention. We show NP-completeness results on the recognition problem of certain mixed linear layouts and present a new heuristic for minimizing conflicts. In a computational experiment for the case s, q = 1 we show that the new heuristic is an improvement over previous heuristics for linear layouts. Copyright © 2019, The Authors. All rights reserved.

关键词： Queueing theory

A SAT Approach to Twin-Width

学校读者我要写书评

暂无评论

arXiv 2021年

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

The graph invariant twin-width was recently introduced by Bonnet, Kim, Thomassé, and Watrigan. Problems expressible in first-order logic, which includes many prominent NP-hard problems, are tractable on graphs of bounded twin-width if a certificate for the twin-width bound is provided as an input. Computing such a certificate, however, is an intrinsic problem, for which no nontrivial algorithm is known. In this paper, we propose the first practical approach for computing the twin-width of graphs together with the corresponding certificate. We propose efficient SAT-encodings that rely on a characterization of twin-width based on elimination sequences. This allows us to determine the twin-width of many famous graphs with previously unknown twin-width. We utilize our encodings to identify the smallest graphs for a given twin-width bound d ∈ {1, . . ., 4}. Copyright © 2021, The Authors. All rights reserved.

关键词： Encoding (symbols)