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

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

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

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

A Structural complexity Analysis of Hierarchical Task Network Planning

学校读者我要写书评

暂无评论

arXiv 2024年

作者： Brand, Cornelius Ganian, Robert Inerney, Fion Mc Wietheger, Simon Algorithms & Complexity Theory Group Regensburg University Germany Algorithms and Complexity Group TU Wien Austria Telefónica Scientific Research Barcelona Spain

We perform a refined complexity-theoretic analysis of three classical problems in the context of Hierarchical Task Network Planning: the verification of a provided plan, whether an executable plan exists, and whether a given state can be reached. Our focus lies on identifying structural properties which yield tractability. We obtain new polynomial algorithms for all three problems on a natural class of primitive networks, along with corresponding lower bounds. We also obtain an algorithmic meta-theorem for lifting polynomial-time solvability from primitive to general task networks, and prove that its preconditions are tight. Finally, we analyze the parameterized complexity of the three problems. Copyright © 2024, The Authors. All rights reserved.

关键词： Complex networks

A Relative Value Function Based Learning Beam Search for the Longest Common Subsequence Problem 18th

学校读者我要写书评

暂无评论

A Relative Value Function Based Learning Beam Search for th...

18th International Conference on Computer Aided Systems Theory, EUROCAST 2022

作者： Huber, M. Raidl, G.R. Algorithms and Complexity Group Institute of Logic and Computation TU Wien Vienna Austria

ISBN: (纸本)9783031253119

Beam search (BS) is a well-known graph search algorithm frequently used to heuristically find good or near-optimal solutions to combinatorial optimization problems. Its most crucial component is a heuristic function that estimates the best achievable length-to-go from any state to a goal state. This function usually needs to be developed specificially for a problem at hand, which is a manual and time-consuming process. Building on previous work, we propose a Relative Value Function Based Learning Beam Search (RV-LBS) to automate this task at least partially by using a multilayer perceptron (MLP) as heuristic function, which is trained in a reinforcement learning manner on many randomly created problem instances. This MLP predicts the difference of the expected solution length from a given state to the expected average solution length of all states at a current BS level. To support the training of the MLP on the longest common subsequence (LCS) problem, a compact fixed-size encoding of the distribution of differences of remaining string lengths to the average string length at the current level is presented. Tests show that a MLP trained by RV-LBS on randomly created small-size problem instances is able to guide BS well also on larger established LCS benchmark instances. The obtained results are highly competitive to the state-of-the-art. © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

关键词： Benchmarking

学校读者我要写书评

暂无评论

Backdoor Dnfs

SSRN

SSRN 2023年

作者： Ordyniak, Sebastian Schidler, Andre Szeider, Stefan Algorithms and Complexity Group TU Wien Vienna Austria Algorithms and Complexity Group University of Leeds United Kingdom

We introduce backdoor DNFs, as a tool to measure the theoretical hardness of CNF formulas. Like backdoor sets and backdoor trees, backdoor DNFs are defined relative to a tractable class of CNF formulas. Each conjunctive term of a backdoor DNF defines a partial assignment that moves the input CNF formula into the base class. Backdoor DNFs are more expressive and potentially smaller than their predecessors backdoor sets and backdoor trees. We establish the fixed-parameter tractability of the backdoor DNF detection problem. Our results hold for the fundamental base classes Horn and 2CNF, and their combination. We complement our theoretical findings by an empirical study. Our experiments show that backdoor DNFs provide a significant improvement over their predecessors. © 2023, The Authors. All rights reserved.

关键词：

FPT Approximation for Fair Minimum-Load Clustering 17

学校读者我要写书评

暂无评论

FPT Approximation for Fair Minimum-Load Clustering

17th International Symposium on Parameterized and Exact Computation, IPEC 2022

作者： Bandyapadhyay, Sayan Fomin, Fedor V. Golovach, Petr A. Purohit, Nidhi Simonov, Kirill Department of Informatics University of Bergen Norway Algorithms and Complexity Group TU Wien Austria

ISBN: (纸本)9783959772600

