[Model] Planar3Satisfiability

[isPANN]

Motivation

PLANAR 3-SATISFIABILITY from Garey & Johnson (implicit in ND48 reference chain). A restricted variant of 3-SAT where the variable-clause incidence graph is planar. Despite this restriction, the problem remains NP-complete (Lichtenstein, 1982). It is a key intermediate problem for proving NP-completeness of geometric and planar graph problems.

Associated rules:

• R68: PLANAR 3SAT -> GEOMETRIC CONNECTED DOMINATING SET (establishes NP-completeness of geometric CDS)
• Widely used as starting point for geometric NP-hardness proofs (e.g., rectilinear covering, art gallery problems, geometric intersection graphs)

Definition

Name: Planar3Satisfiability

Canonical name: Planar 3-Satisfiability; also: Planar 3-SAT, Planar 3SAT, P3SAT
Reference: Lichtenstein, D. (1982). "Planar Formulae and Their Uses." SIAM Journal on Computing, 11(2), pp. 329-343.

Mathematical definition:

INSTANCE: A 3-CNF Boolean formula F = C_1 AND C_2 AND ... AND C_m over variables x_1, ..., x_n, where each clause C_j contains exactly 3 literals, and the variable-clause incidence graph H(F) is planar. The incidence graph H(F) = (V_x UNION V_C, E) is the bipartite graph with one node per variable (V_x), one node per clause (V_C), and an edge between variable x_i and clause C_j if and only if x_i or NOT(x_i) appears in C_j.
QUESTION: Is there a truth assignment to x_1, ..., x_n that satisfies F (i.e., makes every clause true)?

This is a feasibility (decision) problem: the answer is yes or no.

Variables

• Count: n = number of Boolean variables
• Per-variable domain: {0, 1} -- 0 = FALSE, 1 = TRUE
• Meaning: x_i in {0, 1} assigns a truth value to each variable. The formula is satisfied iff every clause contains at least one true literal under this assignment.

Schema (data type)

Type name: Planar3Satisfiability
Variants: none (operates on a fixed clause width K=3 with planarity constraint)

Field	Type	Description
num_variables	usize	Number of Boolean variables n
clauses	Vec<[Literal; 3]>	Each clause is an array of 3 literals (variable index + sign)

Notes:

• This is a feasibility (decision) problem: Value = Or (satisfiability-style).
• Structurally identical to KSatisfiability with K=3, but with an additional invariant: the variable-clause incidence graph must be planar. This invariant should be validated on construction.
• Key getter methods: num_variables(), num_clauses() (= clauses.len()).
• The Literal type encodes a variable index and its polarity (positive or negated).

Complexity

• Decision complexity: NP-complete. Proved by Lichtenstein (1982) via reduction from general 3-SAT. The key insight is that any 3-SAT formula can be transformed into an equivalent planar 3-SAT formula using crossover gadgets to eliminate edge crossings in the incidence graph.
• Best known exact algorithm: O*(1.307^n) by Scheder & Steinberger (2017), an improvement to the PPSZ algorithm. The same bound applies as for general 3-SAT; planarity does not yield a provably faster worst-case bound.
• Concrete complexity expression: "1.307^num_variables" (for declare_variants!)
• Special tractable cases: Planar NAE-3SAT (not-all-equal variant) is solvable in polynomial time (Moret, 1988). Planar 1-in-3-SAT remains NP-complete. Planar 3-SAT with all clauses on one side of a variable cycle is solvable in polynomial time via dynamic programming.
• ETH connection: Under the Exponential Time Hypothesis (ETH), Planar 3-SAT cannot be solved in 2^{o(√n)} time on planar instances with n variables and O(n) clauses, due to the planar separator theorem.
• References:
  • D. Lichtenstein (1982). "Planar Formulae and Their Uses." SIAM J. Comput. 11(2), pp. 329-343.
  • D. Scheder, J.P. Steinberger (2017). "PPSZ for General k-SAT — Making Hertli's Analysis Simpler and 3-SAT Faster." CCC 2017. Published in Computational Complexity 33, Article 3 (2024).

Specialization

• Special case of: 3-Satisfiability (KSatisfiability with K=3) -- the additional constraint is that the variable-clause incidence graph must be planar.
• Generalization of: Planar 3-SAT with variable cycle (a further restriction where variables form a cycle in the incidence graph embedding).
• Relationship to Satisfiability hierarchy: SAT -> 3-SAT -> Planar 3-SAT (each is a restriction of the previous, all NP-complete).

Extra Remark

Full book text (from ND48 reference chain):

