On Davis-Putnam reductions for minimally unsatisfiable clause-sets

DOI10.1016/j.tcs.2013.04.020zbMath1296.03010arXiv1202.2600OpenAlexW4246030944MaRDI QIDQ391124

Oliver Kullmann, Zhao, Xishun

Publication date: 10 January 2014

Published in: Theoretical Computer Science, Theory and Applications of Satisfiability Testing – SAT 2012 (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1202.2600

zbMATH Keywords

isomorphismconfluencevariable eliminationdeficiencyclause-sets (CNFs)Davis-Putnam reductionminimal unsatisfiabilitysingular DP-reductionsingular variables

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Related Items (4)

On Davis-Putnam reductions for minimally unsatisfiable clause-sets ⋮ Are hitting formulas hard for resolution? ⋮ Irreducible subcube partitions ⋮ Finding the Hardest Formulas for Resolution

Uses Software

• MiniSat
• JBool
• NiVER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On Davis-Putnam reductions for minimally unsatisfiable clause-sets
• Theory and applications of satisfiability testing -- SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19--22, 2011. Proceedings
• Resolution-based lower bounds in MaxSAT
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• On subclasses of minimal unsatisfiable formulas
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• Two tractable subclasses of minimal unsatisfiable formulas
• Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency
• On Variables with Few Occurrences in Conjunctive Normal Forms
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Elimination of Infrequent Variables Improves Average Case Performance of Satisfiability Algorithms
• Unit Refutations and Horn Sets
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

This page was built for publication: On Davis-Putnam reductions for minimally unsatisfiable clause-sets