Advanced Tools and Methods for Treewidth-Based Problem Solving -- Extended Abstract

• URL: http://arxiv.org/abs/2208.11340v1
• Date: Wed, 24 Aug 2022 07:43:58 GMT
• Title: Advanced Tools and Methods for Treewidth-Based Problem Solving -- Extended Abstract
• Authors: Markus Hecher
• Abstract summary: This work focuses on logic-based problems and treewidth-based methods and tools for solving them. We present a new type of problem reduction, which is referred to by decomposition-guided (DG) We implement an algorithm for solving extensions of Sat efficiently, by directly using treewidth.
• Score: 9.480212602202517
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Computer programs, so-called solvers, for solving the well-known Boolean satisfiability problem (Sat) have been improving for decades. Among the reasons, why these solvers are so fast, is the implicit usage of the formula's structural properties during solving. One of such structural indicators is the so-called treewidth, which tries to measure how close a formula instance is to being easy (tree-like). This work focuses on logic-based problems and treewidth-based methods and tools for solving them. Many of these problems are also relevant for knowledge representation and reasoning (KR) as well as artificial intelligence (AI) in general. We present a new type of problem reduction, which is referred to by decomposition-guided (DG). This reduction type forms the basis to solve a problem for quantified Boolean formulas (QBFs) of bounded treewidth that has been open since 2004. The solution of this problem then gives rise to a new methodology for proving precise lower bounds for a range of further formalisms in logic, KR, and AI. Despite the established lower bounds, we implement an algorithm for solving extensions of Sat efficiently, by directly using treewidth. Our implementation is based on finding abstractions of instances, which are then incrementally refined in the process. Thereby, our observations confirm that treewidth is an important measure that should be considered in the design of modern solvers.

Related papers

• Solving Projected Model Counting by Utilizing Treewidth and its Limits [23.81311815698799]
  We introduce a novel algorithm to solve projected model counting (PMC) Inspired by the observation that the so-called "treewidth" is one of the most prominent structural parameters, our algorithm utilizes small treewidth of the primal graph of the input instance.
  arXiv  Detail & Related papers  (2023-05-30T17:02:07Z)
• FastDiagP: An Algorithm for Parallelized Direct Diagnosis [64.65251961564606]
  FastDiag is a typical direct diagnosis algorithm that supports diagnosis calculation without predetermining conflicts. We propose a novel algorithm, so-called FastDiagP, which is based on the idea of speculative programming. This mechanism helps to provide consistency checks with fast answers and boosts the algorithm's runtime performance.
  arXiv  Detail & Related papers  (2023-05-11T16:26:23Z)
• NeuroPrim: An Attention-based Model for Solving NP-hard Spanning Tree Problems [0.0]
  We propose NeuroPrim, a novel framework for solving various spanning tree problems by defining a Decision Process (MDP) for general optimization problems on graphs. We apply our framework to three difficult problems on Euclidean space: the Degree-constrained Minimum Spanning Tree (DCMST) problem, the Minimum Cost Spanning Tree (MRCST) problem, and the Steiner Tree Problem in Routing graphs (STP)
  arXiv  Detail & Related papers  (2022-10-22T13:49:29Z)
• Efficient Knowledge Compilation Beyond Weighted Model Counting [7.828647825246474]
  We introduce Second Level Algebraic Model Counting (2AMC) as a generic framework for these kinds of problems. First level techniques based on Knowledge Compilation (KC) have been adapted for specific 2AMC instances by imposing variable order constraints. We show that we can exploit the logical structure of a 2AMC problem to omit parts of these constraints, thus limiting the negative effect.
  arXiv  Detail & Related papers  (2022-05-16T08:10:40Z)
• What's Wrong with Deep Learning in Tree Search for Combinatorial Optimization [8.879790406465556]
  We present an open-source benchmark suite for the NP-hard Maximum Independent Set problem, in both its weighted and unweighted variants. We also conduct an in-depth analysis of the popular guided tree search algorithm by Li et al. [NeurIPS 2018], testing various configurations on small and large synthetic and real-world graphs. We show that the graph convolution network used in the tree search does not learn a meaningful representation of the solution structure, and can in fact be replaced by random values.
  arXiv  Detail & Related papers  (2022-01-25T17:37:34Z)
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition [161.09660864941603]
  We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. We present a novel activation-based branching strategy and a BaB framework, named Branch and Dual Network Bound (BaDNB) BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial properties.
  arXiv  Detail & Related papers  (2021-04-14T09:22:42Z)
• Accelerating Recursive Partition-Based Causal Structure Learning [4.357523892518871]
  Recursive causal discovery algorithms provide good results by using Conditional Independent (CI) tests in smaller sub-problems. This paper proposes a generic causal structure refinement strategy that can locate the undesired relations with a small number of CI-tests. We then empirically evaluate its performance against the state-of-the-art algorithms in terms of solution quality and completion time in synthetic and real datasets.
  arXiv  Detail & Related papers  (2021-02-23T08:28:55Z)
• Learning by Fixing: Solving Math Word Problems with Weak Supervision [70.62896781438694]
  Previous neural solvers of math word problems (MWPs) are learned with full supervision and fail to generate diverse solutions. We introduce a textitweakly-supervised paradigm for learning MWPs. Our method only requires the annotations of the final answers and can generate various solutions for a single problem.
  arXiv  Detail & Related papers  (2020-12-19T03:10:21Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  We present a novel approach to formulate different notions of causal reasoning, over binary acyclic models, as optimization problems. We show that both notions are efficiently automated. Using models with more than $8000$ variables, checking is computed in a matter of seconds, with MaxSAT outperforming ILP in many cases.
  arXiv  Detail & Related papers  (2020-06-05T10:56:52Z)
• Learning to Accelerate Heuristic Searching for Large-Scale Maximum Weighted b-Matching Problems in Online Advertising [51.97494906131859]
  Bipartite b-matching is fundamental in algorithm design, and has been widely applied into economic markets, labor markets, etc. Existing exact and approximate algorithms usually fail in such settings due to either requiring intolerable running time or too much computation resource. We propose textttNeuSearcher which leverages the knowledge learned from previously instances to solve new problem instances.
  arXiv  Detail & Related papers  (2020-05-09T02:48:23Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  A fundamental component of neural network verification is the computation of bounds on the values their outputs can take. We propose a novel approach based on Lagrangian Decomposition. We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
  arXiv  Detail & Related papers  (2020-02-24T17:55:10Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.