Finding the hardest formulas for resolution

DOI10.1613/JAIR.1.12589MaRDI QIDQ5154766zbMATH OpenOpenAlexWikidataFDO

Authors Tomáš Peitl, Stefan Szeider

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 reasoningmathematical foundationssatisfiability

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• Long proofs of (seemingly) simple formulas
• Resolution remains hard under equivalence
• Many hard examples for resolution
• scientific article; zbMATH DE number 1361489
• scientific article; zbMATH DE number 176731

Cites work

• A Computing Procedure for Quantification Theory
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Computing Optimal Hypertree Decompositions
• Constraints for symmetry breaking in graph representation
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Investigations on autark assignments
• Local Search for Unsatisfiability
• Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas
• Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
• On non-computable functions
• On reducibility and symmetry of disjoint NP pairs.
• On subclasses of minimal unsatisfiable formulas
• On the automatizability of resolution and related propositional proof systems
• Practical graph isomorphism. II.
• PySAT: a Python toolkit for prototyping with SAT oracles
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• The Complexity of Propositional Proofs
• The intractability of resolution
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints

Cited in

(4)

• Resolution remains hard under equivalence
• Long proofs of (seemingly) simple formulas
• Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs
• Are hitting formulas hard for resolution?

Describes a project that uses

Uses Software

• SciPy
• Traces
• MiniZinc
• nauty
• PySAT

This page was built for publication: Finding the hardest formulas for resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5154766)