Resolution cannot polynomially simulate compressed-BFS

DOI10.1007/s10472-004-8427-2zbMath1099.68102OpenAlexW2142612879MaRDI QIDQ1776193

Igor L. Markov, DoRon B. Motter, Jarrod A. Roy

Publication date: 20 May 2005

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-004-8427-2

zbMATH Keywords

Boolean satisfiability

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (2)

The Complexity of Propositional Proofs ⋮ \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver

Uses Software

• Chaff
• ZRes

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The intractability of resolution
• Resolution and binary decision diagrams cannot simulate each other polynomially
• Investigations on autark assignments
• Two-level logic minimization: an overview
• GRASP: a search algorithm for propositional satisfiability
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• An experimental study of a compressed index

This page was built for publication: Resolution cannot polynomially simulate compressed-BFS