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

DOI10.1016/j.artint.2005.01.004zbMath1132.68716OpenAlexW2029688740MaRDI QIDQ2457672

Weixiong Zhang, Zhao Xing

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

linear programmingnonlinear programmingvariable orderingunit propagationDPLLweighted maximum satisfiability

Mathematics Subject Classification ID

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

Related Items (19)

A logical approach to efficient Max-SAT solving ⋮ Solving satisfiability problems with preferences ⋮ Boosting branch-and-bound MaxSAT solvers with clause learning ⋮ A framework for certified Boolean branch-and-bound optimization ⋮ Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks ⋮ On Inconsistent Clause-Subsets for Max-SAT Solving ⋮ Scatter search and genetic algorithms for MAX-SAT problems ⋮ Comparing action descriptions based on semantic preferences ⋮ Efficient branch-and-bound algorithms for weighted MAX-2-SAT ⋮ A framework for reasoning under uncertainty based on non-deterministic distance semantics ⋮ Simplified forms of computerized reasoning with distance semantics ⋮ Exact Max-SAT solvers for over-constrained problems ⋮ Semidefinite Programming and Constraint Programming ⋮ A new bounding procedure and an improved exact algorithm for the Max-2-SAT problem ⋮ MaxSolver ⋮ Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates ⋮ Resolution for Max-SAT ⋮ ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver ⋮ Iterative and core-guided maxsat solving: a survey and assessment

Uses Software

• PBS
• WSAT(OIP)
• Chaff

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algorithms for the maximum satisfiability problem
• Some results and experiments in programming techniques for propositional logic
• Approximation algorithms for combinatorial problems
• A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
• Integer optimization by local search. A domain-independent approach
• Branch-and-cut solution of inference problems in propositional logic
• Branching rules for satisfiability
• On projected newton barrier methods for linear programming and an equivalence to Karmarkar’s projective method
• An Empirical Study of MAX-2-SAT Phase Transitions
• Smoothed analysis of algorithms
• Roof duality, complementation and persistency in quadratic 0–1 optimization
• Input Proofs and Rank One Cutting Planes
• Linear Programming
• New Upper Bounds for Maximum Satisfiability
• Exact Algorithms for MAX-SAT
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The complexity of theorem-proving procedures
• Principles and Practice of Constraint Programming – CP 2003
• Principles and Practice of Constraint Programming – CP 2004

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