Are hitting formulas hard for resolution?

DOI10.1016/j.dam.2023.05.003arXiv2206.15225MaRDI QIDQ6162037

Stefan Szeider, Tomáš Peitl

Publication date: 15 June 2023

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

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

zbMATH Keywords

symmetry breaking; resolution; satisfiability; SAT; hitting formulas

Mathematics Subject Classification ID

68Txx: Artificial intelligence

68Qxx: Theory of computing

03Bxx: General logic

Related Items

Irreducible subcube partitions

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Satisfiability of acyclic and almost acyclic CNF formulas
• On Davis-Putnam reductions for minimally unsatisfiable clause-sets
• On the power of clause-learning SAT solvers as resolution engines
• The intractability of resolution
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• On the structure of some classes of minimal unsatisfiable formulas
• The complexity of read-once resolution
• On subclasses of minimal unsatisfiable formulas
• New width parameters for SAT and \#SAT
• Practical graph isomorphism. II.
• Solving \#SAT using vertex covers
• On the hardness of approximate reasoning
• Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency
• Hard examples for resolution
• CNF-Satisfiability Test by Counting and Polynomial Average Time
• Green-Tao Numbers and SAT
• Finding the Hardest Formulas for Resolution
• Theory and Applications of Satisfiability Testing
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution