The complexity of the satisfiability problem for Krom formulas
type: Item
instance of: scholarly article
title: The complexity of the satisfiability problem for Krom formulas
zbMATH Open document ID: 0552.03023
DOI: 10.1016/0304-3975(84)90138-5
author: Larry Denenberg
author: Harry R. Lewis
published in: Theoretical Computer Science
publication date: 1984-01-01T00:00:00Z
review text: A Krom formula is a formula of pure quantificational theory whose matrix is in conjunctive normal form with at most two disjuncts in each conjunct. The authors study the computational complexity of the satisfiability problem for Krom formulas. Their results are as follows: (1) Satisfiability is decidable in polynomial time for Krom formulas with prefix \(\forall \exists \forall\). Moreover, the unsatisfiable Krom formulas with prefix \(\forall \exists \forall\) form a class complete for nondeterministic log space. (2) Satisfiability for Krom formulas with prefix \(\exists^*\forall^*\exists^*\) is a complete problem for deterministic exponential time. But for each fixed k, satisfiability for Krom formulas with prefix \(\exists^*\forall^ k\exists^*\) is decidable in polynomial time. (3) Satisfiability for Krom formulas with prefix \(\exists^*\forall^*\) is a complete problem for polynomial space. (4) Satisfiability for monadic Krom formulas is complete for P.
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 3878907
zbMATH Keywords: Krom formula
zbMATH Keywords: satisfiability problem
reviewed by: M.Tetruashvili
describes a project that uses: ALGOL 60
MaRDI profile type: Publication
full work available at URL: 0304-3975(84)90138-5
OpenAlex ID: W2007102962
cites work: Q5639707
cites work: Prefix classes of Krom formulas
cites work: A linear-time algorithm for testing the truth of certain quantified Boolean formulas
cites work: Alternation
cites work: Q4138187
cites work: Q3905252
cites work: Bounded Algol-Like Languages
cites work: New problems complete for nondeterministic log space
cites work: Complete problems for deterministic polynomial time
cites work: Resolution Strategies as Decision Procedures
cites work: ENTSCHEIDUNGSPROBLEM REDUCED TO THE AEA CASE
cites work: On the sequential nature of unification
cites work: Q3856727
cites work: Complexity results for classes of quantificational formulas
cites work: Q3915990
cites work: Q5523671
cites work: On the complexity of integer programming
cites work: Q3888985
description: scientific article; zbMATH DE number 3878907