scholarly journals Reduced Cost Fixing for Maximum Satisfiability

Author(s):  
Fahiem Bacchus ◽  
Antti Hyttinen ◽  
Matti Järvisalo ◽  
Paul Saikko

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.

Author(s):  
Jeremias Berg ◽  
Fahiem Bacchus ◽  
Alex Poole

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.


2021 ◽  
pp. 1-21
Author(s):  
Chu-Min Li ◽  
Zhenxing Xu ◽  
Jordi Coll ◽  
Felip Manyà ◽  
Djamal Habet ◽  
...  

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.


2021 ◽  
Author(s):  
Mohammad Shehab ◽  
Laith Abualigah

Abstract Multi-Verse Optimizer (MVO) algorithm is one of the recent metaheuristic algorithms used to solve various problems in different fields. However, MVO suffers from a lack of diversity which may trapping of local minima, and premature convergence. This paper introduces two steps of improving the basic MVO algorithm. The first step using Opposition-based learning (OBL) in MVO, called OMVO. The OBL aids to speed up the searching and improving the learning technique for selecting a better generation of candidate solutions of basic MVO. The second stage, called OMVOD, combines the disturbance operator (DO) and OMVO to improve the consistency of the chosen solution by providing a chance to solve the given problem with a high fitness value and increase diversity. To test the performance of the proposed models, fifteen CEC 2015 benchmark functions problems, thirty CEC 2017 benchmark functions problems, and seven CEC 2011 real-world problems were used in both phases of the enhancement. The second step, known as OMVOD, incorporates the disruption operator (DO) and OMVO to improve the accuracy of the chosen solution by giving a chance to solve the given problem with a high fitness value while also increasing variety. Fifteen CEC 2015 benchmark functions problems, thirty CEC 2017 benchmark functions problems and seven CEC 2011 real-world problems were used in both phases of the upgrade to assess the accuracy of the proposed models.


2021 ◽  
Author(s):  
Leila Zahedi ◽  
Farid Ghareh Mohammadi ◽  
M. Hadi Amini

Machine learning techniques lend themselves as promising decision-making and analytic tools in a wide range of applications. Different ML algorithms have various hyper-parameters. In order to tailor an ML model towards a specific application, a large number of hyper-parameters should be tuned. Tuning the hyper-parameters directly affects the performance (accuracy and run-time). However, for large-scale search spaces, efficiently exploring the ample number of combinations of hyper-parameters is computationally challenging. Existing automated hyper-parameter tuning techniques suffer from high time complexity. In this paper, we propose HyP-ABC, an automatic innovative hybrid hyper-parameter optimization algorithm using the modified artificial bee colony approach, to measure the classification accuracy of three ML algorithms, namely random forest, extreme gradient boosting, and support vector machine. Compared to the state-of-the-art techniques, HyP-ABC is more efficient and has a limited number of parameters to be tuned, making it worthwhile for real-world hyper-parameter optimization problems. We further compare our proposed HyP-ABC algorithm with state-of-the-art techniques. In order to ensure the robustness of the proposed method, the algorithm takes a wide range of feasible hyper-parameter values, and is tested using a real-world educational dataset.


2020 ◽  
Vol 117 (38) ◽  
pp. 23393-23400 ◽  
Author(s):  
Amir Ghasemian ◽  
Homa Hosseinmardi ◽  
Aram Galstyan ◽  
Edoardo M. Airoldi ◽  
Aaron Clauset

Most real-world networks are incompletely observed. Algorithms that can accurately predict which links are missing can dramatically speed up network data collection and improve network model validation. Many algorithms now exist for predicting missing links, given a partially observed network, but it has remained unknown whether a single best predictor exists, how link predictability varies across methods and networks from different domains, and how close to optimality current methods are. We answer these questions by systematically evaluating 203 individual link predictor algorithms, representing three popular families of methods, applied to a large corpus of 550 structurally diverse networks from six scientific domains. We first show that individual algorithms exhibit a broad diversity of prediction errors, such that no one predictor or family is best, or worst, across all realistic inputs. We then exploit this diversity using network-based metalearning to construct a series of “stacked” models that combine predictors into a single algorithm. Applied to a broad range of synthetic networks, for which we may analytically calculate optimal performance, these stacked models achieve optimal or nearly optimal levels of accuracy. Applied to real-world networks, stacked models are superior, but their accuracy varies strongly by domain, suggesting that link prediction may be fundamentally easier in social networks than in biological or technological networks. These results indicate that the state of the art for link prediction comes from combining individual algorithms, which can achieve nearly optimal predictions. We close with a brief discussion of limitations and opportunities for further improvements.