In this paper, we consider the Minimum-Load k-Clustering/Facility Location (MLkC) problem where we are given a set P of n points in a metric space that we have to cluster and an integer k > 0 that denotes the number of clusters. Additionally, we are given a set F of cluster centers in the same metric space. The goal is to select a set C ⊆ F of k centers and assign each point in P to a center in C, such that the maximum load over all centers is minimized. Here the load of a center is the sum of the distances between it and the points assigned to it. Although clustering/facility location problems have rich literature, the minimum-load objective has not been studied substantially, and hence MLkC has remained a poorly understood problem. More interestingly, the problem is notoriously hard even in some special cases including the one in line metrics as shown by Ahmadian et al. [APPROX 2014, ACM Trans. algorithms 2018]. They also show APX-hardness of the problem in the plane. On the other hand, the best-known approximation factor for MLkC is O(k), even in the plane. In this work, we study a fair version of MLkC inspired by the work of Chierichetti et al. [NeurIPS, 2017]. Here the input points are partitioned into protected groups, and only clusters that proportionally represent each group are allowed. MLkC is the special case with = 1. For the fair version, we are able to obtain a randomized 3-approximation algorithm in f(k, ) · nO(1) time. Also, our scheme leads to an improved (1 + ϵ)-approximation in the case of Euclidean norm with the same running time (depending also linearly on the dimension d). Our results imply the same approximations for MLkC with running time f(k) · nO(1), achieving the first constant-factor FPT approximations for this problem in general and Euclidean metric spaces. © Sayan Bandyapadhyay, Fedor V. Fomin, Petr A. Golovach, Nidhi Purohit, and Kirill Simonov.

关键词： Topology

Weighted Model Counting with Twin-Width 25

学校读者我要写书评

暂无评论

Weighted Model Counting with Twin-Width

25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022

作者： Ganian, Robert Pokrývka, Filip Schidler, André Simonov, Kirill Szeider, Stefan Algorithms and Complexity Group TU Wien Austria Masaryk University Brno Czech Republic

ISBN: (纸本)9783959772426

Bonnet et al. (FOCS 2020) introduced the graph invariant twin-width and showed that many NP-hard problems are tractable for graphs of bounded twin-width, generalizing similar results for other width measures, including treewidth and clique-width. In this paper, we investigate the use of twin-width for solving the propositional satisfiability problem (SAT) and propositional model counting. We particularly focus on Bounded-ones Weighted Model Counting (BWMC), which takes as input a CNF formula F along with a bound k and asks for the weighted sum of all models with at most k positive literals. BWMC generalizes not only SAT but also (weighted) model counting. We develop the notion of "signed" twin-width of CNF formulas and establish that BWMC is fixed-parameter tractable when parameterized by the certified signed twin-width of F plus k. We show that this result is tight: it is neither possible to drop the bound k nor use the vanilla twin-width instead if one wishes to retain fixed-parameter tractability, even for the easier problem SAT. Our theoretical results are complemented with an empirical evaluation and comparison of signed twin-width on various classes of CNF formulas. © Robert Ganian, Filip Pokrývka, André Schidler, Kirill Simonov, and Stefan Szeider.

关键词： Computational complexity

MySemCloud: Semantic-aware Word Cloud Editing

学校读者我要写书评

暂无评论

MySemCloud: Semantic-aware Word Cloud Editing

Pacific (formerly Asia-Pacific APVIS) Visualization Symposium

作者： Michael Huber Martin Nöllenburg Anaïs Villedieu Algorithms and Complexity Group TU Wien

Word clouds are a popular text visualization technique that summarize an input text by displaying its most important words in a compact image. The traditional layout methods do not take proximity effects between words into account; this has been improved in semantic word clouds, where relative word placement is controlled by edges in a word similarity graph. We introduce MySemCloud, a new human-in-the-loop tool to visualize and edit semantic word clouds. MySemCloud lets users perform computer-assisted local moves of words, which improve or at least retain the semantic quality. To achieve this, we construct a word similarity graph on which a system of forces is applied to generate a compact initial layout with good semantic quality. The force system also allows us to maintain these attributes after each user interaction, as well as preserve the user’s mental map. The tool provides algorithmic support for the editing operations to help the user enhance the semantic quality of the visualization, while adjusting it to their personal preference. We show that MySemCloud provides high user satisfaction as well as permits users to create layouts of higher quality than state-of-the-art semantic word cloud generation tools.

关键词：