Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers

2005 ◽  
pp. 403-414 ◽  
Author(s):  
Chu Min Li ◽  
Felip Manyà ◽  
Jordi Planes
Keyword(s):  
Lower Bounds ◽  
Branch And Bound ◽  
Sat Solvers ◽  
Max Sat ◽  
Unit Propagation

scholarly journals Improved Exact Solver for the Weighted MAX-SAT Problem

10.29007/38lm ◽  
2018 ◽  
Author(s):  
Adrian Kuegel
Keyword(s):  
Data Structure ◽  
Lower Bound ◽  
Branch And Bound ◽  
State Of The Art ◽  
Branch And Bound Algorithm ◽  
Sat Problem ◽  
Sat Solvers ◽  
Propagation Algorithm ◽  
Max Sat ◽  
Unit Propagation

Many exact Max-SAT solvers use a branch and bound algorithm, where the lower bound is calculated with a combination of Max-SAT resolution and detection of disjoint inconsistent subformulas. We propose a propagation algorithm which improves the detection of disjoint inconsistent subformulas compared to algorithms previously used in Max-SAT solvers. We implemented this algorithm in our new solver akmaxsat and compared our solver with three solvers using unit propagation and restricted failed literal detection; these solvers are currently state-of-the-art on random Max-SAT instances. We also developed a lazy deletion data structure for our solver which speeds up lower bound calculation on instances with a high clauses-to-variables ratio. Our experiments show that our solver runs faster than the previously best solvers on randomly generated instances with a high clauses-to-variables ratio.

scholarly journals New Inference Rules for Max-SAT

2007 ◽  
Vol 30 ◽  
pp. 321-359 ◽  
Author(s):  
C. M. Li ◽  
F. Manya ◽  
J. Planes
Keyword(s):  
Experimental Investigation ◽  
Inference Rules ◽  
Sat Solvers ◽  
Sat Solver ◽  
Proof Tree ◽  
Max Sat ◽  
Unit Propagation ◽  
Unit Resolution ◽  
Original Formula ◽  
Simplified Formula

Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving the Max-SAT problem for the simplified formula is not equivalent to solving it for the original formula. In this paper, we define a number of original inference rules that, besides being applied efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution adapted to Max-SAT, are proved in a novel and simple way via an integer programming transformation. With the aim of finding out how powerful the inference rules are in practice, we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules, and performed an experimental investigation. The results provide empirical evidence that MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, Max-Cut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.

scholarly journals Branch and Bound Method to Solve Multi Objectives Function

2016 ◽  
Vol 12 (3) ◽  
pp. 5964-5974
Author(s):  
Tahani Jabbar Kahribt ◽  
Mohammed Kadhim Al- Zuwaini
Keyword(s):  
Lower Bounds ◽  
Branch And Bound ◽  
Single Machine ◽  
Upper Bound ◽  
Completion Time ◽  
Heuristic Method ◽  
Total Weighted Completion Time ◽  
Branch And Bound Method ◽  
Special Cases ◽  
Weighted Completion Time

This paper  presents  a  branch  and  bound  algorithm  for  sequencing  a  set  of  n independent  jobs  on  a single  machine  to  minimize sum of the discounted total weighted completion time and maximum lateness,  this problems is NP-hard. Two lower bounds were proposed and heuristic method to get an upper bound. Some special cases were  proved and some dominance rules were suggested and proved, the problem solved with up to 50 jobs.

scholarly journals A Two-Stage Assembly-Type Flowshop Scheduling Problem for Minimizing Total Tardiness

2016 ◽  
Vol 2016 ◽  
pp. 1-10 ◽  
Author(s):  
Ju-Yong Lee ◽  
June-Young Bang
Keyword(s):  
Lower Bounds ◽  
Branch And Bound ◽  
Total Tardiness ◽  
Scheduling Problem ◽  
Flowshop Scheduling ◽  
Two Stage ◽  
Algorithm Performance ◽  
Second Stage ◽  
Flowshop Scheduling Problem ◽  
Dominance Properties

This research considers a two-stage assembly-type flowshop scheduling problem with the objective of minimizing the total tardiness. The first stage consists of two independent machines, and the second stage consists of a single machine. Two types of components are fabricated in the first stage, and then they are assembled in the second stage. Dominance properties and lower bounds are developed, and a branch and bound algorithm is presented that uses these properties and lower bounds as well as an upper bound obtained from a heuristic algorithm. The algorithm performance is evaluated using a series of computational experiments on randomly generated instances and the results are reported.

Chapter 23. MaxSAT, Hard and Soft Constraints

2021 ◽  
Author(s):  
Chu Min Li ◽  
Felip Manyà
Keyword(s):  
Combinatorial Optimization ◽  
Lower Bounds ◽  
Branch And Bound ◽  
Data Structures ◽  
Optimization Problems ◽  
Soft Constraints ◽  
Inference Rules ◽  
Combinatorial Optimization Problems ◽  
Definition Of ◽  
Hard And Soft Constraints

MaxSAT solving is becoming a competitive generic approach for solving combinatorial optimization problems, partly due to the development of new solving techniques that have been recently incorporated into modern MaxSAT solvers, and to the challenge problems posed at the MaxSAT Evaluations. In this chapter we present the most relevant results on both approximate and exact MaxSAT solving, and survey in more detail the techniques that have proven to be useful in branch and bound MaxSAT and Weighted MaxSAT solvers. Among such techniques, we pay special attention to the definition of good quality lower bounds, powerful inference rules, clever variable selection heuristics and suitable data structures. Moreover, we discuss the advantages of dealing with hard and soft constraints in the Partial MaxSAT formalims, and present a summary of the MaxSAT Evaluations that have been organized so far as affiliated events of the International Conference on Theory and Applications of Satisfiability Testing.

scholarly journals ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver

2015 ◽  
Vol 9 (1) ◽  
pp. 89-128 ◽  
Author(s):  
André Abramé ◽  
Djamal Habet
Keyword(s):  
Branch And Bound ◽  
Sat Solver ◽  
Max Sat
Sign in / Sign up

Export Citation Format

Share Document