Resolution for Max-SAT
From MaRDI portal
Publication:1028942
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
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