Nested satisfiability (Q582905): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 01:41, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Nested satisfiability |
scientific article |
Statements
Nested satisfiability (English)
0 references
1990
0 references
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.)
0 references
satisfiability problem
0 references
bipartite graph
0 references