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 Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem

2009 ◽  
Vol 36 ◽  
pp. 229-266 ◽  
Author(s):  
H.L. Chieu ◽  
W.S. Lee
Keyword(s):  
Phase Transition ◽  
State Of The Art ◽  
Satisfiability Problem ◽  
Maximum Satisfiability ◽  
Sat Problem ◽  
Sat Solvers ◽  
Minimal Weight ◽  
Survey Propagation ◽  
Max Sat

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.

scholarly journals Memory-Adjustable Navigation Piles with Applications to Sorting and Convex Hulls

2021 ◽  
Vol 17 (2) ◽  
pp. 1-19
Author(s):  
Omar Darwish ◽  
Amr Elmasry ◽  
Jyrki Katajainen
Keyword(s):  
Data Structure ◽  
Lower Bound ◽  
Convex Hull ◽  
Euclidean Plane ◽  
State Of The Art ◽  
Random Access ◽  
Priority Queue ◽  
Convex Hulls ◽  
Limited Capacity ◽  
Range Of Values

We consider space-bounded computations on a random-access machine, where the input is given on a read-only random-access medium, the output is to be produced to a write-only sequential-access medium, and the available workspace allows random reads and writes but is of limited capacity. The length of the input is N elements, the length of the output is limited by the computation, and the capacity of the workspace is O ( S ) bits for some predetermined parameter S ≥ lg N . We present a state-of-the-art priority queue—called an adjustable navigation pile —for this restricted model. This priority queue supports M inimum in O (1) time, C onstruct in O ( N ) time, and E xtract - min in O ( N / S + lg S ) time for any S ≥ lg N . The priority queue can be further augmented in O ( N ) time to deal with a batch of at most S elements in a specified range of values at a time, and allow to I nsert (activate) or E xtract (deactivate) an element among these elements, such that I nsert and E xtract take O ( N / S + lg S ) time for any S ≥ lg N . We show how to use our data structure to sort N elements and to compute the convex hull of N points in the Euclidean plane in O ( N 2 / S + N lg S ) time for any S ≥ lg N . Following a known lower bound for the space-time product of any branching program for finding unique elements, both our sorting and convex-hull algorithms are optimal. The adjustable navigation pile has turned out to be useful when designing other space-efficient algorithms, and we expect that it will find its way to yet other applications.

scholarly journals A partition-based branch-and-bound algorithm for the project duration problem with partially renewable resources and general temporal constraints

OR Spectrum ◽  
2021 ◽  
Author(s):  
Kai Watermeyer ◽  
Jürgen Zimmermann
Keyword(s):  
Exact Solution ◽  
Branch And Bound ◽  
Renewable Resources ◽  
State Of The Art ◽  
Branch And Bound Algorithm ◽  
Time Lags ◽  
Temporal Constraints ◽  
New Approach ◽  
Project Duration ◽  
Partially Renewable Resources

AbstractThe concept of partially renewable resources provides a general modeling framework that can be used for a wide range of different real-life applications. In this paper, we consider a resource-constrained project duration problem with partially renewable resources, where the temporal constraints between the activities are given by minimum and maximum time lags. We present a new branch-and-bound algorithm for this problem, which is based on a stepwise decomposition of the possible resource consumptions by the activities of the project. It is shown that the new approach results in a polynomially bounded depth of the enumeration tree, which is obtained by kind of a binary search. In a comprehensive experimental performance analysis, we compare our exact solution procedure with all branch-and-bound algorithms and state-of-the-art heuristics from the literature on different benchmark sets. The results of the performance study reveal that our branch-and-bound algorithm clearly outperforms all exact solution procedures. Furthermore, it is shown that our new approach dominates the state-of-the-art heuristics on well known benchmark instances.

scholarly journals Two flavors of DRAT

10.29007/lt8r ◽  
2019 ◽  
Author(s):  
Adrian Rebola Pardo ◽  
Armin Biere
Keyword(s):  
State Of The Art ◽  
Operational Definition ◽  
Design Decisions ◽  
Sat Solvers ◽  
Original Definition ◽  
Definition Of ◽  
Unit Propagation ◽  
Practical Implications

DRAT proofs have become the de facto standard for certifying SAT solvers’ results. State-of-the-art DRAT checkers are able to efficiently establish the unsatisfiability of a formula. However, DRAT checking requires unit propagation, and so it is computationally non-trivial. Due to design decisions in the development of early DRAT checkers, the class of proofs accepted by state-of-the-art DRAT checkers differs from the class of proofs accepted by the original definition. In this paper, we formalize the operational definition of DRAT proofs, and discuss practical implications of this difference for generating as well as checking DRAT proofs. We also show that these theoretical differences have the potential to affect whether some proofs generated in practice by SAT solvers are correct or not.

An efficient data structure for branch-and-bound algorithm

2004 ◽  
Vol 167 (1-4) ◽  
pp. 233-237
Author(s):  
Wu Jigang ◽  
Thambipillai Srikanthan
Keyword(s):  
Data Structure ◽  
Branch And Bound ◽  
Branch And Bound Algorithm ◽  
Efficient Data
Sign in / Sign up

Export Citation Format

Share Document