scholarly journals Abstract Cores in Implicit Hitting Set MaxSat Solving (Extended Abstract)

2021 ◽  
Author(s):  
Jeremias Berg ◽  
Fahiem Bacchus ◽  
Alex Poole
Keyword(s):  
Linear Programming ◽  
Optimization Problems ◽  
State Of The Art ◽  
Empirical Evaluation ◽  
Boolean Satisfiability ◽  
Compact Representation ◽  
Maximum Satisfiability ◽  
Hitting Set ◽  
Combinatorial Optimization Problems ◽  
Core Extraction

Maximum satisfiability (MaxSat) solving is an active area of research motivated by numerous successful applications to solving NP-hard combinatorial optimization problems. One of the most successful approaches for solving MaxSat instances from real world domains are the so called implicit hitting set (IHS) solvers. IHS solvers decouple MaxSat solving into separate core-extraction (i.e. reasoning) and optimization steps which are tackled by a Boolean satisfiability (SAT) and an integer linear programming (IP) solver, respectively. While the approach shows state-of-the-art performance on many industrial instances, it is known that there exists instances on which IHS solvers need to extract an exponential number of cores before terminating. Motivated by the simplest of these problematic instances, we propose abstract cores, a compact representation for a potentially exponential number of regular cores. We demonstrate how to incorporate abstract core reasoning into the IHS algorithm and report on an empirical evaluation demonstrating, that including abstract cores into a state-of-the-art IHS solver improves its performance enough to surpass the best performing solvers of the 2019 MaxSat Evaluation.

scholarly journals Reduced Cost Fixing for Maximum Satisfiability

2018 ◽  
Author(s):  
Fahiem Bacchus ◽  
Antti Hyttinen ◽  
Matti Järvisalo ◽  
Paul Saikko
Keyword(s):  
Integer Programming ◽  
Real World ◽  
Recent Trend ◽  
Optimization Problems ◽  
State Of The Art ◽  
Boolean Satisfiability ◽  
Maximum Satisfiability ◽  
Hitting Set ◽  
Sat Solvers ◽  
Speed Up

Maximum satisfiability (MaxSAT) offers a competitive approach to solving NP-hard real-world optimization problems. While state-of-the-art MaxSAT solvers rely heavily on Boolean satisfiability (SAT) solvers, a recent trend, brought on by MaxSAT solvers implementing the so-called implicit hitting set (IHS) approach, is to integrate techniques from the realm of integer programming (IP) into the solving process. This allows for making use of additional IP solving techniques to further speed up MaxSAT solving. In this line of work, we investigate the integration of the technique of reduced cost fixing from the IP realm into IHS solvers, and empirically show that reduced cost fixing considerable speeds up a state-of-the-art MaxSAT solver implementing the IHS approach.

Boosting branch-and-bound MaxSAT solvers with clause learning

2021 ◽  
pp. 1-21
Author(s):  
Chu-Min Li ◽  
Zhenxing Xu ◽  
Jordi Coll ◽  
Felip Manyà ◽  
Djamal Habet ◽  
...  
Keyword(s):  
Experimental Investigation ◽  
Combinatorial Optimization ◽  
Problem Solving ◽  
Branch And Bound ◽  
Real World ◽  
Optimization Problems ◽  
Satisfiability Problem ◽  
Maximum Satisfiability ◽  
Combinatorial Optimization Problems ◽  
Clause Learning

The Maximum Satisfiability Problem, or MaxSAT, offers a suitable problem solving formalism for combinatorial optimization problems. Nevertheless, MaxSAT solvers implementing the Branch-and-Bound (BnB) scheme have not succeeded in solving challenging real-world optimization problems. It is widely believed that BnB MaxSAT solvers are only superior on random and some specific crafted instances. At the same time, SAT-based MaxSAT solvers perform particularly well on real-world instances. To overcome this shortcoming of BnB MaxSAT solvers, this paper proposes a new BnB MaxSAT solver called MaxCDCL. The main feature of MaxCDCL is the combination of clause learning of soft conflicts and an efficient bounding procedure. Moreover, the paper reports on an experimental investigation showing that MaxCDCL is competitive when compared with the best performing solvers of the 2020 MaxSAT Evaluation. MaxCDCL performs very well on real-world instances, and solves a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best performing MaxSAT solvers, solves the highest number of instances of a collection from all the MaxSAT evaluations held so far.

scholarly journals AsymDPOP: Complete Inference for Asymmetric Distributed Constraint Optimization Problems

2019 ◽  
Author(s):  
Yanchen Deng ◽  
Ziyu Chen ◽  
Dingding Chen ◽  
Wenxin Zhang ◽  
Xingqiong Jiang
Keyword(s):  
Optimization Problems ◽  
State Of The Art ◽  
Empirical Evaluation ◽  
The State ◽  
Constraint Optimization ◽  
Memory Consumption ◽  
Distributed Constraint Optimization ◽  
Constraint Optimization Problems

