The complexity of the satisfiability problem for Krom formulas

DOI10.1016/0304-3975(84)90138-5MaRDI QIDQ800915zbMATH OpenOpenAlexFDO

Authors Larry Denenberg, Harry R. Lewis

Publication date 1984

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(84)90138-5

zbMATH Keywords

Krom formulasatisfiability problem

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15)

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.

Recommendations

• The complexity of satisfiability problems
• Satisfiability of formulae with one \(\forall\) is decidable in exponential time
• Tractable and intractable classes of propositional schemata
• scientific article; zbMATH DE number 4085614
• The Complexity of Very Simple Boolean Formulas with Applications

Cites work

• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Alternation
• Bounded Algol-Like Languages
• Complete problems for deterministic polynomial time
• Complexity results for classes of quantificational formulas
• ENTSCHEIDUNGSPROBLEM REDUCED TO THE AEA CASE
• scientific article; zbMATH DE number 3657754 (Why is no real title available?)
• scientific article; zbMATH DE number 3695102 (Why is no real title available?)
• scientific article; zbMATH DE number 3715502 (Why is no real title available?)
• scientific article; zbMATH DE number 3727583 (Why is no real title available?)
• scientific article; zbMATH DE number 3566230 (Why is no real title available?)
• scientific article; zbMATH DE number 3236051 (Why is no real title available?)
• scientific article; zbMATH DE number 3366917 (Why is no real title available?)
• New problems complete for nondeterministic log space
• On the complexity of integer programming
• On the sequential nature of unification
• Prefix classes of Krom formulas
• Resolution Strategies as Decision Procedures

Cited in

(4)

• scientific article; zbMATH DE number 8117 (Why is no real title available?)
• scientific article; zbMATH DE number 6970794 (Why is no real title available?)
• Complexity of the satisfiability problem for multilinear forms over a finite field
• Satisfiability of formulae with one \(\forall\) is decidable in exponential time

Describes a project that uses

Uses Software

• ALGOL 60

This page was built for publication: The complexity of the satisfiability problem for Krom formulas

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