Author(s):  
Alexey Ignatiev ◽  
Antonio Morgado ◽  
Joao Marques-Silva

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.


Symmetry ◽  
2022 ◽  
Vol 14 (1) ◽  
pp. 116
Author(s):  
Junhua Ku ◽  
Fei Ming ◽  
Wenyin Gong

In the real-world, symmetry or asymmetry widely exists in various problems. Some of them can be formulated as constrained multi-objective optimization problems (CMOPs). During the past few years, handling CMOPs by evolutionary algorithms has become more popular. Lots of constrained multi-objective optimization evolutionary algorithms (CMOEAs) have been proposed. Whereas different CMOEAs may be more suitable for different CMOPs, it is difficult to choose the best one for a CMOP at hand. In this paper, we propose an ensemble framework of CMOEAs that aims to achieve better versatility on handling diverse CMOPs. In the proposed framework, the hypervolume indicator is used to evaluate the performance of CMOEAs, and a decreasing mechanism is devised to delete the poorly performed CMOEAs and to gradually determine the most suitable CMOEA. A new CMOEA, namely ECMOEA, is developed based on the framework and three state-of-the-art CMOEAs. Experimental results on five benchmarks with totally 52 instances demonstrate the effectiveness of our approach. In addition, the superiority of ECMOEA is verified through comparisons to seven state-of-the-art CMOEAs. Moreover, the effectiveness of ECMOEA on the real-world problems is also evaluated for eight instances.


Author(s):  
Marijn J.H. Heule

Satisfiability (SAT) solvers have become complex tools, which raises the question of whether we can trust their results. This question is particularly important when the solvers are used to determine the correctness of hardware and software and when they are used to produce mathematical results. To deal with this issue, solvers can provide proofs of unsatisfiability to certify the correctness of their answers. This chapter presents the history and state-of-the-art of producing and validating proofs of unsatisfiability. The chapter covers the most popular proof formats with and without hints to speed up certification. Hints in proofs make validation easy, which resulted in several efficient formally-verified checkers. Various proof systems are discussed, ranging from resolution to the recent propagation redundancy system. The chapter also describes techniques to compress and optimize proofs.


Author(s):  
Fahiem Bacchus ◽  
Matti Järvisalo ◽  
Ruben Martins

Maximum satisfiability (MaxSAT) is an optimization version of SAT that is solved by finding an optimal truth assignment instead of just a satisfying one. In MaxSAT the objective function to be optimized is specified by a set of weighted soft clauses: the objective value of a truth assignment is the sum of the weights of the soft clauses it satisfies. In addition, the MaxSAT problem can have hard clauses that the truth assignment must satisfy. Many optimization problems can be naturally encoded into MaxSAT and this, along with significant performance improvements in MaxSAT solvers, has led to MaxSAT being used in a number of different application areas. This chapter provides a detailed overview of the approaches to MaxSAT solving that have in recent years been most successful in solving real-world optimization problems. Further recent developments in MaxSAT research are also overviewed, including encodings, applications, preprocessing, incomplete solving, algorithm portfolios, partitioning-based solving, and parallel solving.


2009 ◽  
Vol 36 ◽  
pp. 229-266 ◽  
Author(s):  
H.L. Chieu ◽  
W.S. Lee

The survey propagation (SP) algorithm has been shown to work well on large instances of the random 3-SAT problem near its phase transition. It was shown that SP estimates marginals over covers that represent clusters of solutions. The SP-y algorithm generalizes SP to work on the maximum satisfiability (Max-SAT) problem, but the cover interpretation of SP does not generalize to SP-y. In this paper, we formulate the relaxed survey propagation (RSP) algorithm, which extends the SP algorithm to apply to the weighted Max-SAT problem. We show that RSP has an interpretation of estimating marginals over covers violating a set of clauses with minimal weight. This naturally generalizes the cover interpretation of SP. Empirically, we show that RSP outperforms SP-y and other state-of-the-art Max-SAT solvers on random Max-SAT instances. RSP also outperforms state-of-the-art weighted Max-SAT solvers on random weighted Max-SAT instances.


Sign in / Sign up

Export Citation Format

Share Document