Nested satisfiability

DOI10.1007/BF02983372MaRDI QIDQ582905zbMATH OpenOpenAlexFDO

Authors Donald E. Knuth

Publication date 1990

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/cs/9301111

zbMATH Keywords

bipartite graphsatisfiability problem

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Abstract: A special case of the satisfiability problem, in which the clauses have a hierarchical structure, is shown to be solvable in linear time, assuming that the clauses have been represented in a convenient way.

Review text

A special case of the satisfiability problem is shown to be solvable in linear time. This special case is essentially one-sided planar satisfiability: It is means that the bipartite graph whose vertices are variables and clauses, and whose edges run from variables to the clauses containing the variables, can be represented in the plane without crossing edges, with all variables appearing in a straight line, and with all clauses on one side of that line. The linear-time algorithm assumes that such a representation has been given, and decides whether or not the clauses are satisfiable by dynamically replacing clauses by simpler clauses containing only two literals. (The running time needed to decide whether or not a given set of clauses has such a nested structure is not considered.)

Recommendations

• scientific article; zbMATH DE number 152108
• Solving satisfiability in less than \(2^ n\) steps
• Polynomially solvable satisfiability problems
• Satisfiability of co-nested formulas
• A simplified NP-complete satisfiability problem

Cites work

• Planar Formulae and Their Uses

Cited in

(16)

• Satisfiability of co-nested formulas
• On exact selection of minimally unsatisfiable subformulae
• Solving the resolution-free SAT problem by submodel propagation in linear time
• Selecting and covering colored points
• New tractable classes for default reasoning from conditional knowledge bases
• Nested structure in parameterized rough reduction
• Backdoors to satisfaction
• Recognition of Nested Gates in CNF Formulas
• A CNF Class Generalizing Exact Linear Formulas
• On Some Aspects of Mixed Horn Formulas
• On satisfiability problems with a linear structure
• Planar 3-SAT with a clause/variable cycle
• Nested Pebbles and Transitive Closure
• The complexity of the falsifiability problem for pure implicational formulas
• Optimization and probabilistic satisfiability on nested and co-nested formulas
• Satisfiability of mixed Horn formulas

This page was built for publication: Nested satisfiability

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