KSatisfiability → TimetableDesign reduction: gadget blowup 64·L² seems excessive

[isPANN]

Summary

src/rules/ksatisfiability_timetabledesign.rs declares an overhead of

num_craftsmen = 64 * num_literals^2 + 32 * num_literals + 1
num_tasks     = 64 * num_literals^2 + 32 * num_literals + 1
num_periods   = 4 * num_literals

This O(L²) constant of 64 looks suspiciously large and produces unusable example instances.

Observed impact

On the canonical fixture (source: 2 clauses, 2 variables, L=6 literal occurrences), the reduced target instance is:

• num_craftsmen = 696
• num_tasks = 662
• num_periods = 20
• dims product = 9,215,040 configuration entries, only 1362 of which are 1

This single example bloats docs/paper/data/examples.json to 19 MB (27 MB of the 30 MB raw JSON is just its target_config), and dominates Typst paper compile time. Source minimization can't help — this is already the smallest non-trivial 3-SAT input.

Suspected root cause

The reduction chain (Even–Itai–Shamir 1976 style): bounded-occurrence preprocessing → list-edge-coloring → 3-edge-path gadget replacement for 2-list edges → color-blocking craftsmen/tasks. The 64× constant likely comes from nested gadget replication (path replacement × color count × blocker duplication), possibly multiplied redundantly.

Worth checking:

1. Is every blocker craftsman/task actually needed, or are some duplicates of an existing constraint?
2. Can the path gadget be shared across list-edge-coloring edges that touch the same vertex?
3. Does the literature (Even–Itai–Shamir 1976 or later simplifications) give a tighter construction, e.g. linear in L rather than 64·L²?

Definition of done

• Reduction still passes closed-loop tests and agrees with NP-hardness proof.
• Overhead constants documented and cited from the literature.
• Canonical fixture for KSat → TimetableDesign has target dims small enough that examples.json returns to a reasonable size (target: full rule fixture < 100 KB).

Related

• Discovered while profiling slow Typst paper compilation (27 s → 9.7 s after pre-indexing; remaining ~10 s dominated by parsing this fixture).
• File: src/rules/ksatisfiability_timetabledesign.rs:805-808