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

scholarly journals A Verified SAT Solver Framework including Optimization and Partial Valuations

10.29007/96wb ◽  
2020 ◽  
Author(s):  
Mathias Fleury ◽  
Christoph Weidenbach
Keyword(s):  
Branch And Bound ◽  
Proof Assistant ◽  
Minimal Cost ◽  
Minimal Models ◽  
Total Cost ◽  
Formal Framework ◽  
Clause Learning ◽  
Sat Solver ◽  
Max Sat

Based on our formal framework for CDCL (conflict-driven clause learning) using the proof assistant Isabelle/HOL, we verify an extension of CDCL computing cost-minimal models called OCDCL. It is based on branch and bound and computes models of minimal cost with respect to total valuations. The verification starts by developing a framework for CDCL with branch and bound, called CDCLBnB, which is then instantiated to get OCDCL. We then apply our formalization to three different applications. Firstly, through the dual rail encoding, we reduce the search for cost-optimal models with respect to partial valuations to searching for total cost-optimal models, as derived by OCDCL. Secondly, we instantiate OCDCL to solve MAX-SAT, and, thirdly, CDCLBnB to compute a set of covering models. A large part of the original CDCL verification framework was reused without changes to reduce the complexity of the new formalization. To the best of our knowledge, this is the first rigorous formalization of CDCL with branch and bound and its application to an optimizing CDCL calculus, and the first solution that computes cost-optimal models with respect to partial valuations.

scholarly journals QMaxSAT: A Partial Max-SAT Solver

2012 ◽  
Vol 8 (1-2) ◽  
pp. 95-100 ◽  
Author(s):  
Miyuki Koshimura ◽  
Tong Zhang ◽  
Hiroshi Fujita ◽  
Ryuzo Hasegawa
Keyword(s):  
Sat Solver ◽  
Max Sat

scholarly journals MiniMaxSat: A New Weighted Max-SAT Solver

2007 ◽  
pp. 41-55 ◽  
Author(s):  
Federico Heras ◽  
Javier Larrosa ◽  
Albert Oliveras
Keyword(s):  
Sat Solver ◽  
Max Sat

scholarly journals MiniMaxSAT: An Efficient Weighted Max-SAT solver

2008 ◽  
Vol 31 ◽  
pp. 1-32 ◽  
Author(s):  
F. Heras ◽  
J. Larrosa ◽  
A. Oliveras
Keyword(s):  
Empirical Evaluation ◽  
Objective Functions ◽  
Lower Bounding ◽  
Sat Solver ◽  
Max Sat

In this paper we introduce MiniMaxSat, a new Max-SAT solver that is built on top of MiniSat+. It incorporates the best current SAT and Max-SAT techniques. It can handle hard clauses(clauses of mandatory satisfaction as in SAT), soft clauses (clauses whose falsification is penalized by a cost as in Max-SAT) as well as pseudo-boolean objective functions and constraints. Its main features are: learning and backjumping on hard clauses; resolution-based and substraction-based lower bounding; and lazy propagation with the two-watched literal scheme. Our empirical evaluation comparing a wide set of solving alternatives on a broad set of optimization benchmarks indicates that the performance of MiniMaxSat is usually close to the best specialized alternative and, in some cases, even better.

Authorization query method for RBAC based on partial MAX-SAT solver

2013 ◽  
Vol 33 (5) ◽  
pp. 1367-1370
Author(s):  
Wei SUN ◽  
Yanling LI ◽  
Jun LU
Keyword(s):  
Sat Solver ◽  
Max Sat

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.

Sign in / Sign up

Export Citation Format

Share Document