Resolution for Max-SAT

DOI10.1016/j.artint.2007.03.001zbMath1168.68541OpenAlexW2154352023WikidataQ60512184 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

completenessresolutionsatisfiabilitysaturationMax-SATweighted Max-SAT

Mathematics Subject Classification ID

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

Related Items

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

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