[Rule] GraphBandwidth to KSatisfiability

[QingyunQian]

Source: GraphBandwidth
Target: KSatisfiability (3-SAT)
Motivation: Enables solving the decision version of GraphBandwidth ("is bandwidth ≤ k?") using SAT solvers. Optimization via binary search on k with O(log n) SAT calls.
Reference:

• Prestwich, S. D. (2009). "CNF Encodings." In Handbook of Satisfiability, Chapter 2.

Reduction Algorithm

Notation:

• Source: GraphBandwidth instance with G = (V, E), n = |V|, m = |E|, bandwidth bound k
• Target: KSatisfiability<K3> instance

Variable mapping:

Boolean variables x_{i,p} for i ∈ V, p ∈ {0, ..., n−1}. x_{i,p} = true iff vertex i is at position p. Total: n² variables.
For implementation, a standard indexing is id(i,p) = i·n + p + 1 (1-based literal IDs in DIMACS CNF).

Constraint/objective transformation:

1. At-least-one (ALO): ∀i: (x_{i,0} ∨ x_{i,1} ∨ ... ∨ x_{i,n-1}) — each vertex gets a position
2. At-most-one (AMO): ∀i, p < q: (¬x_{i,p} ∨ ¬x_{i,q}) — each vertex at most one position
3. ALO columns: ∀p: (x_{0,p} ∨ x_{1,p} ∨ ... ∨ x_{n-1,p}) — each position occupied
4. AMO columns: ∀p, i < j: (¬x_{i,p} ∨ ¬x_{j,p}) — each position at most one vertex
5. Forbidden pairs: ∀(u,v) ∈ E, |p−q| > k: (¬x_{u,p} ∨ ¬x_{v,q})

ALO clauses (length n) are converted to 3-SAT via sequential encoding with auxiliary variables. AMO and forbidden-pair clauses are padded to length 3 by literal duplication, e.g. (A ∨ B) → (A ∨ B ∨ B). Final output is a KSatisfiability<K3> instance with all clauses of length exactly 3.

Note: keeping all four groups (ALO rows, AMO rows, ALO cols, AMO cols) is an intentional redundant modeling choice to strengthen unit propagation in CDCL SAT solvers.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_vars	n² + O(n²) auxiliary
num_clauses	O(n³ + m·n²) with pairwise AMO; O(n² + m·n²) with sequential AMO

Validation Method

• Cross-check with brute-force solver on small instances (n ≤ 8)
• Compare with ILP reduction results on the same instances
• Test both SAT (bandwidth ≤ k) and UNSAT (bandwidth > k) cases against known values

Example

Source: P₄ (path of 4 vertices), k = 1

Vertices: {0, 1, 2, 3}
Edges: {(0,1), (1,2), (2,3)}
Bandwidth bound: k = 1
Decision: is B*(P₄) ≤ 1?  (YES)

Target CNF (before 3-SAT conversion)

Variables: x_{i,p} for i,p ∈ {0..3}  (16 Boolean variables)

Clauses:
  ALO rows (4):    (x_{0,0} ∨ x_{0,1} ∨ x_{0,2} ∨ x_{0,3}), ...
  AMO rows (24):   (¬x_{0,0} ∨ ¬x_{0,1}), (¬x_{0,0} ∨ ¬x_{0,2}), ...
  ALO cols (4):    (x_{0,0} ∨ x_{1,0} ∨ x_{2,0} ∨ x_{3,0}), ...
  AMO cols (24):   (¬x_{0,0} ∨ ¬x_{1,0}), ...
  Forbidden (18):  for each edge, pairs with |p−q| > 1
    e.g. edge (0,1): (¬x_{0,0} ∨ ¬x_{1,2}), (¬x_{0,0} ∨ ¬x_{1,3}), ...

Solution: SAT. Model: x_{0,0}=T, x_{1,1}=T, x_{2,2}=T, x_{3,3}=T → f = [0,1,2,3], all spans = 1 ≤ k ✓

Base Overhead: n=4, m=3, k=1 → base num_vars = 16, base num_clauses = 74.

After strict 3-SAT conversion, auxiliary variables and clauses are added (from ALO conversion), so final counts are larger than the base CNF counts above.

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	GraphBandwidth does not exist yet; novel reduction to a new source model
Non-trivial	✅ Pass	Constructs permutation matrix + forbidden-pair gadgets; genuine structural transformation
Correctness	⚠️ Warn	Reference exists but does not specifically cover graph bandwidth encoding; the reduction itself is a standard permutation-to-SAT construction
Well-written	⚠️ Warn	Overhead formulas use Big-O instead of exact expressions; minor notation gaps

Overall: 2 passed, 0 failed, 2 warnings

---

Usefulness

GraphBandwidth is not yet in the reduction graph (pred show GraphBandwidth returns "Unknown problem"). No path from GraphBandwidth to KSatisfiability (or any other problem) exists. This is a novel reduction that introduces a new problem into the graph and connects it to the well-supported SAT ecosystem. The motivation is clear: enabling SAT-solver-based exact solving of bandwidth with binary search on k.

