Exploiting Configurations of MaxSAT Solvers

• URL: http://arxiv.org/abs/2306.07635v1
• Date: Tue, 13 Jun 2023 09:11:17 GMT
• Title: Exploiting Configurations of MaxSAT Solvers
• Authors: Josep Al\`os, Carlos Ans\'otegui, Josep M. Salvia, Eduard Torres
• Abstract summary: We describe how these configurations can be computed in the context of MaxSAT. In particular, we experimentally show how to easily combine configurations of a non-competitive solver to obtain a better solving approach.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: In this paper, we describe how we can effectively exploit alternative parameter configurations to a MaxSAT solver. We describe how these configurations can be computed in the context of MaxSAT. In particular, we experimentally show how to easily combine configurations of a non-competitive solver to obtain a better solving approach.

Related papers

• Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
  We propose a resource-constrained for instances of Max-SAT that iteratively decomposes a larger problem into smaller subcomponents. We analyze a set of variable selection methods, including a novel graph-based method that exploits the structure of a given SAT instance. We demonstrate our results on a set of randomly generated Max-SAT instances as well as real world examples from the Max-SAT evaluation benchmarks.
  arXiv  Detail & Related papers  (2024-10-11T18:20:08Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  We derive a single differentiable function capable of approximating solutions for the Maximum Satisfiability Problem (MaxSAT) We present a novel neural network architecture to model our differentiable function, and progressively solve MaxSAT using backpropagation.
  arXiv  Detail & Related papers  (2024-02-06T02:33:00Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
  arXiv  Detail & Related papers  (2023-12-16T12:44:36Z)
• UpMax: User partitioning for MaxSAT [2.2022484178680872]
  partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms. This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms.
  arXiv  Detail & Related papers  (2023-05-25T15:50:00Z)
• MultiZenoTravel: a Tunable Benchmark for Multi-Objective Planning with Known Pareto Front [71.19090689055054]
  Multi-objective AI planning suffers from a lack of benchmarks exhibiting known Pareto Fronts. We propose a tunable benchmark generator, together with a dedicated solver that provably computes the true Pareto front of the resulting instances. We show how to characterize the optimal plans for a constrained version of the problem, and then show how to reduce the general problem to the constrained one.
  arXiv  Detail & Related papers  (2023-04-28T07:09:23Z)
• Tree ensemble kernels for Bayesian optimization with known constraints over mixed-feature spaces [54.58348769621782]
  Tree ensembles can be well-suited for black-box optimization tasks such as algorithm tuning and neural architecture search. Two well-known challenges in using tree ensembles for black-box optimization are (i) effectively quantifying model uncertainty for exploration and (ii) optimizing over the piece-wise constant acquisition function. Our framework performs as well as state-of-the-art methods for unconstrained black-box optimization over continuous/discrete features and outperforms competing methods for problems combining mixed-variable feature spaces and known input constraints.
  arXiv  Detail & Related papers  (2022-07-02T16:59:37Z)
• DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving [45.21499915442282]
  We propose a novel dynamic-programming approach for solving generalized MaxSAT problems with hybrid constraints. Our versatile framework admits many generalizations of CNF-MaxSAT, such as MaxSAT, Min-MaxSAT, and MinSAT with hybrid constraints. Empirical results indicate that DPMS is able to solve certain problems quickly, where other algorithms based on various techniques all fail.
  arXiv  Detail & Related papers  (2022-05-08T00:31:53Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
  We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length. This problem is central in Combinatorial Testing for the detection of system failures.
  arXiv  Detail & Related papers  (2021-05-26T14:00:56Z)
• Fault Tree Analysis: Identifying Maximum Probability Minimal Cut Sets with MaxSAT [0.342658286826597]
  We model the MPMCS problem as a weighted Partial MaxSAT problem and solve it using a parallel SAT-solving architecture. The results obtained with our open source tool indicate that the approach is effective and efficient.
  arXiv  Detail & Related papers  (2020-05-05T19:47:15Z)
• Compositional ADAM: An Adaptive Compositional Solver [69.31447856853833]
  C-ADAM is the first adaptive solver for compositional problems involving a non-linear functional nesting of expected values. We prove that C-ADAM converges to a stationary point in $mathcalO(delta-2.25)$ with $delta$ being a precision parameter.
  arXiv  Detail & Related papers  (2020-02-10T14:00:45Z)

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.