Solving satisfiability in less than \(2^ n\) steps
type: Item
instance of: scholarly article
title: Solving satisfiability in less than \(2^ n\) steps
zbMATH Open document ID: 0603.68092
DOI: 10.1016/0166-218X(85)90050-2
published in: Discrete Applied Mathematics
publication date: 1985-01-01T00:00:00Z
review text: In this paper we describe and analyze an algorithm for solving the satisfiability problem. If E is a boolean formula in conjunctive normal form with n variables and r clauses, then we will show that this algorithm solves the satisfiability problem for formulas with at most k literals per clause in time \(O(| F| \cdot a^ n_ k)\), where \(a_ k\) is the greatest number satisfying \(a_ k=2-1/a_ k^{k-1}\) (in the case of 3-satisfiability \(a_ 3=1,6181)\).
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q25
zbMATH DE Number: 3974341
zbMATH Keywords: algorithm
zbMATH Keywords: boolean formula
zbMATH Keywords: conjunctive normal form
author: Burkhard Monien
author: Ewald Speckenmeyer
MaRDI profile type: Publication
cites work: Q4138187
cites work: Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
cites work: Average time analyses of simplified Davis-Putnam procedures
cites work: On Optimal Control and Identification of Processes Governed by Parabolic Differential Equations of Second Order
description: scientific article; zbMATH DE number 3974341