Verdict: Pass.

Non-trivial

The reduction constructs a full permutation matrix encoding (n² Boolean variables with ALO/AMO row and column constraints) plus forbidden-pair clauses derived from the edge set and bandwidth bound. This involves:

• Auxiliary variables for the sequential encoding of long ALO clauses into 3-SAT
• Pairwise AMO clauses with literal-duplication padding to length 3
• Structural forbidden-pair constraints coupling graph topology to positional distance

This is a genuine structural transformation, not a variable substitution or subtype coercion.

Verdict: Pass.

Correctness

Reference verification:

• Prestwich (2009), "CNF Encodings," Handbook of Satisfiability, Chapter 2 — This chapter exists and is published by IOS Press (DOI: 10.3233/978-1-58603-929-5-75). It covers general CNF encoding methodology including ALO/AMO constraints, pairwise vs. sequential encodings, and Tseitin transformations. However, the chapter is a general encoding reference — it does not specifically present a graph bandwidth to SAT reduction. The reduction in the issue is a standard permutation-to-SAT encoding (well-known technique) applied to the bandwidth decision problem, so citing Prestwich as a general encoding reference is reasonable but not a direct source for this specific reduction.

• The NP-completeness of graph bandwidth was established by Papadimitriou (1976), "The NP-Completeness of the bandwidth minimization problem," Computing 16, 263–270. This foundational result is not cited in the issue but would strengthen it.

Mathematical verification of the example:

The P4 example (n=4, m=3, k=1) checks out:

• 16 base variables (4×4 permutation matrix)
• ALO rows: 4 clauses, AMO rows: 24 clauses, ALO cols: 4 clauses, AMO cols: 24 clauses
• Forbidden pairs: 3 edges × 6 forbidden position-pairs each = 18 clauses
• Total base clauses: 74 ✓
• The identity permutation [0,1,2,3] is a valid solution with all edge spans = 1 ≤ k ✓

The encoding logic (ALO + AMO for rows and columns to enforce a permutation, forbidden pairs for bandwidth) is a correct and standard approach.

Verdict: Warn — The cited reference is a valid general encoding chapter but does not specifically describe this reduction. Recommend adding the Papadimitriou (1976) citation for NP-completeness and noting that the construction is a standard permutation-matrix SAT encoding applied to the bandwidth decision problem.

Well-written

4a — Information Completeness: All required sections (Source, Target, Motivation, Reference, Reduction Algorithm, Size Overhead, Validation Method, Example) are present and substantive.

4b — Algorithm Completeness: The reduction algorithm is detailed and step-by-step: variable mapping with explicit indexing formula, five numbered constraint groups, and the 3-SAT conversion strategy (sequential encoding for long clauses, literal duplication for short ones). An implementer could follow this.

4c — Symbol and Notation Consistency:

• Symbols are generally well-defined: G=(V,E), n=|V|, m=|E|, k = bandwidth bound, x_{i,p} with clear semantics.
• The indexing formula id(i,p) = i·n + p + 1 references 1-based DIMACS literal IDs, which is a CNF convention but not how KSatisfiability variables work in this codebase (0-based variable indices). This is a minor note for implementation.

4d — Overhead Table Issues:

• The overhead formulas use Big-O notation (O(n²), O(n³ + m·n²)) instead of exact polynomial expressions. The #[reduction(overhead = {...})] macro requires concrete symbolic expressions using source getter method names (e.g., num_vertices, num_edges), not asymptotic notation. The issue should provide exact formulas.
• The num_literals field of KSatisfiability is not addressed in the overhead table (only num_vars and num_clauses are listed). While num_literals can be derived (3 × num_clauses for 3-SAT), it should be explicitly stated.
• The overhead lists two alternatives ("with pairwise AMO" vs "with sequential AMO") without committing to one. The implementation must choose one encoding, and the overhead should reflect that choice exactly.

4e — Example Quality: The example is well-worked with concrete clause counts and a verified solution. It is small enough to check by hand.

Verdict: Warn — The overhead table needs exact formulas instead of Big-O, must include num_literals, and should commit to one AMO encoding choice.

Recommendations

• Add the Papadimitriou (1976) citation for NP-completeness of graph bandwidth.
• Replace Big-O overhead expressions with exact formulas. For pairwise AMO encoding: num_vars = n^2 + 2 * n * (n - 2) (base + auxiliary for ALO→3-SAT conversion), num_clauses = 2 * n * (n - 1) + 2 * n + m * n * (n - 1) - 2 * m * k + <ALO conversion clauses>, num_literals = 3 * num_clauses.
• Add num_literals to the overhead table.
• Commit to one AMO encoding (pairwise is simpler; sequential gives fewer clauses) and give the exact formula for that choice.
• Note that variable indices in the implementation should be 0-based (not DIMACS 1-based).

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Source problem (GraphBandwidth) does not yet exist in the reduction graph; novel reduction
Non-trivial	✅ Pass	Constructs bijection variables, ALO/AMO constraints, forbidden-pair clauses, and 3-SAT conversion with auxiliary variables
Correctness	✅ Pass	Prestwich (2009) verified; encoding approach is standard for permutation-to-SAT reductions
Well-written	⚠️ Warn	Minor issues in overhead table and notation (see details)

