Finding the Hardest Formulas for Resolution

DOI10.1613/jair.1.12589OpenAlexW3203169850WikidataQ113739705 ScholiaQ113739705MaRDI QIDQ5154766

Stefan Szeider, Tomáš Peitl

Publication date: 5 October 2021

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

Full work available at URL: https://doi.org/10.1613/jair.1.12589

zbMATH Keywords

automated reasoningsatisfiabilitymathematical foundations

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Related Items (1)

Are hitting formulas hard for resolution?

Uses Software

• nauty
• MiniZinc
• SciPy
• Traces
• PySAT

Cites Work

• Unnamed Item
• On Davis-Putnam reductions for minimally unsatisfiable clause-sets
• The intractability of resolution
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• On reducibility and symmetry of disjoint NP pairs.
• PySAT: a Python toolkit for prototyping with SAT oracles
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• On subclasses of minimal unsatisfiable formulas
• Investigations on autark assignments
• On the automatizability of resolution and related propositional proof systems
• Constraints for symmetry breaking in graph representation
• Practical graph isomorphism. II.
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
• The Complexity of Propositional Proofs
• On Non-Computable Functions
• Computing Optimal Hypertree Decompositions
• A Computing Procedure for Quantification Theory
• Local Search for Unsatisfiability

This page was built for publication: Finding the Hardest Formulas for Resolution