MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability

DOI10.1016/J.ARTINT.2005.01.004MaRDI QIDQ2457672zbMATH OpenOpenAlexFDO

Authors Zhao Xing, Weixiong Zhang

Publication date 23 October 2007

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.artint.2005.01.004

zbMATH Keywords

DPLLlinear programmingnonlinear programmingunit propagationvariable orderingweighted maximum satisfiability

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Linear programming (90C05) Boolean programming (90C09)

Recommendations

• Principles and Practice of Constraint Programming – CP 2004
• Minimaxsat: an efficient weighted Max-SAT solver
• New Upper Bounds for Maximum Satisfiability
• Resolution for Max-SAT
• A logical approach to efficient Max-SAT solving

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
• Algorithms for the maximum satisfiability problem
• An Empirical Study of MAX-2-SAT Phase Transitions
• Approximation algorithms for combinatorial problems
• Branch-and-cut solution of inference problems in propositional logic
• Branching rules for satisfiability
• Exact algorithms for MAX-SAT
• scientific article; zbMATH DE number 3571502 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1114003 (Why is no real title available?)
• scientific article; zbMATH DE number 2079360 (Why is no real title available?)
• scientific article; zbMATH DE number 2084703 (Why is no real title available?)
• scientific article; zbMATH DE number 3249560 (Why is no real title available?)
• scientific article; zbMATH DE number 3249566 (Why is no real title available?)
• scientific article; zbMATH DE number 3299758 (Why is no real title available?)
• scientific article; zbMATH DE number 956866 (Why is no real title available?)
• Input Proofs and Rank One Cutting Planes
• Integer optimization by local search. A domain-independent approach
• Linear Programming
• New Upper Bounds for Maximum Satisfiability
• On projected newton barrier methods for linear programming and an equivalence to Karmarkar’s projective method
• Principles and Practice of Constraint Programming – CP 2004
• Roof duality, complementation and persistency in quadratic 0–1 optimization
• Smoothed analysis of algorithms
• Solving Max-SAT as weighted CSP
• Some results and experiments in programming techniques for propositional logic
• The complexity of theorem-proving procedures

Cited in

(42)

• Resolution for Max-SAT
• A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
• MaxSolver
• Dynamic polynomial watchdog encoding for solving weighted MaxSAT
• The \textsc{MergeSat} solver
• Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability
• Core-boosted linear search for incomplete MaxSAT
• Iterative and core-guided maxsat solving: a survey and assessment
• A logical approach to efficient Max-SAT solving
• A framework for certified Boolean branch-and-bound optimization
• Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks
• A taxonomy of exact methods for partial Max-SAT
• Comparing action descriptions based on semantic preferences
• Exact Max-SAT solvers for over-constrained problems
• A new greedy randomised adaptive search procedure for solving the maximum satisfiability problem
• CHAMP: a multipass algorithm for Max Sat based on saver variables
• Efficient solution of MAX-SAT and SAT via higher order Boltzmann machines
• scientific article; zbMATH DE number 1629855 (Why is no real title available?)
• Semidefinite programming and constraint programming
• scientific article; zbMATH DE number 5996844 (Why is no real title available?)
• A Preprocessor for Max-SAT Solvers
• Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms
• On Inconsistent Clause-Subsets for Max-SAT Solving
• New inference rules for Max-SAT
• Minimaxsat: an efficient weighted Max-SAT solver
• Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates
• Algorithms for Weighted Boolean Optimization
• Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem
• \textsc{ahmaxsat}: description and evaluation of a branch and bound Max-SAT solver
• CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability
• Boosting branch-and-bound MaxSAT solvers with clause learning
• Exploiting the power of MIP solvers in MAXSAT
• Efficient branch-and-bound algorithms for weighted MAX-2-SAT
• A Spectral Method for MAX2SAT in the Planted Solution Model
• A framework for reasoning under uncertainty based on non-deterministic distance semantics
• Simplified forms of computerized reasoning with distance semantics
• Theory and Applications of Satisfiability Testing
• Principles and Practice of Constraint Programming – CP 2004
• Solving satisfiability problems with preferences
• A new bounding procedure and an improved exact algorithm for the Max-2-SAT problem
• Scatter search and genetic algorithms for MAX-SAT problems
• An efficient solver for weighted Max-SAT

Describes a project that uses

Uses Software

• PBS
• WSAT(OIP)
• Chaff

This page was built for publication: MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2457672)