Related papers: UpMax: User partitioning for MaxSAT

UpMax: User partitioning for MaxSAT

URL: http://arxiv.org/abs/2305.16191v1
Date: Thu, 25 May 2023 15:50:00 GMT
Title: UpMax: User partitioning for MaxSAT
Authors: Pedro Orvalho and Vasco Manquinho and Ruben Martins
Abstract summary: 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.
Score: 2.2022484178680872
License: http://creativecommons.org/licenses/by-nc-sa/4.0/
Abstract: It has been shown that Maximum Satisfiability (MaxSAT) problem instances can be effectively solved by partitioning the set of soft clauses into several disjoint sets. The partitioning methods can be based on clause weights (e.g., stratification) or based on graph representations of the formula. Afterwards, a merge procedure is applied to guarantee that an optimal solution is found. This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms. As a result, new partitioning procedures can be defined independently of the MaxSAT algorithm to be used. Moreover, this decoupling also allows users that build new MaxSAT formulas to propose partition schemes based on knowledge of the problem to be solved. We illustrate this approach using several problems and show that partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms.

Related papers

Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers [20.866863965121013]
MaxSAT is an optimization version of the famous NP-complete Satisfiability problem (SAT) We propose a new local search algorithm called SPB-MaxSAT that provides new perspectives for clause weighting on MaxSAT local search solvers.
arXiv Detail & Related papers (2024-01-19T09:59:02Z)
Combinatorial Stochastic-Greedy Bandit [79.1700188160944]
We propose a novelgreedy bandit (SGB) algorithm for multi-armed bandit problems when no extra information other than the joint reward of the selected set of $n$ arms at each time $tin [T]$ is observed. SGB adopts an optimized-explore-then-commit approach and is specifically designed for scenarios with a large set of base arms.
arXiv Detail & Related papers (2023-12-13T11:08:25Z)
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)
Incorporating Multi-armed Bandit with Local Search for MaxSAT [16.371916145216737]
Two generalizations of the MaxSAT problem: Partial MaxSAT (PMS) and Weighted PMS (WPMS) We propose a local search algorithm for these problems, called BandHS, which applies two multi-armed bandits to guide the search directions when escaping local optima. These two bandits can improve the algorithm's search ability in both feasible and infeasible solution spaces.
arXiv Detail & Related papers (2022-11-29T08:19:26Z)
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)
Constrained mixers for the quantum approximate optimization algorithm [55.41644538483948]
We present a framework for constructing mixing operators that restrict the evolution to a subspace of the full Hilbert space. We generalize the "XY"-mixer designed to preserve the subspace of "one-hot" states to the general case of subspaces given by a number of computational basis states. Our analysis also leads to valid Trotterizations for "XY"-mixer with fewer CX gates than is known to date.
arXiv Detail & Related papers (2022-03-11T17:19:26Z)
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)
Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
We propose the setting of extreme algorithm selection (XAS) where we consider fixed sets of thousands of candidate algorithms. We assess the applicability of state-of-the-art AS techniques to the XAS setting and propose approaches leveraging a dyadic feature representation.
arXiv Detail & Related papers (2020-01-29T09:40:58Z)

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