Asymmetric distributed constraint optimization problems (ADCOPs) are an emerging model for coordinating agents with personal preferences. However, the existing inference-based complete algorithms which use local eliminations cannot be applied to ADCOPs, as the parent agents are required to transfer their private functions to their children. Rather than disclosing private functions explicitly to facilitate local eliminations, we solve the problem by enforcing delayed eliminations and propose AsymDPOP, the first inference-based complete algorithm for ADCOPs. To solve the severe scalability problems incurred by delayed eliminations, we propose to reduce the memory consumption by propagating a set of smaller utility tables instead of a joint utility table, and to reduce the computation efforts by sequential optimizations instead of joint optimizations. The empirical evaluation indicates that AsymDPOP significantly outperforms the state-of-the-art, as well as the vanilla DPOP with PEAV formulation.

scholarly journals Bin Completion Algorithms for Multicontainer Packing, Knapsack, and Covering Problems

2007 ◽  
Vol 28 ◽  
pp. 393-429 ◽  
Author(s):  
A. S. Fukunaga ◽  
R. E. Korf
Keyword(s):  
Bin Packing ◽  
Optimization Problems ◽  
State Of The Art ◽  
Cutting Stock ◽  
Multi Agent Systems ◽  
Covering Problems ◽  
Combinatorial Optimization Problems ◽  
Bin Covering ◽  
Multiple Knapsack ◽  
Dominance Criterion

Many combinatorial optimization problems such as the bin packing and multiple knapsack problems involve assigning a set of discrete objects to multiple containers. These problems can be used to model task and resource allocation problems in multi-agent systems and distributed systms, and can also be found as subproblems of scheduling problems. We propose bin completion, a branch-and-bound strategy for one-dimensional, multicontainer packing problems. Bin completion combines a bin-oriented search space with a powerful dominance criterion that enables us to prune much of the space. The performance of the basic bin completion framework can be enhanced by using a number of extensions, including nogood-based pruning techniques that allow further exploitation of the dominance criterion. Bin completion is applied to four problems: multiple knapsack, bin covering, min-cost covering, and bin packing. We show that our bin completion algorithms yield new, state-of-the-art results for the multiple knapsack, bin covering, and min-cost covering problems, outperforming previous algorithms by several orders of magnitude with respect to runtime on some classes of hard, random problem instances. For the bin packing problem, we demonstrate significant improvements compared to most previous results, but show that bin completion is not competitive with current state-of-the-art cutting-stock based approaches.

scholarly journals Cardinality Encodings for Graph Optimization Problems

2017 ◽  
Author(s):  
Alexey Ignatiev ◽  
Antonio Morgado ◽  
Joao Marques-Silva
Keyword(s):  
Optimization Problems ◽  
State Of The Art ◽  
Maximum Clique ◽  
Maximum Clique Problem ◽  
Concrete Case ◽  
Large Graphs ◽  
Sparse Graphs ◽  
Maximum Satisfiability ◽  
Graph Optimization ◽  
Sparse Networks

Different optimization problems defined on graphs find application in complex network analysis. Existing propositional encodings render impractical the use of propositional satisfiability (SAT) and maximum satisfiability (MaxSAT) solvers for solving a variety of these problems on large graphs. This paper has two main contributions. First, the paper identifies sources of inefficiency in existing encodings for different optimization problems in graphs. Second, for the concrete case of the maximum clique problem, the paper develops a novel encoding which is shown to be far more compact than existing encodings for large sparse graphs. More importantly, the experimental results show that the proposed encoding enables existing SAT solvers to compute a maximum clique for large sparse networks, often more efficiently than the state of the art.

scholarly journals Searching for the M Best Solutions in Graphical Models

2016 ◽  
Vol 55 ◽  
pp. 889-952 ◽  
Author(s):  
Natalia Flerova ◽  
Radu Marinescu ◽  
Rina Dechter
Keyword(s):  
Branch And Bound ◽  
Graphical Models ◽  
Complexity Analysis ◽  
Optimization Problems ◽  
Empirical Evaluation ◽  
Combinatorial Optimization Problems ◽  
Optimal Efficiency ◽  
Weighted Csp ◽  
First Time ◽  
Memory Efficient

The paper focuses on finding the m best solutions to combinatorial optimization problems using best-first or depth-first branch and bound search. Specifically, we present a new algorithm m-A*, extending the well-known A* to the m-best task, and for the first time prove that all its desirable properties, including soundness, completeness and optimal efficiency, are maintained. Since best-first algorithms require extensive memory, we also extend the memory-efficient depth-first branch and bound to the m-best task. We adapt both algorithms to optimization tasks over graphical models (e.g., Weighted CSP and MPE in Bayesian networks), provide complexity analysis and an empirical evaluation. Our experiments confirm theory that the best-first approach is largely superior when memory is available, but depth-first branch and bound is more robust. We also show that our algorithms are competitive with related schemes recently developed for the m-best task.

Sign in / Sign up

Export Citation Format

Share Document