Overall: 3 passed, 0 failed, 1 warning

---

Usefulness

GraphBandwidth is not yet implemented in the codebase (pred show GraphBandwidth fails). No existing path exists from GraphBandwidth to KSatisfiability or any other problem. This is a novel reduction that would connect a new graph ordering problem to the SAT solver ecosystem. The motivation is clear: enabling SAT-based solving of bandwidth decision problems with binary search for optimization.

Non-trivial

The reduction involves genuine structural transformation:

• Introduces n^2 Boolean variables encoding a bijection (vertex-to-position assignment)
• Constructs ALO and AMO constraints for both rows and columns (doubly stochastic assignment matrix)
• Generates forbidden-pair clauses from the edge set and bandwidth bound
• Requires a non-trivial 3-SAT conversion step with auxiliary variables for long ALO clauses

This is clearly not a variable substitution or subtype coercion.

Correctness

Reference verification:

• Prestwich, S. D. (2009). "CNF Encodings." In Handbook of Satisfiability, Chapter 2, pp. 75-97, vol. 185 FAIA, IOS Press. DOI: 10.3233/978-1-58603-929-5-75 — Verified. The DOI resolves correctly to IOS Press. The chapter covers CNF encoding techniques for combinatorial problems including Tseitin encodings and constraint encodings. It is a well-known reference in the SAT community.

The encoding approach (Boolean variables x_{i,p} for vertex-position assignment with ALO/AMO and forbidden-distance constraints) is a standard permutation-to-SAT encoding pattern, well-established in the constraint programming and SAT literature. The specific application to graph bandwidth follows naturally from the problem definition.

Example verification: For P4 with k=1:

• 16 variables (4 vertices x 4 positions) — correct
• ALO rows: 4 clauses — correct
• AMO rows: 4 * C(4,2) = 24 clauses — correct
• ALO cols: 4 clauses — correct
• AMO cols: 24 clauses — correct
• Forbidden pairs: 3 edges x 6 forbidden (p,q) pairs per edge = 18 — correct
• Total base clauses: 4+24+4+24+18 = 74 — matches the issue
• Solution f=[0,1,2,3] with all spans = 1 is valid — correct

Note: The reference (Prestwich 2009) covers general CNF encoding techniques but does not specifically discuss graph bandwidth. The reduction described in the issue is a straightforward application of these encoding techniques to the bandwidth decision problem. This is fine — the encoding is standard and does not require a bandwidth-specific reference.

Well-written

4a: Information Completeness — All required sections are present and substantive. ✅

4b: Algorithm Completeness — The step-by-step procedure is detailed enough to implement: variable mapping is explicit, each constraint group is enumerated, 3-SAT conversion method is specified (sequential encoding with auxiliary variables, literal duplication for short clauses). ✅

4c: Symbol and Notation Consistency — Minor issues:

• ⚠️ The overhead table uses Big-O notation (O(n^2), O(n^3 + m*n^2)) instead of exact symbolic expressions using source getter method names. The #[reduction(overhead = {...})] macro requires exact expressions referencing getter methods (e.g., num_vertices, num_edges), not asymptotic bounds. The implementer will need to derive the exact formulas. For instance, with pairwise AMO encoding: num_vars = n^2 + 4*(n-3) auxiliary (from sequential encoding of 4 ALO clauses of length n), and num_clauses needs exact counting rather than Big-O.
• ⚠️ The overhead table lists two alternative formulas for num_clauses (pairwise AMO vs sequential AMO) without specifying which one the implementation should use. The implementation must pick one.

4d: Example Quality — The example is well-chosen: P4 with k=1 is small enough to verify by hand, exercises all constraint groups, has a clear solution, and the clause counts are fully worked out. ✅

Recommendations

• Replace the Big-O overhead formulas with exact symbolic expressions using source problem getter method names (e.g., num_vertices, num_edges, bandwidth_bound). For pairwise AMO: num_vars = num_vertices^2 + 4*(num_vertices - 3), num_clauses = 4*num_vertices + 2*num_vertices*(num_vertices-1) + .... Choose one AMO encoding strategy and commit to it.
• The issue depends on a GraphBandwidth model that does not yet exist. A corresponding [Model] issue should be filed (or referenced) before this rule can be implemented.

[GiggleLiu]

Closing: this SAT encoding is a multi-step solving strategy (binary search over k with O(log n) SAT calls), not a single-step reduction compatible with the ReduceTo framework.

The source problem MinimumGraphBandwidth has been modeled as an OptimizationProblem (Minimize) — see #133. The optimization version has no bound parameter k, so constructing a single SAT instance requires knowing the target bandwidth in advance. SAT-based solvers handle this internally via binary search, but that's a solving technique, not a primitive reduction.

The ILP reduction (#136) provides a clean single-step opt→opt path for solver-based solving.