Skip to content

Planar SAT

A Boolean satisfiability restriction in which the bipartite incidence graph connecting variables to the clauses containing them is planar, while the decision question remains whether a satisfying truth assignment exists.

Version
v1 · 2026-09-28 · History
Domain-specific #
11338
Domain group
Applied Sciences & Engineering
Origin domain
Computer Science & Software Engineering
Subdomains
Computational Complexity, Satisfiability → Computer Science & Software Engineering
Aliases
Planar satisfiability, Planar 3-SAT, Planar 3SAT

Core Idea

Planar SAT keeps the usual satisfiability decision while restricting how variables participate in clauses. Its bipartite incidence graph has one side for variables, one for clauses, and an edge for each literal occurrence; that graph must admit a plane embedding.

The restriction matters because many target problems are inherently planar. Planar 3SAT remains hard enough to serve as a reduction source, but results attach to precise variants, including clause size, polarity treatment, embedding, and sometimes variable-cycle conditions.

Structural Signature

Sig role-phrases:

  • Boolean formula — Provides variables, literals, and clauses. It is logical input. Counterfactual: A planar graph without formula semantics is not an instance.
  • Variable vertices — Represent shared truth choices. It is incidence part. Counterfactual: Duplicating variables without consistency changes the formula.
  • Clause vertices — Represent disjunctive constraints. It is incidence part. Counterfactual: No clause semantics means no SAT decision.
  • Occurrence edges — Connect variables to clauses in which literals occur. It is graph relation. Counterfactual: An unrelated drawing cannot establish the promise.
  • Planar embedding — Shows the incidence graph can be drawn without crossings. It is structural promise. Counterfactual: A crossed sketch does not prove nonplanarity, but a nonplanar graph violates the class.
  • Truth assignment — Tests whether all constraints can be satisfied simultaneously. It is decision witness. Counterfactual: Planarity alone says nothing about satisfiability.

What It Is Not

  • A planar parse tree does not establish planar incidence.
  • A single drawing with crossings does not prove the graph is nonplanar.
  • Splitting one variable into unrelated copies changes the logical instance.
  • Planar SAT and Planar 3SAT should not be treated as identical without stating clause restrictions.
  • Closest near-miss. Planar 3SAT adds a three-literal clause restriction; Planar SAT is the broader incidence-planarity condition and variant names must not be interchanged silently.

Scope of Application

  • NP-hardness reductions. Seeds proofs for planar games, puzzles, and layouts.
  • Complexity classification. Studies hardness under incidence restrictions.
  • Graph algorithms. Uses planarity testing and embeddings as instance promises.
  • Gadget design. Preserves logical equivalence while respecting geometric constraints.

Clarity

Define the incidence graph explicitly, state clause-size and polarity conventions, and say whether an embedding is part of the input or merely promised to exist. In reductions, identify crossover or equality gadgets and prove both directions of satisfiability preservation.

Manages Complexity

The abstraction binds two structures that must remain synchronized: Boolean semantics and topological embeddability. A reduction can be logically correct but geometrically invalid, or planar but no longer equivalent, so both proof obligations are constitutive.

Abstract Reasoning

  1. Specify formula syntax and the exact Planar SAT variant.
  2. Construct the bipartite variable–clause incidence graph with literal polarity represented correctly.
  3. Test or provide a planar embedding without changing variable identity.
  4. Evaluate or reduce satisfiability under the original Boolean semantics.
  5. When using gadgets, prove both logical equivalence and preservation of the promised embedding.

Knowledge Transfer

Planar-SAT hardness transfers only through reductions that preserve satisfiability and the exact graph promise. A planar-looking circuit, formula parse tree, or drawing is not enough; incidence identity and any variant-specific ordering or embedding constraints must survive.

Examples

Canonical

A 3-CNF formula has variable and clause nodes connected for each occurrence; the resulting bipartite graph has a crossing-free embedding, and the question asks for an assignment satisfying all clauses.

