Resolution for Max-SAT

DOI10.1016/j.artint.2007.03.001zbMath1168.68541WikidataQ60512184 ScholiaQ60512184MaRDI QIDQ1028942

Jordi Levy, Felip Manyà, Maria Luisa Bonet

Publication date: 9 July 2009

Published in: Artificial Intelligence (Search for Journal in Brave)

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

zbMATH Keywords

completeness; resolution; satisfiability; saturation; Max-SAT; weighted Max-SAT

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

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

Related Items

Breaking Cycle Structure to Improve Lower Bound for Max-SAT, ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver, Applications and Computational Advances for Solving the QUBO Model, Boosting branch-and-bound MaxSAT solvers with clause learning, Proofs and Certificates for Max-SAT, MaxSAT Resolution and Subcube Sums, MaxSAT resolution for regular propositional logic, A framework for reasoning under uncertainty based on non-deterministic distance semantics, Simplified forms of computerized reasoning with distance semantics, Resolution-based lower bounds in MaxSAT, WPM3: an (in)complete algorithm for weighted partial MaxSAT, Incomplete inference for graph problems, Understanding the power of Max-SAT resolution through up-resilience, An improved algorithm for the \((n, 3)\)-MaxSAT problem: asking branchings to satisfy the clauses, Cable tree wiring -- benchmarking solvers on a real-world scheduling problem with a variety of precedence constraints, A proof builder for Max-SAT, Propositional proof systems based on maximum satisfiability, Iterative and core-guided maxsat solving: a survey and assessment, Resolution and linear CNF formulas: improved \((n,3)\)-\textsc{MaxSAT} algorithms, QMaxSATpb: a certified MaxSAT solver, Improved MaxSAT Algorithms for Instances of Degree 3, A Max-SAT Inference-Based Pre-processing for Max-Clique, Exploiting Cycle Structures in Max-SAT, Algorithms for Weighted Boolean Optimization

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
• On the automatizability of resolution and related propositional proof systems
• Mutilated chessboard problem is exponentially hard for resolution
• MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
• Bucket elimination for multiobjective optimization problems
• The Approximability of Constraint Satisfaction Problems
• The Efficiency of Resolution and Davis--Putnam Procedures
• Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers
• Local Consistency in Weighted CSPs and Inference in Max-SAT
• Resolution lower bounds for the weak pigeonhole principle
• Hard examples for resolution
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Short proofs are narrow—resolution made simple
• New Upper Bounds for Maximum Satisfiability
• Exact Algorithms for MAX-SAT
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• A Complete Calculus for Max-SAT
• Principles and Practice of Constraint Programming – CP 2004