Lichtenstein (1982) defines the set of planar Boolean formulae and shows that satisfiability of planar formulae is NP-complete. The Garey & Johnson entry ND48 (GEOMETRIC CONNECTED DOMINATING SET) references "[Lichtenstein, 1977]" for NP-completeness via "Transformation from PLANAR 3SAT", establishing Planar 3SAT as the source problem in the reduction chain.

The key property is that any 3-CNF formula can be made planar by introducing crossover gadgets. Each crossover gadget replaces an edge crossing in the incidence graph with a constant-size sub-formula that preserves satisfiability equivalence while maintaining planarity.

How to solve

• It can be solved by (existing) bruteforce. (Enumerate all 2^n truth assignments; check if each satisfies all clauses.)
• It can be solved by reducing to integer programming. (Same ILP formulation as 3-SAT: binary variable per Boolean variable, linear constraint per clause requiring at least one true literal. Companion rule issue to be filed separately.)
• Other: DPLL/CDCL solvers; PPSZ algorithm in O*(1.307^n).

Example Instance

Input:
n = 4 variables: x_0, x_1, x_2, x_3
m = 4 clauses:

• C_0 = (x_0 OR x_1 OR x_2)
• C_1 = (NOT x_0 OR x_1 OR x_3)
• C_2 = (NOT x_1 OR x_2 OR NOT x_3)
• C_3 = (x_0 OR NOT x_2 OR x_3)

Incidence graph planarity:
Each variable appears in exactly 3 clauses: x_0 ∈ {C_0,C_1,C_3}, x_1 ∈ {C_0,C_1,C_2}, x_2 ∈ {C_0,C_2,C_3}, x_3 ∈ {C_1,C_2,C_3}. The incidence graph has 8 vertices and 12 edges, exactly at the bipartite planarity bound (2v − 4 = 12). Exhaustive K_{3,3} subgraph search confirms no K_{3,3} exists, so the graph is planar.

Satisfying assignment: (x_0, x_1, x_2, x_3) = (1, 1, 0, 0):

• C_0: x_0 = T → TRUE ✓
• C_1: x_1 = T → TRUE ✓
• C_2: NOT x_1 = F, x_2 = F, NOT x_3 = T → TRUE ✓
• C_3: x_0 = T → TRUE ✓

Answer: YES — 8 out of 16 assignments satisfy all clauses.

Non-satisfying assignment: (x_0, x_1, x_2, x_3) = (0, 0, 0, 0):

• C_0 = (F OR F OR F) = FALSE ✗ — fails immediately.

Python validation script

# Positive example
count = 0
sat = []
for x0 in range(2):
    for x1 in range(2):
        for x2 in range(2):
            for x3 in range(2):
                c0 = x0 or x1 or x2
                c1 = (1-x0) or x1 or x3
                c2 = (1-x1) or x2 or (1-x3)
                c3 = x0 or (1-x2) or x3
                if c0 and c1 and c2 and c3:
                    count += 1
                    sat.append((x0,x1,x2,x3))
assert count == 8
assert (1,1,0,0) in sat
assert (0,0,0,0) not in sat
print(f"Positive: {count}/16 satisfying")

# Planarity: K_{3,3} subgraph check on incidence graph
from itertools import combinations
vc = {'x0':{'C0','C1','C3'}, 'x1':{'C0','C1','C2'},
      'x2':{'C0','C2','C3'}, 'x3':{'C1','C2','C3'}}
k33 = any(
    all(c in vc[v] for v in v3 for c in c3)
    for v3 in combinations(vc.keys(), 3)
    for c3 in combinations(['C0','C1','C2','C3'], 3)
)
assert not k33
print("Planarity: no K_{3,3} subgraph (planar)")

[isPANN]

Issue Quality Check — Model

Check	Result	Details
Usefulness	✅ Pass	Novel problem not yet in reduction graph; concrete planned reductions
Non-trivial	✅ Pass	Planarity invariant is a genuine structural constraint, not a simple variant
Correctness	⚠️ Warn	Complexity bound misquoted; Lichtenstein reference is correct
Well-written	❌ Fail	Missing ILP companion issue; example non-triviality argument is self-contradictory

Overall: 2 passed, 1 warning, 1 failed

---

Usefulness

Pass. Planar3Satisfiability does not exist in the codebase (pred show Planar3Satisfiability returns not found). The issue identifies a concrete planned reduction (R68: Planar 3SAT -> Geometric Connected Dominating Set) and notes the problem's role as a key intermediate for proving NP-completeness of geometric and planar graph problems. Motivation is substantive. Both brute-force and ILP solver paths are identified.

Non-trivial

