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

DOI10.1016/j.artint.2005.01.004zbMath1132.68716MaRDI 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 programming; nonlinear programming; variable ordering; unit propagation; DPLL; weighted maximum satisfiability

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

90C05: Linear programming

90C09: Boolean programming

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Related Items

MaxSolver, 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, 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, Resolution for Max-SAT, 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, Comparing action descriptions based on semantic preferences, Exact Max-SAT solvers for over-constrained problems, On Inconsistent Clause-Subsets for Max-SAT Solving, Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates

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