An average case analysis of a resolution principle algorithm in mechanical theorem proving.

DOI10.1007/BF01531030zbMath1034.68542OpenAlexW2009941418MaRDI QIDQ1353997

O. Diekmann

Publication date: 13 May 1997

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

Full work available at URL: https://doi.org/10.1007/bf01531030

zbMATH Keywords

satisfiability problem

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35)

Related Items (2)

The \(Multi\)-SAT algorithm ⋮ Solving the satisfiability problem by using randomized approach

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Average time analyses of simplified Davis-Putnam procedures
• The intractability of resolution
• Polynomial-average-time satisfiability problems
• Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• On the complexity of regular resolution and the Davis-Putnam procedure
• An Analysis of Backtracking with Search Rearrangement
• Many hard examples for resolution
• The Pure Literal Rule and Polynomial Average Time
• Probabilistic Analysis of Two Heuristics for the 3-Satisfiability Problem
• Hard examples for resolution
• CNF-Satisfiability Test by Counting and Polynomial Average Time
• Exponential Average Time for the Pure Literal Rule
• Theorem-Proving on the Computer
• Backtrack programming techniques
• Average Performance of Heuristics for Satisfiability
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The complexity of theorem-proving procedures

This page was built for publication: An average case analysis of a resolution principle algorithm in mechanical theorem proving.