Pass. While KSatisfiability<K3> already exists, it has no mechanism to express or enforce the planarity constraint on the variable-clause incidence graph. This is not a graph-type or weight-type variant that could be added as a parameter to the existing model. The planarity invariant requires a construction-time validation and fundamentally restricts the set of valid instances, making this a genuinely distinct problem.

Correctness

Warn. Two issues found:

1. Complexity bound misquoted. The issue claims the best known exact algorithm runs in O*(1.3303^n) citing Hertli (2014). This is incorrect on two counts:

   • Hertli (2014) proves a bound of O*(1.308^n) for general 3-SAT using the PPSZ algorithm, not 1.3303^n.
   • The figure 1.3303 appears to be confused with improvements to Schoning's randomized local search algorithm (which starts at (4/3)^n ≈ 1.3333^n).
   • Recommendation: Use O*(1.307^n) citing the improved PPSZ result from Scheder & Steinberger (CCC 2017 / Computational Complexity 2024), "PPSZ for General k-SAT — Making Hertli's Analysis Simpler and 3-SAT Faster," which supersedes Hertli (2014) for 3-SAT.

2. Lichtenstein (1982) reference is correct. The paper "Planar Formulae and Their Uses" exists in SIAM J. Comput. 11(2), pp. 329-343. However, note that the DOI is 10.1137/0211025 (volume 11, not a separate issue numbering). The claims about NP-completeness of planar satisfiability and the crossover gadget construction match the paper's content.

3. ETH connection is correct. The claim that Planar 3-SAT cannot be solved in 2^{o(sqrt(n))} time under ETH is well-established via the planar separator theorem.

Well-written

Fail. Several issues found:

4a. Missing ILP companion issue. The "How to solve" section checks the ILP box and states "Same ILP formulation as 3-SAT," but no [Rule] Planar3Satisfiability to ILP companion issue is linked. Per the template requirements, if direct ILP solving is claimed, a companion rule issue must be linked.

4d. Example quality — self-contradictory non-triviality argument. The "Non-trivial aspect" paragraph attempts to show that not all assignments work, but then the author discovers mid-sentence that the assignment x_0=T, x_1=F, x_2=F, x_3=T actually does satisfy all clauses, contradicting the intended argument. The paragraph concludes with the vague note "A more constrained instance would require careful variable-clause wiring." This undermines confidence in the example's suitability.

4d. Example planarity — not verified. The incidence graph has 8 vertices and 12 edges. For a bipartite planar graph, the edge bound is 2v - 4 = 12, so this is at the exact boundary. The issue claims planarity ("can be drawn without crossings by placing variables on a horizontal line and clauses above/below") but does not provide a concrete planar embedding. The planarity claim should be substantiated, especially since this is the defining feature of the problem.

4d. Example round-trip quality. The example has 2^4 = 16 configurations, and the self-contradictory analysis suggests many assignments satisfy the formula. For a feasibility problem, the example should have a meaningful mix of satisfying and non-satisfying configurations to test correctness. The current example may be too easily satisfiable.

4c. Complexity expression format. The Complexity section provides a complexity expression O*(1.3303^n) but the numeric value is wrong (see Correctness above). The corrected expression should be 1.307^num_variables using the getter method name.

Recommendations

• Fix the complexity bound to O*(1.307^n) citing Scheder & Steinberger (2017/2024), or O*(1.308^n) citing Hertli (2014) — not 1.3303^n.
• Create a companion [Rule] Planar3Satisfiability to ILP issue, or remove the ILP checkbox and note that ILP solving is inherited via the same formulation as 3-SAT (which already has an ILP path).
• Replace or fix the example's "non-trivial aspect" analysis. Provide a concrete non-satisfying assignment with verification, or choose a more constrained instance.
• Provide a planar embedding diagram or a more convincing planarity argument for the example instance.

[isPANN]

Fix-issue changelog

• Complexity: Fixed misquoted bound 1.3303^n → 1.307^n, citing Scheder & Steinberger (CCC 2017 / Computational Complexity 2024) instead of Hertli (2014). Added concrete expression "1.307^num_variables" for declare_variants!.
• Example: Removed self-contradictory "non-trivial aspect" paragraph (discovered mid-sentence that the claimed non-satisfying assignment actually satisfies all clauses). Replaced with clean satisfying (1,1,0,0) and non-satisfying (0,0,0,0) examples.
• Planarity verification: Added explicit K_{3,3} subgraph search confirming incidence graph is planar.
• ILP: Added companion rule note.
• Added Python validation script verifying satisfying/non-satisfying counts and planarity.

Applied by /fix-issue.