Mapped back: logic → 3-CNF; graph → variable–clause incidence; promise → planar; decision → satisfiable.

Applied / In Practice

Drawing separate copies of a variable near each clause removes crossings visually but no longer represents one shared truth value unless explicit equality gadgets preserve equivalence.

Mapped back: drawing → crossing-free; variable identity → split; equivalence → not preserved; verdict → invalid shortcut.

Structural Tensions

T1 — Geometric Restriction versus Computational Hardness. Planarity removes arbitrary crossings yet still permits enough interaction to retain NP-completeness.

Diagnostic: Which exact planar variant has the claimed hardness result?

T2 — Diagram versus Graph Property. A particular drawing may contain crossings although the underlying graph is planar.

Diagnostic: Has planarity been tested as an embedding property rather than by inspection?

Structural–Framed Character

Planar SAT is structural as satisfiability under a planar incidence promise and framed by computational complexity. Planarity qualifies the variable–clause relation, not the visual syntax or truth-assignment rule.

Structural Core vs. Domain Accent

The general core is decision under a graph-structural restriction. Complexity theory supplies NP membership, reductions, gadgets, and hardness; propositional logic supplies variables and clauses; planar graph theory supplies the embedding constraint.

This entry is a kind of Constraint satisfaction.

  • Approved unparented root. No reviewed parent entails Boolean satisfiability paired with planar variable–clause incidence.

  • Related — 3SAT and planarity. Each supplies one half of the identity, but neither alone captures the restricted decision problem.

Relationships to Other Abstractions

Local relationship map for Planar SATParents appear above the current abstraction, mutual partners to the right, and children below. Node labels state whether each abstraction is prime or domain-specific; colors identify relation types.Planar SATDOMAINDomain-specific abstraction: Constraint satisfaction — is a kind ofConstraintsatisfactionDOMAIN

Current abstraction Planar SAT Domain-specific

Parents (1) — more general patterns this builds on

  • Planar SAT is a kind of Constraint satisfaction Domain-specific

    Planar SAT is Constraint Satisfaction whose Boolean variable–clause incidence graph must be planar.

Hierarchy path (1) — routes to 1 parentless root

Neighborhood in Abstraction Space

Planar SAT sits in a moderately populated region (41st percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.

Family — Logical Connectives & Formal Systems (13 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-10-08

Not to Be Confused With

  • 3SAT. Tell: Restricts clause size but permits nonplanar incidence.
  • Planar graph coloring. Tell: Uses graph-color constraints rather than Boolean clauses.
  • Formula syntax tree. Tell: Represents parsing and is not the variable–clause incidence graph.
  • Circuit SAT. Tell: Uses gates and wires with different structural variants.

References

  • Frozen Wikipedia discovery revision: https://en.wikipedia.org/wiki/Planar_SAT (revision 1351698472).
  • Preserved source candidate: https://epubs.siam.org/doi/10.1137/0211025
  • Preserved source candidate: https://www.youtube.com/watch?v=KU8I8LjnQgE
  • Preserved source candidate: https://doi.org/10.1145/1346330.1346336
  • Preserved source candidate: https://www.cs.unm.edu/~moret/nae3sat.ps
  • Preserved source candidate: https://www.youtube.com/watch?v=ziViLYrf1Ak
  • Preserved source candidate: https://pdfs.semanticscholar.org/4855/b7160c651c8cc883def72348463fd77cdbed.pdf
  • Preserved source candidate: https://web.archive.org/web/20200211223237/https://pdfs.semanticscholar.org/4855/b7160c651c8cc883def72348463fd77cdbed.pdf
  • Preserved source candidate: https://dspace.mit.edu/bitstream/1721.1/99994/1/Demaine_Computational%20complexity.pdf

The frozen Wikipedia revision is discovery provenance. The retained source set was reviewed for identity, formal or operational relation, and scope. The encyclopedia's structural synthesis is bounded to those claims; a thin authority surface is recorded as a nonblocking source-strengthening repair rather than concealed.