diff --git a/docs/paper/reductions.typ b/docs/paper/reductions.typ index 413ed4790..9797e57af 100644 --- a/docs/paper/reductions.typ +++ b/docs/paper/reductions.typ @@ -269,6 +269,7 @@ "SpinGlass": [Spin Glass], "QUBO": [QUBO], "ILP": [Integer Linear Programming], + "DecisionILP": [Binary Decision Integer Linear Programming], "IntegerKnapsack": [Integer Knapsack], "Knapsack": [Knapsack], "PartiallyOrderedKnapsack": [Partially Ordered Knapsack], @@ -5100,6 +5101,30 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| ] } +#problem-def("DecisionILP")[ + Given a binary integer linear program with integer coefficients, a minimization + or maximization sense, and an integer bound $b$, find $x in {0,1}^n$ satisfying + all constraints and $c^top x <= b$ for minimization, or $c^top x >= b$ for maximization. +][ + This is the objective-threshold form of binary ILP. Binary adders translate its + pseudo-Boolean constraints to SAT @een2006. Exhaustive enumeration takes + $O^*(2^n)$ time; this is the registered reference bound, not a claim of a tight + best-known SAT solving bound. The registered SAT reduction answers a fixed + objective-threshold query; no reverse ILP-to-DecisionILP edge is registered. + + *Example.* #let x = load-model-example("DecisionILP") + Select exactly one of #x.instance.inner.variables.len() variables and minimize + the objective with coefficients + #x.instance.inner.objective.map(t => str(t.at(1))).join(", "). + At bound #x.instance.bound, the witness + $(#fmt-values(x.optimal_config))$ has objective #x.instance.bound and meets the bound. + #pred-commands( + "pred create --example " + problem-spec(x) + " -o x.json", + "pred solve x.json", + "pred evaluate x.json --config " + cli-config(x.optimal_config), + ) +] + #{ let x = load-model-example("QuadraticAssignment") let C = x.instance.cost_matrix @@ -5369,6 +5394,8 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V| ][ Simultaneous Incongruences is an NP-complete problem @garey1979. It asks whether the complement of a system of congruences — a _covering system_ — can be simultaneously avoided. A _covering system_ is a finite collection of congruences $\{a_i space (op("mod") space b_i)\}$ that covers every integer; when the system is a covering system there is no valid $x$ and the instance is a "no" instance. The problem generalises checking whether a given set of congruences is a covering system, which has connections to Erdős's covering conjecture and sieve methods in analytic number theory. + Exhaustive search tests the $L = op("lcm")(b_1, dots, b_n)$ candidates in one full period, checking at most $n$ incongruences per candidate. With `lcm_bits` $= floor(log_2 L) + 1$, the catalog bound is $O((n+1) 2^"lcm_bits")$, counting fixed-width arithmetic operations. The period can be exponential in the binary input length, so this is not a polynomial-time algorithm.#footnote[The catalog records exhaustive search; a better general exact bound has not been independently verified from the literature.] + *Example.* Let $n = #pairs.len()$ with pairs #pairs.map(p => $(#p.at(0), #p.at(1))$).join(", "). The full period is $L = op("lcm")(#fmt-values(moduli)) = #lcm-val$. We test $x = #xval$: #pred-commands( @@ -12033,6 +12060,333 @@ The _penalty method_ @glover2019 @lucas2014 converts a constrained optimization $ f(bold(x)) = "obj"(bold(x)) + P sum_k g_k (bold(x))^2 $ where $P$ is a penalty weight large enough that any constraint violation costs more than the entire objective range. Since $g_k (bold(x))^2 >= 0$ with equality iff $g_k (bold(x)) = 0$, minimizers of $f$ are feasible and optimal for the original problem. Because binary variables satisfy $x_i^2 = x_i$, the resulting $f$ is a quadratic in $bold(x)$, i.e.\ a QUBO. +== Direct Ordering, Scheduling, and Assignment QUBOs + +The following constructions apply the integer penalty method @glover2019 @lucas2014 directly, without an intermediate ILP. Write the expanded source objective as $f(x) = c + sum_(a <= b) q_(a b) x_a x_b$, after combining coefficients. Set $L = c + sum_(a <= b) min(0, q_(a b))$, $U = c + sum_(a <= b) max(0, q_(a b))$, and $P = U - L + 1$. For the nonnegative integer violation sum $g$ defined in each rule, expand $F = f + P g$ and store its nonconstant terms as QUBO energy $E = F - C$. + +A source witness has $g = 0$, so its energy lies in $[L-C,U-C]$ and adding $C$ recovers its objective. Conversely, any invalid assignment has $g >= 1$, hence $F >= L+P > U$. Thus every target minimum in the interval decodes to a source optimum; a minimum outside it maps to `Min(None)`. This also handles infeasible precedence systems. For feasibility rules use $f = 0$, $P = 1$, and DecisionQUBO bound $-C$; completed `Or` values map identically. Every decoder first validates the target witness and its energy certificate. Coefficients, constants, and energy bounds use checked integer arithmetic; unrepresentable encodings return an overflow error. + +#let direct-qubo-commands(source, target, source-variant: none) = { + let data = load-example(source, target, source-variant: source-variant) + let solution = data.solutions.at(0) + pred-commands( + "pred create --example " + rule-spec(data) + " -o source.json", + "pred path " + problem-spec(data.source) + " " + problem-spec(data.target) + " --limit all --quiet --json | jq ' .paths[] | select(.steps == 1)' > route.json", + "pred reduce source.json --via route.json -o bundle.json", + "pred solve bundle.json", + "pred evaluate source.json --config " + cli-config(solution.source_config), + ) +} + +#reduction-rule("SequencingToMinimizeWeightedCompletionTime", "QUBO", example: true, + extra: [#direct-qubo-commands("SequencingToMinimizeWeightedCompletionTime", "QUBO")], +)[ + Weighted completion sequencing has a direct QUBO on $n(n-1)/2$ comparison bits, including signed processing times and weights. +][ + _Construction._ For $ib$, and one when $a=b$. + + _Correctness._ A legal order gives no directed triangles and satisfies every precedence. Each task contributes its own processing time times its weight, and each earlier task contributes its processing time times the later task's weight, yielding $f$. Conversely, a tournament with no directed triangle is transitive: a shortest longer directed cycle has a chord producing a shorter directed cycle. Its unique order satisfies all zero-penalty precedences. The shared penalty bound separates all invalid bitstrings, including cyclic precedence instances. + + _Source arithmetic._ Before expansion, bound every elapsed-time prefix by the sums of negative and positive processing times. For each task, include its own duration in the completion-time bounds, multiply both endpoints by its weight, then bound all partial objective sums by the sums of negative minima and positive maxima. Reject bounds outside `i64`; algebraic cancellation must not hide source evaluation overflow. + + _Extraction and size._ Count incoming arcs to obtain each task's rank and invert these ranks to an ordered task list. There are exactly $n(n-1)/2$ bits and at most $3 binom(n,3)$ couplings: each triple supplies three pairs of comparison bits, while precedences are linear. The canonical example orders the highest-weight unit jobs first; its source and target witnesses are shown below. +] + +#reduction-rule("MaximumLikelihoodRanking", "QUBO", example: true, + extra: [#direct-qubo-commands("MaximumLikelihoodRanking", "QUBO")], +)[ + Maximum likelihood ranking reduces directly to a comparison-bit QUBO with $n(n-1)/2$ variables. +][ + _Construction._ Use the preceding tournament bits and triangle penalties, with no precedence penalties. For comparison matrix $M$, set + $ f = sum_(i=q$, reducing squared bits to linear terms even for self precedences. The objective is $f = sum_(i,p: p+1>d_i) x_(i p)$, where $d_i$ is the task deadline. + _Correctness._ A valid schedule activates a permutation matrix, violates no precedence, and contributes one precisely for each late job. Conversely, zero row and column penalties yield a permutation; zero precedence products force the required strict ordering. Its objective is the number of late jobs. The penalty bound detects cycles and self precedences as infeasible sources. + _Extraction and size._ Read each task's selected position and invert to the ordered task list. Exactly $n^2$ bits are used, with at most $n^2(n^2-1)/2$ off-diagonal terms. The canonical schedule meets all deadlines. + + _Positive integer lengths._ The `i64` constructor requires strictly positive lengths, but accepts signed deadlines. Set $H=sum_i p_i$ and use choices $t=0,dots,H-p_i$ per task. Add one-hot row squares and conflicts between overlapping selected intervals, plus every precedence pair whose starts satisfy $t>=u$ (a self precedence penalizes every selected row bit). The objective charges one exactly when $t+p_i>d_i$. With $U$ the sum of all choice costs, use $P=U+1$. + + _Correctness for integer lengths._ ($arrow.r.double$) Prefix starts of any legal permutation fit the horizon, have zero penalties, and give its exact late-task count. ($arrow.l.double$) A zero-penalty selection consists of nonoverlapping intervals of total duration $H$ inside $[0,H]$, so they fill the horizon without gaps. Sorting starts reconstructs the exact source completion times and respects all precedences. Invalid selections cost more than $U$; an infeasible source therefore recovers `Min(None)`. Source elapsed-time prefixes fit the checked positive total $H$. + + _Integer extraction and size._ Validate the energy interval, decode starts and sort to an order. Exactly $S=sum_i(H-p_i+1)$ bits and at most $S(S-1)/2$ couplings are used. For processing magnitude bits $h$, $S<=n^2 2^h$. The registry reports unavailable size transforms because its expression contract permits only constant integer exponents. This is pseudopolynomial in processing times; it can exceed binary-time alternatives. A simple construction enumerates $O((1+q)S^2)$ conflict candidates for $q$ precedences, plus sparse accumulation costs. + + *Integer example.* #let weighted = load-example("MinimumTardinessSequencing", "QUBO", source-variant: (weight: "i64")) + Lengths #repr(weighted.source.instance.lengths), deadlines #repr(weighted.source.instance.deadlines), and order #repr(weighted.solutions.at(0).source_config) give completions 1, 2, 4 and one late task. The target has #weighted.target.instance.num_vars variables. + +] + +#reduction-rule("QuadraticAssignment", "QUBO", example: true, + extra: [#direct-qubo-commands("QuadraticAssignment", "QUBO")], +)[ + Quadratic assignment with $n<=m$ facilities and locations reduces directly to $n m$ bits. +][ + _Construction._ Let $x_(i p)$ assign facility $i$ to location $p$. Penalize each row by $(1-sum_p x_(i p))^2$ and each column by $sum_(i0$. Empty groups are allowed by the source definition. + _Correctness._ Each partition activates exactly one bit per item and its objective is the sum of squared group totals. Conversely, zero row penalties assign each item once; substitution gives those same group totals and objective. The shared penalty lemma excludes dropped or multiply assigned items. + _Extraction and size._ Return each item's selected group. There are exactly $n k$ bits and at most $n k(k-1)/2+k n(n-1)/2$ couplings: same-item pairs from the constraints and same-group pairs from the objective. These two pair families are disjoint. The example splits the total size equally between its two groups. +] + +#reduction-rule("OptimalLinearArrangement", "QUBO", example: true, + extra: [#direct-qubo-commands("OptimalLinearArrangement", "QUBO")], +)[ + Optimal linear arrangement on `SimpleGraph` reduces to $n(n-1)/2$ tournament comparison bits. +][ + _Construction._ Let $r_(i j)$ mean that vertex $i$ precedes vertex $j$, with $r_(j i)=1-r_(i j)$. For $m$ source edges set + $ F=m+sum_((u,v) in E) sum_(w != u,v) (r_(u w)+r_(v w)-2r_(u w)r_(v w)). $ + For $n>=2$ let $U=m(n-1)$; empty and singleton graphs have $U=0$. Add the tournament triangle penalties with weight $P=U+1$, remove the resulting constant $C$, and recover completed minima by adding $C$ inside $[0,U]$. + _Correctness._ A source ordering gives a transitive tournament. For each edge, the XOR of its endpoints' comparisons with $w$ equals one precisely when $w$ lies strictly between those endpoints. Thus its contribution is one plus the number of intermediate vertices, equal to the rank distance. Conversely, every XOR and triangle penalty is nonnegative on arbitrary bits. A positive triangle penalty costs more than $U$, so a target inside the recovery interval has no directed triangle and hence is a total order. Predecessor counts give its ranks, and the same between-vertex identity proves equality of the objective. Every graph has a feasible ordering, including the empty graph. + _Extraction and size._ Validate the target, reject cycles, and return predecessor counts. Exactly $n(n-1)/2$ bits and at most $3 binom(n,3)=n(n-1)(n-2)/2$ couplings suffice: objective terms and triangle penalties couple only comparisons sharing a vertex, and every such pair belongs to one index triple. The coupling bound is cubic even for dense graphs. Construction uses $O(n^3+m n)$ coefficient additions; ordered maps add a logarithmic factor. For the canonical three-vertex path, $U=4$, $P=5$, $C=2$, and the all-true comparison vector has target value zero, recovering source cost two. +] + +#reduction-rule("SequencingWithinIntervals", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("SequencingWithinIntervals", "DecisionQUBO")], +)[ + Interval-constrained sequencing has a direct decision QUBO using one bit for each allowed integer start slot. +][ + _Construction._ Task $i$ has release $r_i$, deadline $d_i$, and duration $l_i$. Allocate $s_i=max(0,d_i-r_i-l_i+1)$ bits for starts $r_i+t$, $0<=t0$ and both resources are available in period $h$. Add $(sum_h x_(c t h)-R_(c t))^2$ for every demand and one product for each pair sharing a period and either resource. Remove $C=sum_(c,t)R_(c t)^2$ and use decision bound $-C$. If a demand is negative or exceeds its eligible-period count, use the zero polynomial on the same variable set with bound $-1$ instead. + _Correctness._ A feasible timetable meets every demand and has no resource conflict, so all penalties vanish. Conversely, zero demand squares enforce exact assignment counts and zero conflict products enforce exclusivity. Unavailable or zero-demand cells are false by construction. The special target is unsatisfiable precisely in the immediately impossible-demand branch: a sum of eligible boolean cells cannot equal such a demand. + _Extraction and size._ Fill a false craftsman-task-period tensor and insert the eligible selected bits. The target has exactly $A$ variables and at most $A(A-1)/2$ couplings, where $A$ is the eligible-assignment count, including the impossible-demand branch. +] + + +== Further direct integer QUBO constructions + +The following rules use the checked penalty and aggregate-recovery conventions above. Their constructions adapt the quadratic penalty method @glover2019; each proof states the exact source semantics. + +#reduction-rule("SchedulingWithIndividualDeadlines", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("SchedulingWithIndividualDeadlines", "DecisionQUBO")], +)[ + Unit-task scheduling with individual deadlines reduces to a decision QUBO with deadline-valid starts and exact processor capacities. +][ + _Construction._ For $n$ tasks and processor capacity $m$, allocate row bits $x_(i t)$ for $0 <= t < h_i = min(d_i,n)$. Add $(sum_t x_(i t)-1)^2$ for each task. At time $t$ let $k_t$ be the number of available task bits. If $m < k_t$, introduce $b= floor(log_2(m))+1$ slack bits with weights $1,2,dots,2^(b-1)$ (no slack bits for $m=0$), and add $(sum_i x_(i t)+s_t-m)^2$. Omit automatically satisfied capacities. For each precedence $(i,j)$ add $x_(i t)x_(j u)$ for every $t>=u$, including repeated indices for self precedences. Use unit penalties and bound $-C$. + +_Correctness._ $arrow.r.double$: compress the occupied slots of a source schedule to consecutive integers starting at zero. There are at most $n$ occupied slots; this preserves strict precedences and capacity and only decreases completion times. Choose these starts and the representable slack $m-sum_i x_(i t)$, obtaining zero penalty. $arrow.l.double$: zero penalty selects exactly one deadline-valid start per task, respects every capacity, and has no forbidden precedence pair. Empty rows and cyclic or self precedences remain infeasible. + +_Solution extraction and bounds._ Decode the unique start in each row. Completed `Or` values map identically. The actual variable count is $sum_i h_i + sum_(t: m v$ add $w_(u v)(1-r_(u v))$ using the tournament convention. Parallel arcs remain separate source indices; their coefficients add. Apply the shared objective interval and triangle penalty $P=U-L+1$. Before cancellation, check the sums of all negative and all positive source weights, bounding every selected-prefix sum. + +_Correctness._ $arrow.r.double$: augment any feasible removal set with every negative arc, without increasing cost. Topologically order its retained graph. All backward arcs were removed; discarding any additionally removed forward nonnegative arcs cannot increase the objective. This produces a canonical order with no greater cost. $arrow.l.double$: removing negative arcs, loops and all backward arcs leaves only forward arcs and hence a DAG, whose removal cost equals the quadratic objective. These inequalities prove equal optima; the shared penalty separates every cyclic target tournament. This argument covers signed, zero, loop and parallel-arc semantics. + +_Solution extraction and bounds._ Remove each indexed arc exactly when its weight is negative, it is a loop, or its endpoints are backward in the decoded order. Add the omitted constant for aggregate recovery inside the certified interval. With $v$ vertices, exactly $v(v-1)/2$ bits and at most $3 binom(v,3)$ couplings suffice; construction takes $O(m+v^3)$ additions. Empty graphs have objective zero. Every source has the all-arcs-removed feasible witness. + + *Example.* #let ex = load-example("MinimumFeedbackArcSet", "QUBO") + The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above. +] + +#reduction-rule("Partition", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("Partition", "DecisionQUBO")], +)[ + Partition reduces to one selection bit per element by squaring the difference between subset totals @lucas2014. +][ + _Construction._ For positive sizes $s_i$ with validated total $S$, set $H=(2 sum_i s_i x_i-S)^2$ and remove $C=S^2$. Use bound $-C$. + +_Correctness._ $arrow.r.double$: equal subset totals make the residual zero. $arrow.l.double$: every square is nonnegative, so satisfying the energy threshold forces the selected sum to equal its complement. Odd totals therefore remain NO instances without a special branch. + +_Solution extraction and bounds._ Copy the selection bits; aggregate `Or` recovery is identity. Exactly $n$ variables and at most $n^2$ couplings are registered; expansion takes $O(n^2)$ arithmetic operations. Every source subtotal lies between zero and the checked total. Target coefficients, constant and energy sums are independently checked: a representable source need not yield a representable squared penalty. + + *Example.* #let ex = load-example("Partition", "DecisionQUBO") + The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above. +] + +#reduction-rule("SubsetSum", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("SubsetSum", "DecisionQUBO")], +)[ + Arbitrary-precision SubsetSum reduces to a checked integer decision QUBO with one bit per element. +][ + _Construction._ Expand $H=(sum_i s_i x_i-T)^2$ using arbitrary-precision signed integers. Only then convert the coefficients and $C=T^2$ into the target integer representation. Check positive and negative coefficient sums and use bound $-C$. + +_Correctness._ $arrow.r.double$: a subset of sum $T$ gives zero residual. $arrow.l.double$: satisfying the threshold forces the integer square to vanish and hence exactly the source equality. Empty selections and target zero follow the same equations. Arbitrary-precision input arithmetic is preserved; no input-size restriction is silently assumed. + +_Solution extraction and bounds._ Copy the bits and use identity `Or` recovery. Exactly $n$ variables and at most $n^2$ couplings suffice. Expansion takes $O(n^2)$ big-integer operations, whose bit cost depends on input magnitudes. Unrepresentable derived constants or coefficients return a typed numeric error. Expanding before conversion matters: a size $2^32$ and target $2^31$ produce a zero diagonal coefficient despite the intermediate size square exceeding `i64`. + + *Example.* #let ex = load-example("SubsetSum", "DecisionQUBO") + The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above. +] + +#reduction-rule("ExactCoverBy3Sets", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("ExactCoverBy3Sets", "DecisionQUBO")], +)[ + Exact cover by 3-sets reduces to a decision QUBO with one bit per indexed subset @lucas2014. +][ + _Construction._ For universe $U$ and subset-selection bits $x_j$, set $H=sum_(u in U)(sum_(j: u in S_j)x_j-1)^2$. The omitted constant is $C=|U|$; use bound $-C$. Duplicate subsets retain distinct bits. + +_Correctness._ $arrow.r.double$: an exact cover selects each element exactly once and makes every equation vanish. $arrow.l.double$: zero penalty means every element is covered once, so selected triples are disjoint and cover the whole universe. Summing incidences gives exactly $|U|/3$ selected triples, matching the source's cardinality check. Uncovered elements contribute unavoidable constants; the empty universe gives the empty cover. + +_Solution extraction and bounds._ Copy the subset bits; aggregate recovery is identity. Exactly $m$ bits and at most $m^2$ couplings suffice. The implementation scans incidences in $O(|U|m)$ time and expands only intersecting rows, with at most three contributions per pair of triples. Diagonals are $-3$ and pair coefficients twice the intersection cardinality. + + *Example.* #let ex = load-example("ExactCoverBy3Sets", "DecisionQUBO") + The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above. +] + +#reduction-rule("StaffScheduling", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("StaffScheduling", "DecisionQUBO")], +)[ + Integer worker multiplicities reduce to bounded binary budget and coverage residuals, using the squared-equality construction of @lucas2014. +][ + _Construction._ Let $s$ be the number of indexed schedule patterns, $p$ the number of periods, $W >= 0$ the worker budget, $a_(j t)$ the pattern incidence, and $r_t$ the signed requirement. Encode each count $c_j$ and unused budget $z$ in $[0,W]$ with bounded binary weights: successive powers of two and a final remainder, whose sum is exactly the upper bound. This represents every integer in the interval and no others. For each $r_t>0$, encode surplus $h_t$ in $[0,W-r_t]$. A requirement above $W$ instead emits the constant NO decision with no variables and bound $-1$. Otherwise expand + $ H=(sum_j c_j+z-W)^2 + sum_(t:r_t>0)(sum_j a_(j t)c_j-h_t-r_t)^2. $ + Remove $C=W^2+sum_(t:r_t>0)r_t^2$ and use decision bound $-C$. Nonpositive requirements need no row, including the minimum signed integer; empty and duplicate patterns retain their source meaning. + + _Correctness._ $arrow.r.double$: a feasible staffing vector has unused budget $z=W-sum_j c_j$ and nonnegative coverage surplus at most $W-r_t$, so all squares vanish. $arrow.l.double$: a target witness meeting the bound has $H<=0$. Every square is nonnegative, so the budget and coverage equations hold exactly. All decoded counts are nonnegative, their sum is at most $W$, and every positive requirement is met. Nonpositive requirements hold automatically. Unit penalties suffice because this endpoint is feasibility, with no competing objective. + + _Solution extraction and bounds._ Validate target feasibility, then sum each schedule's weighted bits. Aggregate `Or` recovery is identity, including NO results and the existing ExactCoverBy3Sets incoming route. With $b(B)=ceil(log_2(B+1))$, the exact variable count outside the early NO case is $(s+1)b(W)+sum_(t:r_t>0)b(W-r_t)$. With $beta$ the magnitude bits of $W$ (so $b(W-r_t)<=b(W)<=beta$), this is at most $N=beta(s+p+1)$, with at most $binom(beta(s+1),2)+p(beta^2 s+binom(beta,2))$ registered couplings. The budget row already contains every count-count pair and every count-budget pair. Each period adds only count-surplus pairs (at most $beta^2 s$) and within-surplus pairs (at most $binom(beta,2)$); different periods' surplus blocks never interact. The coupling bound is therefore $O(s^2+s p+p)$, linear in periods for fixed schedule count. Construction performs $O((p+1)(s+1)^2+s+p)$ coefficient updates and row bookkeeping for fixed $beta$, since each coverage square may revisit count-count coefficients; ordered-map updates add a logarithmic factor. Bit counts grow logarithmically with the budget. Before expansion, check $s W$ to protect the source's count and coverage folds. Dimension arithmetic, expanded coefficients, omitted constant, and separate positive and negative coefficient sums are checked independently; an unrepresentable construction returns a typed overflow error. The conservative guard can reject representable special cases. + + *Example.* #let ex = load-example("StaffScheduling", "DecisionQUBO") + The canonical source assigns #repr(ex.solutions.at(0).source_config) workers across its #ex.source.instance.schedules.len() patterns, with budget #ex.source.instance.num_workers. The required coverages are #repr(ex.source.instance.requirements). The count blocks, unused-budget block and coverage-surplus blocks produce the displayed target; its canonical bits make every residual zero. +] + +#reduction-rule("ThreePartition", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("ThreePartition", "DecisionQUBO")], +)[ + ThreePartition reduces to multiplicities of eligible value triples, without labeled-group assignment bits. +][ + _Construction._ For each distinct size $v$, let $c_v$ count its indexed items. Enumerate unordered value triples $t=(a,b,c)$ with $a+b+c=B$. Write $r_(v t)$ for the number of occurrences of $v$ in $t$, and discard triples needing unavailable copies. A triple multiplicity $z_t$ is bounded by $M_t=min_(v:r_(v t)>0) floor(c_v/r_(v t))$. Encode it with bounded binary weights whose sum is $M_t$, then expand + $ H=sum_v (sum_t r_(v t) z_t-c_v)^2. $ + Remove $C=sum_v c_v^2$ and use decision bound $-C$. All penalties have unit weight. Pair enumeration and lookup of $B-a-b$ find the eligible triples. + + _Correctness._ A source partition supplies representable triple multiplicities satisfying every count equation. Conversely, a target at the threshold makes every square zero. For each selected triple copy, consume the next unused original index of each required value and assign those three indices one group. The count equations guarantee that every item is used exactly once; each group has sum $B$, and their number is $n/3$. The original positive-size, range, and total-sum constraints remain in force. If no triple is eligible, the target has zero variables and a negative decision bound, certifying NO. + + _Solution extraction and bounds._ Validate the target and perform the indexed assignment just described; completed `Or` values map identically. If $b_t$ is the bit count for $z_t$, bounded binary encoding gives $b_t<=M_t$. Charge three distinct indexed item pairs per unit of $M_t$. The multiplicity caps supply enough pairs even for repeated values. Different triple types cannot share a pair-value class because its missing value is uniquely $B-a-b$. Thus $3 sum_t M_t<=binom(n,2)$ and $N=sum_t b_t<=n(n-1)/6$. + + For one count row $v$, its triple types correspond to complementary value pairs summing to $B-v$. Each value has only one complement. A distinct pair contributes at most half its combined item count in bits; an equal pair contributes at most half its item count. Hence the number $D_v$ of bits in that row is at most $n/2$. Each bit occurs in at most three rows, so $sum_v D_v<=3N$ and $E<=sum_v binom(D_v,2)<=3N(n-2)/4<=n(n-1)(n-2)/8$. These bounds reduce both the Boolean exponent and the cubic coupling coefficient of labeled-group assignment. With $d$ distinct values, construction uses $O(d^2 log d)$ triple lookup work and $O(n^3)$ coefficient additions, with sparse-map logarithmic factors. Target coefficients depend on item counts rather than squared size magnitudes; all arithmetic remains checked. + + *Example.* #let ex = load-example("ThreePartition", "DecisionQUBO") + The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above. +] + +#reduction-rule("ThreeDimensionalMatching", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("ThreeDimensionalMatching", "DecisionQUBO")], +)[ + Perfect three-dimensional matching reduces to one selection bit per indexed triple. +][ + _Construction._ For each of the three axes and each coordinate $u$ add $(sum_(j: t_(j,"axis")=u)x_j-1)^2$. Remove constant $C=3q$ and use bound $-C$, where each axis has $q$ coordinates. + +_Correctness._ $arrow.r.double$: a perfect matching covers each coordinate once, so all equations vanish. $arrow.l.double$: zero penalty forces every coordinate on each axis to appear exactly once. Summing any axis gives exactly $q$ selected triples, and zero duplicate incidences proves pairwise coordinate disjointness. Indexed duplicate triples and the empty matching are covered by the same reasoning. + +_Solution extraction and bounds._ Copy the triple bits and recover `Or` identically. Exactly $m$ variables and at most $m^2$ couplings suffice. The incidence scans cost $O(q m)$ and expansion has at most three contributions per triple pair. This preserves perfect matching, rather than weakening it to arbitrary disjoint triples. + + *Example.* #let ex = load-example("ThreeDimensionalMatching", "DecisionQUBO") + The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above. +] + +#reduction-rule("StackerCrane", "QUBO", example: true, + extra: [#direct-qubo-commands("StackerCrane", "QUBO")], +)[ + StackerCrane reduces to a cyclic required-arc assignment QUBO using the source's exact connector evaluation contract. +][ + _Construction._ Let $n$ be the number of required directed arcs and $B$ their total length. Precompute $d_(i j)$ from the head of arc $i$ to the tail of arc $j$ by reusing the source Dijkstra routine on required directed arcs and optional undirected edges. This preserves its adjacency order, equal-distance tie order, maximum-integer sentinel, and overflow-to-unavailable behavior. For $n^2$ arc-position bits use $f=B+sum_(i,j,p) d_(i j)x_(i p)x_(j,(p+1) mod n)$ over available connectors, omitting $i=j$ when $n>1$. Add row and column one-hot squares and forbidden-transition products for unavailable connectors, with the shared penalty $P$. For $n=1$ include its diagonal connector once; for $n=0$ use zero objective. + +_Correctness._ $arrow.r.double$: a feasible source arc order selects a permutation matrix and available connectors, giving exactly its closed-walk cost. $arrow.l.double$: a certified target has a unique arc in each position and every required connector available, hence its decoded order evaluates to the same cost. Required arcs may be traversed again inside connectors, as allowed by the source. Disconnected sources have no unpenalized permutation. Before construction check $B+n max_(i,j: d_(i j) " available") d_(i j)$ for representability, independently of all target bounds, so every nonnegative route prefix is safe. + +_Solution extraction and bounds._ Invert the selected positions to the source-native arc-order witness. The source expands it into the closed walk using those same connector queries; no vertex-route witness is substituted. Recover the objective by adding the constant in the certified interval, and `Min(None)` outside it. Exactly $n^2$ bits suffice. Row and column penalties contribute $n^2(n-1)$ pairs, and cyclic transitions contribute at most another $n^2(n-1)$ pairs. Thus at most $2n^2(n-1)$ couplings suffice. For $n=1$ the connector is diagonal, and for $n=2$ reversed cyclic transitions may coincide; both satisfy the bound. There are $n^2$ shortest-path queries, each bounded by $O((v+e+n) log(v+e+n+1))$ for the lazy heap with parallel edges. Polynomial expansion uses $O(n^3)$ coefficient updates and storage; ordered-map updates add a logarithmic factor to time. + + *Example.* #let ex = load-example("StackerCrane", "QUBO") + The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above. +] + +#reduction-rule("ShortestCommonSuperstring", "QUBO", example: true, + extra: [#direct-qubo-commands("ShortestCommonSuperstring", "QUBO")], +)[ + ShortestCommonSuperstring reduces to an overlap-path assignment QUBO after exact containment preprocessing. +][ + _Construction._ Remove empty strings, duplicate strings (retain the first), and proper contained strings. For the retained $k$ strings let $o_(i j)$ be maximal suffix-prefix overlap. Use $k^2$ string-position bits and objective $f=sum_i |s_i|-sum_(p=0)^(k-2) sum_(i != j) o_(i j)x_(i p)x_(j,p+1)$, with row and column assignment penalties from the shared objective lemma. The source constructor accepts input symbols outside its declared alphabet; add an unconditional penalty for these infeasible instances, rather than producing an invalid reconstructed witness. + +_Correctness._ $arrow.r.double$: order retained strings by their occurrence starts in a shortest source superstring. With containment removed, their ends have the same strict order. Consecutive start distances are at least the preceding length minus maximal overlap, so the path objective is no greater than the source length. $arrow.l.double$: concatenate any path using its maximal overlaps. The current word ends with the previous string, so every retained string remains contained and the length is exactly $f$. Removed duplicates, substrings and empty strings are also contained. These two inequalities prove equality of optima. All-empty inputs give the empty word; an invalid alphabet symbol gives an infeasible source and no certified target value. + +_Solution extraction and bounds._ Decode a string permutation, concatenate with the recorded overlaps, and pad with `None` to the sum of original input lengths. Aggregate recovery uses the shared constant and interval. Actual variables are $k^2<=n^2$. Row and column penalties contribute $k^2(k-1)$ pairs. Each of the $k(k-1)$ directed string transitions has $k-1$ adjacent-position pairs, contributing at most $k(k-1)^2$ further pairs. Hence the coupling count is at most $k(k-1)(2k-1)<=n(n-1)(2n-1)$, cubic in the number of strings. The bound also covers $k=0$ and $k=1$. Naive containment and overlap preprocessing is bounded by $O(n^2 L^2)$ for original total length $L$, with $O(k^3)$ polynomial coefficient updates. Ordered-map updates add a logarithmic factor. Check source length conversion and target arithmetic independently. + + *Example.* #let ex = load-example("ShortestCommonSuperstring", "QUBO") + The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above. +] #let kc_qubo = load-example("KColoring", "DecisionQUBO") #let kc_qubo_sol = kc_qubo.solutions.at(0) #reduction-rule("KColoring", "DecisionQUBO", @@ -12111,11 +12465,11 @@ where $P$ is a penalty weight large enough that any constraint violation costs m $ H = a y_3 + 2(y_1 y_2 - 2 y_1 a - 2 y_2 a + 3a). $ Rosenberg's penalty is zero when $a=y_1 y_2$ and positive otherwise @borosgruber2014quadratization. Its multiplier 2 strictly exceeds the possible unit gain from the $a y_3$ term. Thus minimizing over each independent auxiliary gives exactly the clause falsification indicator, including repeated or complementary literals. Expand with $x^2=x$ into an upper-triangular QUBO matrix, and retain the omitted constant $C$. - _Correctness._ For every source assignment, the minimum target energy over auxiliaries is the number of falsified clauses minus $C$. Every clause expression is nonnegative before subtracting $C$. Hence the formula is satisfiable iff the global target minimum is exactly $-C$. A satisfying assignment lifts by setting each cubic auxiliary to $y_1 y_2$; every zero-penalty target configuration projects to a satisfying source assignment. If an empty clause occurs, its constant penalty 1 prevents the threshold from being attained. Empty formulas have $C=0$ and every source assignment satisfies them. + _Correctness._ For every source assignment, the minimum target energy over auxiliaries is the number of falsified clauses minus $C$. Every clause expression is nonnegative before subtracting $C$. Hence the formula is satisfiable iff the global target minimum is exactly $-C$. A satisfying assignment lifts by setting each cubic auxiliary to $y_1 y_2$; every zero-penalty target configuration projects to a satisfying source assignment. Empty formulas have $C=0$ and every source assignment satisfies them. _Extraction._ Formal target validation precedes decoding. The DecisionQUBO target checks the bound $E <= -C$, and the registered aggregate decoder maps its completed `Or` value identically. Direct witness extraction rejects energies above the bound and reads the first $n$ coordinates only for a satisfying target witness. It does not solve SAT or repair auxiliary assignments. A completed target decision gives the source decision. - _Domain and overhead._ The K2 variant has $n$ variables; K3 reserves $n+m$, with unused auxiliaries mathematically free for short clauses. Native `new_allow_less` permits widths up to K; CLI and serde still require exactly K per actual clause. Source and target both use `Or`; the target wraps the integer QUBO with the signed bound $-C$. Matrix and constant accumulation use checked arithmetic; literal indices come from the formal `CNFClause::variables` API. Neither endpoint nor variant changes. + _Domain and overhead._ The K2 variant has $n$ variables; K3 reserves $n+m$, one auxiliary per clause. Every clause has exactly K literals. Source and target both use `Or`; the target wraps the integer QUBO with the signed bound $-C$. Matrix and constant accumulation use checked arithmetic; literal indices come from the formal `CNFClause::variables` API. Neither endpoint nor variant changes. ] #let ksat_qc = load-example("KSatisfiability", "QuadraticCongruences") @@ -12149,9 +12503,9 @@ where $P$ is a penalty weight large enough that any constraint violation costs m *Multiplicity:* The fixture stores one canonical satisfying witness. ], )[ - The bounded quadratic-congruence construction of Manders and Adleman @mandersAdleman1976 converts an odd signed-knapsack target into a square congruence using prime powers and the Chinese Remainder Theorem. We give base-eight positions only to the actual normalized clauses. The same slack equation handles every native clause width from zero through three. + The bounded quadratic-congruence construction of Manders and Adleman @mandersAdleman1976 converts an odd signed-knapsack target into a square congruence using prime powers and the Chinese Remainder Theorem. We give base-eight positions only to the actual normalized clauses. The same slack equation handles clauses of at most three literals after normalization. ][ - _Construction._ Delete tautologies and duplicate literals and clauses, retaining empty clauses. Compact the $l$ occurring variables, recording their original positions. Let $C_1, dots, C_m$ be the remaining clauses, $r_j = |C_j|$, $N = 2m+l+1$, and $D=8^(m+1)$. Let $f_i^+$ and $f_i^-$ be the sums of $8^j$ over clauses containing variable $i$ positively and negatively. Define $N$ integer coefficients and an odd target: + _Construction._ Delete tautologies and duplicate literals and clauses. Compact the $l$ occurring variables, recording their original positions. Let $C_1, dots, C_m$ be the remaining clauses, $r_j = |C_j|$, $N = 2m+l+1$, and $D=8^(m+1)$. Let $f_i^+$ and $f_i^-$ be the sums of $8^j$ over clauses containing variable $i$ positively and negatively. Define $N$ integer coefficients and an odd target: $ c_0=1, quad c_(2j-1)=-8^j/2, quad c_(2j)=-8^j, quad c_(2m+i)=(f_i^+-f_i^-)/2, $ $ tau=1+sum_(j=1)^m (r_j-5)8^j/2. $ Take the first $N$ primes starting at $13$, indexed from zero, and put $q_i=p_i^N$ and $K=product_i q_i$. Let $theta_i$ be the least positive integer satisfying $theta_i equiv c_i mod D$, $theta_i equiv 0 mod (K/q_i)$, and $p_i$ not dividing $theta_i$. CRT gives a residue modulo $D K/q_i$; choosing the first positive representative and, if necessary, adding that modulus once gives $theta_i$. Set $H=sum_i theta_i$ and @@ -12160,7 +12514,7 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Clause encoding._ For signs $alpha_i in {-1,+1}$, put $t_i=(1-alpha_(2m+i))/2$ and $y_j=(3-alpha_(2j-1)-2alpha_(2j))/2 in {0,1,2,3}$. Let $T_j$ count true literals in $C_j$ and $R_j=y_j-T_j+1$. Direct expansion gives $ sum_i c_i alpha_i-tau=alpha_0-1+sum_(j=1)^m R_j 8^j. $ - Here $-2<=R_j<=4$ and $alpha_0-1 in {-2,0}$. The right side has absolute value less than $D$. Taking successive residues modulo eight shows that it vanishes exactly when $alpha_0=1$ and all $R_j=0$. Thus the linear congruence modulo $D$ encodes precisely the satisfying assignments. An empty clause has $T_j=0$ and cannot have $R_j=0$; it requires no exceptional construction. + Here $-2<=R_j<=4$ and $alpha_0-1 in {-2,0}$. The right side has absolute value less than $D$. Taking successive residues modulo eight shows that it vanishes exactly when $alpha_0=1$ and all $R_j=0$. Thus the linear congruence modulo $D$ encodes precisely the satisfying assignments. _Magnitude and square-root lemmas._ Each $theta_i<=2D K/q_i$. For $m>=1$, $N>=2m+1>=3$ and $13^N>4N D$, giving $2H route.json", + "pred reduce x.json --via route.json -o bundle.json", + "pred solve bundle.json --solver ilp", + ) + *Example.* The source selects exactly one of + #decision-ilp-sat.source.instance.inner.variables.len() variables, with objective + coefficients #decision-ilp-sat.source.instance.inner.objective.map(t => str(t.at(1))).join(", ") + and minimization bound #decision-ilp-sat.source.instance.bound. + The CNF has #decision-ilp-sat.target.instance.num_vars variables and + #decision-ilp-sat.target.instance.clauses.len() clauses. Its canonical witness + projects to $(#fmt-values(decision-ilp-sat.solutions.at(0).source_config))$; + both the selected-variable sum and the objective equal the bound. + Lowering the bound to zero makes the instance infeasible: exactly one variable + must be selected, and every objective coefficient is at least one. + ], +)[ + Binary decision ILP reduces to CNF satisfiability by binary addition and + Tseitin gate equivalences, following the adder-based pseudo-Boolean encoding + approach @een2006. The encoding preserves the objective threshold and both + optimization senses; it does not turn an arbitrary feasible assignment into an optimum. +][ + _Construction._ Let $n$ be the number of binary variables and $m$ the number of + constraints. Append the objective comparison as one additional row. Reserve + the first $n$ SAT variables for the source assignment and one false constant $f$. + For a row $sum_i a_i x_i diamond b$, replace each negative term by + $a_i x_i = (-a_i)(1-x_i)+a_i$. The normalized weights are $w_i=abs(a_i)$, + literals are $x_i$ or $not x_i$, and the threshold is + $B=b-sum_(i:a_i<0) a_i$. Set $T=sum_i w_i$. + Rows constant over $[0,T]$ emit either no clauses or an empty clause. + + Otherwise, sum the weighted literals using $W$ bits, where $W$ is the binary + length of $T$. Starting from zero, add each weighted literal with ripple + full-adders: for input bits $a,b$ and carry $d$, compute + $p=a xor b$, output $p xor d$, and carry $(a and b) or (p and d)$. + Every partial sum is at most $T<2^W$, so the last carry can be discarded. + Use equivalence clauses for each AND, OR, and XOR gate; constants may be folded. + Equality asserts each sum bit. For a less-than-or-equal comparison, start + $q="true"$ and scan from least to most significant bit: set + $q=(not s_j or q)$ when $B_j=1$, and $q=(not s_j and q)$ when $B_j=0$. + Assert the final $q$. Greater-than-or-equal complements both $W$-bit operands + before applying the same comparator. + + _Correctness._ ($arrow.r.double$) A feasible source assignment meeting the bound + satisfies every normalized comparison by the signed-term identity. Extend it + with the deterministic gate outputs. Induction over adders gives exact sums; + at each comparator bit, a more significant unequal bit decides the comparison, + while equal bits retain the previous result. Every asserted output is therefore true. + ($arrow.l.double$) A satisfying CNF assignment obeys every gate equivalence and + the false-constant clause, forcing the computed sums and comparisons. The output + assertions imply every source row and its objective bound after reversing normalization. + + _Solution extraction._ Validate the full SAT witness, then convert its first + $n$ bits to integers zero or one. Completed Boolean values map identically. + + _Arithmetic and overhead._ Before encoding, checked sums of positive and negative + coefficients must each fit signed 64-bit arithmetic, including the objective row. + Otherwise the reduction returns a typed overflow error: some binary assignments + would overflow the source evaluator. Normalization uses arbitrary-precision integers. + On the accepted domain $T<=2^64-1$, hence $W<=64$. Each row uses at most $5 n W$ + adder gates, $W$ comparator gates, and $W+1$ assertion clauses; every gate uses + at most four clauses of at most three literals. Including the constant gives + $V<=n+1+64(m+1)(5n+1)$ variables, + $C<=1+(m+1)(1280n+321)$ clauses, and at most $3C$ literal occurrences. +] + #reduction-rule("ILP", "QUBO")[ Binary ILP constraints are encoded by squared integer residuals with binary slack variables, following the penalty construction discussed by Lucas @lucas2014[Section 3]. The rule retains the omitted constant and uses a certified energy interval to recover the original objective direction or report infeasibility. No assumption that the ILP is feasible is needed. ][ @@ -12704,6 +13130,36 @@ where $P$ is a penalty weight large enough that any constraint violation costs m _Overhead._ For $v$ named variables, $t$ expression nodes and $o$ named outputs, the target has at most $v+2t$ variables and $5t+o$ constraints. Non-XOR outputs and empty XOR outputs contribute at most $t$ auxiliaries. Binary XOR steps contribute at most the number of expression-tree edges, hence at most $t$. Base gate rows contribute at most $t$, while input inequalities and binary XOR rows contribute at most four times the number of tree edges. Output equalities add at most $o$ rows. This accounts for arbitrarily many constant inputs: three constants under one XOR use five auxiliaries, exceeding the former one-auxiliary-per-node bound of four. ] +== Conditional Direct QUBO Constructions + +These constructions use the checked sparse penalty and extraction contracts above. Their logical-size advantages are instance-dependent. Every decoder includes target validation, costing $O(N+E)$ in addition to decoding, for $N$ variables and $E$ nonzero terms. Construction costs count arithmetic operations; coefficient bit lengths and sparse-map accumulation also contribute. The scheduling conflict construction follows the time-indexed penalty pattern of #link("https://arxiv.org/abs/1506.08479")[Venturelli et al.]. + +#reduction-rule("SequencingWithReleaseTimesAndDeadlines", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("SequencingWithReleaseTimesAndDeadlines", "DecisionQUBO")], +)[ + Release-time/deadline sequencing reduces to DecisionQUBO on admissible starts, including zero-duration tasks. +][ + _Construction._ First check that $max_i r_i+sum_i p_i$ fits the source integer type, bounding finish additions for every source order. Task $i$ chooses $t=r_i,dots,d_i-p_i$. An impossible window gives an empty row. Add squared one-hot rows and a unit pair penalty whenever neither selected task finishes before the other starts. Store the nonconstant energy with bound equal to the negative omitted constant. + _Correctness._ ($arrow.r.double$) Earliest execution of a feasible source order gives valid choices without conflicts. ($arrow.l.double$) Zero-penalty choices are sorted by start, duration and index, placing zero-duration tasks first at a shared start. Inductively, earliest execution of that order starts no later than each selected start and finishes by its deadline. Source finish additions on recovered witnesses are bounded by these deadlines. Empty rows enforce NO and touching intervals are allowed. + _Extraction and size._ Decode and sort after target validation; completed feasibility maps identically. For $T=max_i d_i$, $S=sum_i max(0,d_i-p_i-r_i+1)<=n w$, where $w<=T+1$ is the largest single start window, with at most $S(S-1)/2$ couplings and $O(S^2)$ candidate pairs. This grid is pseudopolynomial in $T$, and can be much larger than the existing bounded-start route. + + *Example.* #let ex = load-example("SequencingWithReleaseTimesAndDeadlines", "DecisionQUBO") + The canonical source witness #repr(ex.solutions.at(0).source_config) maps to a target with #ex.target.instance.inner.num_vars variables; the exact source and target configurations are shown below. +] + +#reduction-rule("DynamicStorageAllocation", "DecisionQUBO", example: true, + extra: [#direct-qubo-commands("DynamicStorageAllocation", "DecisionQUBO")], +)[ + Dynamic storage allocation gains a direct address-choice DecisionQUBO formulation. +][ + _Construction._ Item $i$, size $s_i$, chooses one address $a=0,dots,D-s_i$ using a squared one-hot row. For items with strictly overlapping lifetimes, penalize each pair of selected address intervals that strictly overlap. All penalties have unit weight; the decision threshold restores the omitted constant to zero. + _Correctness._ ($arrow.r.double$) Every valid allocation selects one address per item and has no conflict. ($arrow.l.double$) A target at the threshold has exactly one address per row, each fitting within memory, and no overlapping addresses for simultaneously live items. Lifetimes or addresses that merely touch incur no conflict. Selected endpoints never exceed $D$, so source address addition is representable. + _Extraction and size._ Validate once and return selected addresses. Completed `Or` maps identically, including NO. Exactly $S=sum_i(D-s_i+1)<=n D$ bits and at most $S(S-1)/2$ couplings; construction enumerates $O(S^2)$ pairs. This is pseudopolynomial in numeric memory capacity, not polynomial in its bit length. + + *Example.* #let ex = load-example("DynamicStorageAllocation", "DecisionQUBO") + The canonical source witness #repr(ex.solutions.at(0).source_config) maps to a target with #ex.target.instance.inner.num_vars variables; the exact source and target configurations are shown below. +] + == Non-Trivial Reductions #let sat_mis = load-example("Satisfiability", "DecisionMaximumIndependentSet") @@ -14486,6 +14942,65 @@ The following reductions to Integer Linear Programming are straightforward formu _Solution extraction._ Direct: $x_i = 1$ iff variable $i$ is true. ] +#let ss_nae = load-example("SetSplitting", "NAESatisfiability") +#let ss_nae_sol = ss_nae.solutions.at(0) +#reduction-rule("SetSplitting", "NAESatisfiability", + example: true, + example-caption: [One NAE clause per subset], + extra: [ + #pred-commands( + "pred create --example " + rule-spec(ss_nae) + " -o set-splitting.json", + "pred reduce set-splitting.json --via route.json -o bundle.json", + "pred solve bundle.json", + "pred evaluate set-splitting.json --config " + cli-config(ss_nae_sol.source_config), + ) + + The canonical source has $#ss_nae.source.instance.universe_size$ elements and + subsets #{ss_nae.source.instance.subsets.map(s => [${#s.map(str).join(", ")}$]).join(", ")}. + It produces $#ss_nae.target.instance.num_vars$ Boolean variables and + $#ss_nae.target.instance.clauses.len()$ NAE clauses. + Under the stored target witness $(#fmt-values(ss_nae_sol.target_config))$, + the subsets have truth values + #{ss_nae.source.instance.subsets.map(s => [$(#fmt-values(s.map(u => ss_nae_sol.target_config.at(u))))$]).join(", ")}. + Each contains both values, so the same vector + $(#fmt-values(ss_nae_sol.source_config))$ is a valid splitting. + ], +)[ + Encode each universe element by a Boolean variable and each subset by its + not-all-equal constraint @schaefer1978. The target has exactly $n$ variables + and $m$ clauses for a source universe of size $n$ with $m$ subset vectors. +][ + _Construction._ For $U = {0, dots, n-1}$, introduce $x_u$ for each $u in U$. + In each subset vector, retain the first occurrence of each distinct element. + If the resulting list is $(u_1, dots, u_k)$ with $k >= 2$, emit the NAE clause + $(x_(u_1), dots, x_(u_k))$. If only one distinct element $u$ remains, emit + $(x_u, x_u)$. Source construction excludes empty subset vectors; an empty + family of subsets produces an empty formula. Unused elements retain their + variables. Positive literal $x_u$ is represented by the signed integer $u+1$; + universes outside the target literal domain return a construction error. + + _Correctness._ ($arrow.r.double$) In a valid splitting, every subset contains + both colors. Removing repeated occurrences preserves these colors, so assigning + each $x_u$ its element's color satisfies every emitted NAE clause. + ($arrow.l.double$) In any satisfying target assignment, every clause has both + truth values. Giving each element its variable's value therefore splits every + source subset. A subset containing only one distinct element is unsplittable; + its repeated-literal clause is unsatisfiable, preserving the equivalence. + + _Parameter bounds._ Each clause uses at most $n$ distinct variables, so the + sum of clause-variable counts is at most $n m$. A clause has at most $2n$ + literal occurrences, including the repeated-literal case. Thus the total + literal count $L$ is at most $2 n m$, and the sum of within-clause literal-pair + counts is at most $L(L-1)/2 <= 2 n m (2 n m + 1)$. For an empty universe, the + accepted family is empty and all these counts are zero. Deduplication by + scanning previously retained elements takes polynomial time in the source + representation length. + + _Solution extraction._ Validate the target witness and return it unchanged. + The assignment to every original element is preserved, with no auxiliary + variables to discard. +] + #reduction-rule("SetSplitting", "ILP")[ Each subset must contain at least one element of each color, encoded as a pair of linear inequalities per subset. ][ @@ -16866,17 +17381,6 @@ Problems parameterized by graph type, weight type, target type, or clause width _Solution extraction._ Return the target configuration unchanged. ] -#reduction-rule("KSatisfiability", "KSatisfiability")[ - A $k$-SAT instance with fixed clause width ($k = 2$ or $k = 3$) converts to generic $k$-SAT by constructing the registered $K_N$ variant. The clauses and variables are preserved verbatim; the target uses `new_allow_less` to accept clauses with fewer than $k$ literals. -][ - _Construction._ Given $"KSat"_(K_j)(n, cal(C))$ with $j in {2, 3}$, construct $"KSat"_(K_N)(n, cal(C))$ with the same $n$ variables and clause set $cal(C)$. - - _Correctness._ Every clause in $cal(C)$ has at most $j$ literals. The $K_N$ variant accepts clauses of any width, so all clauses remain valid. The satisfiability condition (every clause has at least one true literal) is unchanged. - - _Solution extraction._ Return the target configuration unchanged. -] - - // Completeness check: warn about reduction rules in JSON but missing from paper #context { let covered = covered-rules.final() @@ -17446,6 +17950,8 @@ The following table shows concrete target-variable counts for example instances, _Correctness._ ($arrow.r.double$) An exact cover $I$ with $|I| = q$ assigns one worker per selected schedule, covering each period exactly once. ($arrow.l.double$) A feasible assignment with $sum_j w_j = q$ and each period covered exactly once gives pairwise-disjoint schedules covering all of $X$. + _Size._ The budget $q$ has at most $q+1$ magnitude bits; transforms carry no logarithm, so the declared bound is linear in $|X|/3$. + _Solution extraction._ Map $w in NN^m$ to $c in {0,1}^m$ by $c[j] = 1$ if $w[j] > 0$. ] @@ -17479,7 +17985,7 @@ The following table shows concrete target-variable counts for example instances, )[ Use the classical 3-SAT to Vertex Cover gadget construction, then ask whether the resulting graph has a vertex cover of size at most $k = n + 2m$ @garey1979. ][ - _Construction._ Given 3-CNF $phi$ with $n$ variables and $m$ clauses, build the graph $G = (V, E)$ used in the classical 3-SAT $arrow.r$ Minimum Vertex Cover reduction: for each variable $x_i$, add literal vertices $u_i$ and $overline(u)_i$ with one truth-setting edge between them; for each clause $c_j$, add triangle vertices $t^j_0, t^j_1, t^j_2$; for each literal position $(j, r)$, add a communication edge from $t^j_r$ to the literal vertex representing that literal. Assign unit weight to every vertex and set the decision threshold to $k = n + 2m$. For accepted short nonempty clauses, repeat their literals to fill three positions. For an empty clause, keep its triangle without communication edges and use threshold $-1$, making the decision instance infeasible. The vertex count stays exact; the edge count is at most $n+6m$. + _Construction._ Given 3-CNF $phi$ with $n$ variables and $m$ clauses, build the graph $G = (V, E)$ used in the classical 3-SAT $arrow.r$ Minimum Vertex Cover reduction: for each variable $x_i$, add literal vertices $u_i$ and $overline(u)_i$ with one truth-setting edge between them; for each clause $c_j$, add triangle vertices $t^j_0, t^j_1, t^j_2$; for each literal position $(j, r)$, add a communication edge from $t^j_r$ to the literal vertex representing that literal. Assign unit weight to every vertex and set the decision threshold to $k = n + 2m$. The graph has exactly $2n+3m$ vertices and $n+6m$ edges. _Correctness._ ($arrow.r.double$) If $phi$ is satisfiable, choose one literal vertex per variable according to a satisfying assignment and choose two triangle vertices per clause, omitting a vertex whose literal is true. This gives a cover of size $n + 2m$, so the decision instance is yes. ($arrow.l.double$) If the decision instance is yes, any cover of size at most $n + 2m$ must use exactly one literal vertex per variable edge and exactly two vertices per clause triangle. The omitted triangle vertex in each clause has its communication edge covered only by a selected literal vertex, so the corresponding literal is true. These selected literal vertices define a satisfying assignment for $phi$. @@ -17535,14 +18041,14 @@ The following table shows concrete target-variable counts for example instances, Conversely, either equal signal colouring extends: make that colour the cycles $u,v,w,a,b,u$ and $u,v,w,c,d,u$ in the two cliques, and give all remaining edges the other colour. Both cycles agree on the private triangle, and each clique has no monochromatic triangle. No triangle crosses between the two signal edges. - _Construction._ Let the source have $n$ variables and $m$ clauses of length at most three; the typed API also admits shorter clauses. Let $q$ count its length-three clauses. + _Construction._ Let the source have $n$ variables and $m$ clauses, each with three literal positions. - 1. Apply the existing typed embedding into Satisfiability and the existing SAT-to-NAE reduction. It adds a sentinel $s$, replacing each nonempty clause $C$ by $"NAE"(C,s)$ and an empty clause by $"NAE"(s,s)$. - 2. Replace $"NAE"(a,b)$ by $"NAE"(a,b,b)$; keep triples unchanged; replace $"NAE"(a,b,c,d)$ by $"NAE"(a,b,z)$ and $"NAE"(overline(z),c,d)$ with a fresh variable $z$. There are $N=n+1+q$ logical variables and $m+q$ resulting triples. - 3. Give every logical variable $i$ two disjoint signal edges $P_i,M_i$. Their $4N$ vertices are disjoint from all subsequent clause vertices. For each variable include the sign-consistency triple $"NAE"(P_i,P_i,M_i)$, followed by the logical triples, using $P_i$ for a positive literal and $M_i$ for a negative one. There are $T=N+m+q$ triples in total. + 1. Apply the existing typed embedding into Satisfiability and the existing SAT-to-NAE reduction. It adds a sentinel $s$, replacing each clause $C$ by the four-literal $"NAE"(C,s)$. + 2. Replace each $"NAE"(a,b,c,d)$ by $"NAE"(a,b,z)$ and $"NAE"(overline(z),c,d)$ with a fresh variable $z$. There are $N=n+1+m$ logical variables and $2m$ resulting triples. + 3. Give every logical variable $i$ two disjoint signal edges $P_i,M_i$. Their $4N$ vertices are disjoint from all subsequent clause vertices. For each variable include the sign-consistency triple $"NAE"(P_i,P_i,M_i)$, followed by the logical triples, using $P_i$ for a positive literal and $M_i$ for a negative one. There are $T=N+2m$ triples in total. 4. Give every triple its own triangle. Connect its three edges to the three literal signals using three equality senders, each with fresh private vertices. The terminal edges already exist, so a sender adds three vertices and fifteen edges. Repeated literals use separate senders; no endpoint identification or case-specific repair is performed. - _NAE identities._ The length-two identity holds because duplicating a value does not change whether all values agree. For the length-four identity, if $a=b$ the first triple forces $z=overline(a)$; if $c=d$ the second forces $z=c$. These requirements conflict exactly when all four values agree. If either pair differs, its corresponding triple imposes no condition on $z$. This proves the identity in both directions for all input patterns. + _NAE identity._ For the length-four identity, if $a=b$ the first triple forces $z=overline(a)$; if $c=d$ the second forces $z=c$. These requirements conflict exactly when all four values agree. If either pair differs, its corresponding triple imposes no condition on $z$. This proves the identity in both directions for all input patterns. _Triangle isolation._ Private vertices from different senders are nonadjacent. Any triangle containing a private sender vertex must lie in that sender: both other vertices belong to it, and the only edges among its four boundary vertices are its two terminal edges. This remains true after assembly because all variable signals and clause triangles have disjoint vertex sets, and senders add no boundary-to-boundary edges. A triangle containing no sender-private vertex is one of the clause triangles. Hence the target contains exactly the intended clause triangles and the nineteen triangles inside each sender, even with repeated or complementary literals and repeated variable occurrences. @@ -17552,7 +18058,7 @@ The following table shows concrete target-variable counts for example instances, _Solution extraction._ Validate the target colouring and read the positive signal colours for the original variables and sentinel. Pass this assignment to the existing SAT-to-NAE extraction API. A global colour swap leaves the normalized source assignment unchanged. - _Overhead._ The exact counts are $4N+12T$ vertices, $2N+48T$ edges and $58T$ triangles. Since $q<=m$, these are bounded by $16n+40m+16$, $50n+146m+50$ and $58n+174m+58$, respectively. All graph-size arithmetic is checked before allocation. With exactly three literals per clause the bounds are equalities. + _Overhead._ The exact counts are $4N+12T$ vertices, $2N+48T$ edges and $58T$ triangles. Substituting $N=n+1+m$ and $T=n+1+3m$ gives exactly $16n+40m+16$, $50n+146m+50$ and $58n+174m+58$, respectively. All graph-size arithmetic is checked before allocation. With exactly three literals per clause the bounds are equalities. _YES example._ For the clause $(x_1 or x_2 or x_3)$, choose values $(1,0,0)$, sentinel $0$ and splitting variable $0$. Both logical triples evaluate to $"NAE"(1,0,0)$. Here $N=5$, $T=7$, giving 104 vertices, 346 edges and 406 triangles. The signal colours extend by the sender construction. @@ -17594,16 +18100,16 @@ The following table shows concrete target-variable counts for example instances, )[ Schaefer's Lemma 3.5 @schaefer1978 expresses a three-input disjunction by five exact-one constraints. The implementation compacts the $a$ appearing source variables, adds two global constant variables and six auxiliaries per clause. A source with $m$ clauses produces $a + 2 + 6m$ target variables and $1 + 5m$ target clauses, bounded by $n + 2 + 6m$ and $1 + 5m$ in the declared source parameters. ][ - _Construction._ Let $J$ be the sorted original indices of the appearing variables. Replace each actual source literal by the corresponding compact variable with its sign preserved. Use the existing SAT variable allocator to allocate $z_0$ and $z_T$, followed by six fresh variables $a_j, b_j, c_j, d_j, e_j, f_j$ for each source clause. The global exact-one constraint $R(z_0,z_0,z_T)$ forces $(z_0,z_T)=(0,1)$. Each native source clause has zero through three positions; fill missing positions with $z_0$. This preserves its disjunction, including the empty clause's false value. For the resulting three literals $ell_1^j,ell_2^j,ell_3^j$, append + _Construction._ Let $J$ be the sorted original indices of the appearing variables. Replace each actual source literal by the corresponding compact variable with its sign preserved. Use the existing SAT variable allocator to allocate $z_0$ and $z_T$, followed by six fresh variables $a_j, b_j, c_j, d_j, e_j, f_j$ for each source clause. The global exact-one constraint $R(z_0,z_0,z_T)$ forces $(z_0,z_T)=(0,1)$. For each clause's three literals $ell_1^j,ell_2^j,ell_3^j$, append $ R(ell_1^j,a_j,d_j), quad R(ell_2^j,b_j,d_j), quad R(a_j,b_j,e_j), quad R(c_j,d_j,f_j), quad R(ell_3^j,c_j,z_0). $ Here $R$ counts literal occurrences, so its repeated $z_0$ in the global constraint is intentional. Negative literals remain permitted by the target model. Every clause uses this same construction; no empty-clause target case is needed. - _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, assign its appearing coordinates to the compact target variables and set the constants as above. Let $(x,y,z)$ be one padded clause's literal truth values. Set $d=(1-x)(1-y)$, $a=1-x-d$, $b=1-y-d$, $c=1-z$, $e=1-a-b$ and $f=z-d$. If $x=y=0$, satisfaction forces $z=1$, giving $(a,b,c,d,e,f)=(0,0,0,1,1,0)$. Otherwise $d=0$, $a=1-x$, $b=1-y$, $e=x+y-1$, and $f=z$; these and $c=1-z$ are Boolean because $x+y>=1$. Substitution gives $x+a+d=y+b+d=a+b+e=c+d+f=z+c=1$, satisfying all five constraints. Auxiliary variables are disjoint across clauses, so the assignments combine. + _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, assign its appearing coordinates to the compact target variables and set the constants as above. Let $(x,y,z)$ be one source clause's literal truth values. Set $d=(1-x)(1-y)$, $a=1-x-d$, $b=1-y-d$, $c=1-z$, $e=1-a-b$ and $f=z-d$. If $x=y=0$, satisfaction forces $z=1$, giving $(a,b,c,d,e,f)=(0,0,0,1,1,0)$. Otherwise $d=0$, $a=1-x$, $b=1-y$, $e=x+y-1$, and $f=z$; these and $c=1-z$ are Boolean because $x+y>=1$. Substitution gives $x+a+d=y+b+d=a+b+e=c+d+f=z+c=1$, satisfying all five constraints. Auxiliary variables are disjoint across clauses, so the assignments combine. - ($arrow.l.double$) Every target solution forces $z_0=0$. If a padded clause had $x=y=z=0$, the final constraint would force $c=1$; the fourth would then force $d=f=0$. The first two would force $a=b=1$, contradicting the third. Thus every padded disjunction is true, which implies every original clause is true. Repetition, opposite signs and missing positions do not change this argument. + ($arrow.l.double$) Every target solution forces $z_0=0$. If a source clause had $x=y=z=0$, the final constraint would force $c=1$; the fourth would then force $d=f=0$. The first two would force $a=b=1$, contradicting the third. Thus every source clause is true. Repeated literals and opposite signs do not change this argument. _Solution extraction._ Validate the target assignment once using the formal evaluator and reject $"Or(false)"$. Initialize a length-$n$ false vector, then restore the compact source coordinates to their original positions in $J$. Unused source variables stay false. The resolved value types are $"Or" arrow.r "Or"$. @@ -17647,9 +18153,9 @@ The following table shows concrete target-variable counts for example instances, #reduction-rule("KSatisfiability", "FeasibleRegisterAssignment", example: false, )[ - Sethi's Reduction 3 @sethi1973 builds a DAG with shared-register variable leaf pairs and $p\/q\/r\/overline(r)$ clause gadgets. Nonempty short clauses are padded by repeating a literal; occurring variables are compacted. For $s$ declared source variables and $c$ clauses, the target has at most $2s+12c$ vertices, $15c$ arcs, $s+9c$ registers, and $s+3c$ pairs of vertices sharing a register. + Sethi's Reduction 3 @sethi1973 builds a DAG with shared-register variable leaf pairs and $p\/q\/r\/overline(r)$ clause gadgets. Occurring variables are compacted. For $s$ declared source variables and $c$ clauses, the target has at most $2s+12c$ vertices, $15c$ arcs, $s+9c$ registers, and $s+3c$ pairs of vertices sharing a register. ][ - _Native normalization._ If any clause is empty, return the three-vertex DAG with dependencies $(2,0),(2,1)$ and register assignment $(0,0,1)$. Both predecessors must stay live until vertex 2, so neither can overwrite the other's register; this target is infeasible. Otherwise collect appearing source indices in increasing order and store their inverse map. Pad each nonempty clause to three literal occurrences by repeating its first literal. Repetition preserves a disjunction, and each occurrence has its own gadget and register pair, so no distinct-variable assumption is needed. An empty conjunction yields the empty DAG and empty realization. + _Native normalization._ Collect appearing source indices in increasing order and store their inverse map. Each of the three literal occurrences of a clause, including repeated literals, has its own gadget and register pair, so no distinct-variable assumption is needed. An empty conjunction yields the empty DAG and empty realization. _Construction._ Let $a$ be the number of appearing variables. For each compact variable $x_k$, create leaves $s_k^+,s_k^-$ sharing register $S_k$. For every clause position $(i,j)$ create $p_(i,j),q_(i,j),r_(i,j),overline(r)_(i,j)$. The $p$ and $q$ registers are unique, while $r$ and $overline(r)$ share a fresh register $R_(i,j)$. Arcs point from a consumer to its dependency: $q_(i,j) -> p_(i,j) -> r_(i,j)$ and $q_(i,j) -> overline(r)_(i,j+1)$, with positions cyclic modulo three. For positive literal $x_k$, add $r_(i,j) -> s_k^+$ and $overline(r)_(i,j) -> s_k^-$; reverse these attachments for a negative literal. This DAG has four levels: leaves, $r/overline(r)$, $p$, and $q$. @@ -17659,7 +18165,7 @@ The following table shows concrete target-variable counts for example instances, _Extraction._ Validate the complete position vector and reject $"Or(false)"$. Set each appearing source variable true iff its compact positive leaf occurs before its negative leaf. Restore original indices through the inverse map and assign false to unused variables. The target model's permitted last-use overwrite does not weaken the order-transfer proof: neither member of a shared pair is the other member's consumer in this construction. - _Bounds and native arithmetic._ For the ordinary construction $a <= min(s,3c)$, so the displayed upper bounds follow from the exact counts $2a+12c$, $15c$, $a+9c$, and $a+3c$. The fixed NO target has counts $(3,2,2,1)$ and also satisfies the bounds whenever an empty clause exists; the empty YES target has all counts zero. Let $I="isize::MAX"$. A native source clause stores a vector object of 24 bytes on 64-bit or 12 bytes on 32-bit, so successful allocation of its outer vector bounds $c$ by $I/24$ or $I/12$. Therefore $2a+12c <= 18c$, $a+9c <= 12c$, and $15c$ fit $"usize"$ before target allocation on both architectures. Once the target register-assignment vector is allocated, every indexed vertex is within that vector. All same-register groups have size two except the fixed target's singleton, so pair counting introduces no large product. Checked construction arithmetic is retained; allocation and solver limits are not infeasibility proofs. + _Bounds and native arithmetic._ For the ordinary construction $a <= min(s,3c)$, so the displayed upper bounds follow from the exact counts $2a+12c$, $15c$, $a+9c$, and $a+3c$. The empty YES target has all counts zero. Let $I="isize::MAX"$. A native source clause stores a vector object of 24 bytes on 64-bit or 12 bytes on 32-bit, so successful allocation of its outer vector bounds $c$ by $I/24$ or $I/12$. Therefore $2a+12c <= 18c$, $a+9c <= 12c$, and $15c$ fit $"usize"$ before target allocation on both architectures. Once the target register-assignment vector is allocated, every indexed vertex is within that vector. All same-register groups have size two, so pair counting introduces no large product. Checked construction arithmetic is retained; allocation and solver limits are not infeasibility proofs. ] #let ksat_rs = load-example("KSatisfiability", "RegisterSufficiency") @@ -17684,9 +18190,9 @@ The following table shows concrete target-variable counts for example instances, *Multiplicity:* The fixture stores one canonical satisfying assignment. Different satisfying assignments can induce different valid computation orders in the target DAG. ], )[ - Sethi's Reduction 1 and Theorem 3.11 @sethi1973 encode literal choices through register pressure. We extend the construction to the native zero-to-three-literal clause domain by truth-preserving normalization and explicit empty-formula boundaries. The original padding $b=max(2n-m,0)$ is retained. + Sethi's Reduction 1 and Theorem 3.11 @sethi1973 encode literal choices through register pressure. The native source has exactly three literals per clause, with repeated literals permitted. We compact appearing variables and handle the empty formula explicitly. The original padding $b=max(2n-m,0)$ is retained. ][ - _Normalization._ A formula containing an empty clause is false; output a single output vertex with register bound zero. An empty conjunction is true; output the empty graph with bound zero. In every other case collect the appearing variables in increasing original-index order, map them to $1,dots,n$, and retain the inverse map. Keep the original clause order and literal occurrences. Repeat the first literal of each nonempty short clause until it has three positions. This preserves disjunction truth, gives $n,m>=1$, and never introduces a fictitious vertex for a missing literal. Let $Y_(i,j)$ denote the literal at position $j$ of clause $i$, allowing repeated literals. + _Normalization._ An empty conjunction is true; output the empty graph with bound zero. Otherwise collect the appearing variables in increasing original-index order, map them to $1,dots,n$, and retain the inverse map. Keep the original clause order and literal occurrences, which gives $n,m>=1$. Let $Y_(i,j)$ denote the literal at position $j$ of clause $i$, allowing repeated literals. _DAG construction._ Put $b=max(2n-m,0)$ and $K=3m+4n+1+b$. Arcs $(v,u)$ mean that $v$ depends on $u$. Create the following disjoint families, with one-based subscripts: $ |A|=2n+1, quad |B|=b, quad |C|=m, quad F={f_(i,j):1<=i<=m,1<=j<=3}, $ @@ -17848,13 +18354,13 @@ The following table shows concrete target-variable counts for example instances, *Multiplicity:* The fixture stores one canonical witness. The formula has multiple satisfying assignments; each induces at least one $k$-clique by choosing one true literal per clause. ], )[ - Karp's literal-compatibility construction @karp1972 is extended with an anchor and, when needed, isolated padding. This keeps the same endpoint and handles both empty formulas and the shorter clauses accepted by the native `new_allow_less` API. + Karp's literal-compatibility construction @karp1972 is extended with an anchor vertex, so the empty formula maps to a one-vertex clique instance. ][ - _Construction._ Let $m$ be the clause count and $t=sum_j |C_j|$ the actual occurrence count. Number literal vertices in clause/position order, with stored variable indices and polarities. Set $N=max(t,m)+1$, $k=m+1$, and anchor $a=t$. Connect two literal vertices iff they come from different clauses and are not opposite polarities of the same variable; then connect $a$ to all literal vertices. Any remaining vertices are isolated. Thus $1<=k<=N$, $N<=3m+1$, and the edge count is at most $9m^2+3m$. + _Construction._ Let $m$ be the clause count. Number the $3m$ literal occurrences in clause/position order, with stored variable indices and polarities. Set $N=3m+1$, $k=m+1$, and anchor $a=3m$. Connect two literal vertices iff they come from different clauses and are not opposite polarities of the same variable; then connect $a$ to all literal vertices. Thus $1<=k<=N$ and the edge count is at most $9m^2+3m$. - _Correctness._ A satisfying assignment selects a true occurrence from each clause; these mutually compatible vertices and the anchor form a $k$-clique. Conversely, the literal subgraph contains at most one vertex per clause in a clique, hence has clique number at most $m$. For $m>0$, any clique of size at least $k>=2$ excludes padding isolates and must contain the anchor plus one occurrence from every clause. Their polarities consistently satisfy all clauses. An empty clause prevents such a clique. For $m=0$, the target is a single anchor with $k=1$, and every source assignment satisfies the empty conjunction. + _Correctness._ A satisfying assignment selects a true occurrence from each clause; these mutually compatible vertices and the anchor form a $k$-clique. Conversely, the literal subgraph contains at most one vertex per clause in a clique, hence has clique number at most $m$. For $m>0$, any clique of size at least $k>=2$ must contain the anchor plus one occurrence from every clause. Their polarities consistently satisfy all clauses. For $m=0$, the target is a single anchor with $k=1$, and every source assignment satisfies the empty conjunction. - _Solution extraction._ Validate the complete target selection and its true clique predicate first. Decode the literal vertices via their stored source indices and signs, leaving unselected variables false; ignore the nonliteral anchor and padding by the defined mapping. Checked occurrence and output counts precede allocation. Formal `CNFClause::variables` supplies validated indices. Normal CLI/serde still requires exactly three literals per actual clause; native short-clause support does not change variants or serialization. + _Solution extraction._ Validate the complete target selection and its true clique predicate first. Decode the literal vertices via their stored source indices and signs, leaving unselected variables false; ignore the anchor by the defined mapping. Checked vertex and output counts precede allocation. Formal `CNFClause::variables` supplies validated indices. ] #let ksat_co = load-example("KSatisfiability", "CyclicOrdering") @@ -17883,7 +18389,7 @@ The following table shows concrete target-variable counts for example instances, )[ This reduction @galilMegiddo1977 first normalizes clauses to three distinct, globally ordered variables. With $s$ declared source variables and $c$ source clauses it produces at most $3s + 26c + 3$ elements and $40c + 2$ cyclic-order constraints. The original ten-constraint gadget is applied to the normalized formula. ][ - _Normalization._ An empty clause maps to the fixed NO target on three elements with constraints $(0,1,2)$ and $(0,2,1)$. Otherwise remove repeated literals within each clause and discard clauses containing both signs of a variable. Compact the remaining appearing variables in increasing original-index order, retaining the inverse map. Replace a two-literal clause $(a or b)$ by $(a or b or u) and (a or b or not u)$ with fresh $u$. Replace a unit clause $a$ by the four clauses $(a or (plus.minus u) or (plus.minus v))$ over both independent signs, with fresh $u,v$. These conjunctions are true for every auxiliary assignment when the original clause is true and false for at least one constituent clause under every auxiliary assignment when the original clause is false. Every resulting clause has three distinct variables; order its literals by increasing variable index. If no clauses remain, use the one-element unconstrained YES target. + _Normalization._ Remove repeated literals within each clause and discard clauses containing both signs of a variable. Compact the remaining appearing variables in increasing original-index order, retaining the inverse map. Replace a two-literal clause $(a or b)$ by $(a or b or u) and (a or b or not u)$ with fresh $u$. Replace a unit clause $a$ by the four clauses $(a or (plus.minus u) or (plus.minus v))$ over both independent signs, with fresh $u,v$. These conjunctions are true for every auxiliary assignment when the original clause is true and false for at least one constituent clause under every auxiliary assignment when the original clause is false. Every resulting clause has three distinct variables; order its literals by increasing variable index. If no clauses remain, use the one-element unconstrained YES target. _Construction._ Let the normalized formula have $N$ variables and $M$ clauses. For each variable $x_i$, create three target elements $alpha_i, beta_i, gamma_i$. A positive literal has associated triple $(alpha_i,beta_i,gamma_i)$; a negative literal has $(alpha_i,gamma_i,beta_i)$. For each normalized clause, let its three literal triples be $(a,b,c)$, $(d,e,f)$, $(g,h,i)$ in increasing variable order. Add five fresh elements $j,k,l,m,n$ and the ten constraints $ @@ -17943,7 +18449,7 @@ The following table shows concrete target-variable counts for example instances, )[ Ullman's reduction first builds a variable-capacity unit-task scheduling instance for 3-SAT, then pads each time slot with chained filler jobs so a fixed number of processors simulates the desired capacity profile. Because every task has length $1$, preemption is irrelevant: the resulting instance is already a valid preemptive scheduling instance whose optimal makespan is at most $T = n + 3$ iff the formula is satisfiable @ullman1975 @garey1979. ][ - Short nonempty clauses are padded by repeating literals. An empty conjunction maps to one unit task with threshold 1; a formula containing an empty clause maps to the same task with threshold 0. The following construction handles the remaining instances. + An empty conjunction maps to one unit task with threshold 1. The following construction handles the remaining instances. _Construction._ Let $phi$ be a 3-CNF formula with variables $x_1, dots, x_n$ and clauses $C_1, dots, C_m$. Create unit jobs $x_(i,j)$ and $overline(x)_(i,j)$ for $1 <= i <= n$ and $0 <= j <= n$, plus forcing jobs $y_i, overline(y)_i$, and clause jobs $D_(r,s)$ for $1 <= r <= m$, $1 <= s <= 7$. Add chain precedences $x_(i,j) prec x_(i,j+1)$ and $overline(x)_(i,j) prec overline(x)_(i,j+1)$, and branching precedences $x_(i,i-1) prec y_i$, $overline(x)_(i,i-1) prec overline(y)_i$. Set $T = n + 3$ and slot capacities $c_0 = n$, $c_1 = 2n + 1$, $c_t = 2n + 2$ for $2 <= t <= n$, $c_(n+1) = m + n + 1$, and $c_(n+2) = 6m$. For each clause $C_r = (ell_1 or ell_2 or ell_3)$ and each nonzero bit pattern $b in {1, dots, 7}$, create clause job $D_(r,b)$. Its predecessors are the three chain endpoints chosen according to the bits of $b$: for literal position $k$, use the endpoint of $ell_k$ when bit $k$ is 1 and of $not ell_k$ when bit $k$ is 0. This makes exactly one clause job per clause ready one slot earlier when the clause is satisfied. @@ -18026,7 +18532,7 @@ The following table shows concrete target-variable counts for example instances, _Solution extraction._ Validate the target partition, select precisely those vertex items sharing the label of $s$, and invoke the formal clique-to-SAT extractor. This mapping is independent of the numerical names of partition blocks. - _Overhead._ There are exactly $h+e+2$ vertices and $2h+4e$ arcs. With $m$ source clauses, $h<=3m+1$ and $e<=9m(m-1)/2+3m$, including native short or empty clauses. Thus target sizes are at most $(9m^2+3m+6)/2$ vertices and $18m^2+2$ arcs. The construction checks representability of counts and signed integer coefficients before allocating its incidence graph. + _Overhead._ There are exactly $h+e+2$ vertices and $2h+4e$ arcs. With $m$ source clauses, $h<=3m+1$ and $e<=9m(m-1)/2+3m$. Thus target sizes are at most $(9m^2+3m+6)/2$ vertices and $18m^2+2$ arcs. The construction checks representability of counts and signed integer coefficients before allocating its incidence graph. ] #let hc_bicon = load-example("HamiltonianCircuit", "BiconnectivityAugmentation") @@ -18553,7 +19059,7 @@ The following table shows concrete target-variable counts for example instances, #reduction-rule("KSatisfiability", "BicliqueCover")[ Polynomial reduction (Chandran, Issac, and Karrenbauer, IPEC 2016 @chandran_et_al:LIPIcs.IPEC.2016.11) from 3-SAT to BicliqueCover with logarithmic rank. Each appearing source variable is split into a positive/negative pair $(t_i, f_i)$, exactly-one clauses tie them to opposite truth values, and the formula is padded so that $n = 2^ell$ normalized variables admit a balanced satisfying assignment with exactly $n / 2$ true variables. The construction then assembles a bipartite gadget whose biclique cover rank equals $k_f + 2 ell + 2$ iff the (normalized) formula is satisfiable. ][ - _Construction._ Let $psi$ have $n_s$ declared variables and $m_s$ clauses. The native Rust API also permits clauses of at most three literals. An empty clause maps to a single-edge, rank-zero NO target. A formula with no clauses maps to an empty, rank-zero YES target. Otherwise compact the $a$ variables that actually appear, recording their original indices, and repeat one literal in each nonempty short clause to obtain exactly three positions. Repetition preserves disjunction, and absent variables may be assigned false in the inverse map. *Normalize* this compact formula: + _Construction._ Let $psi$ have $n_s$ declared variables and $m_s$ three-literal clauses. A formula with no clauses maps to an empty, rank-zero YES target. Otherwise compact the $a$ variables that actually appear, recording their original indices; absent variables may be assigned false in the inverse map. *Normalize* this compact formula: $ "vars:" quad & "introduce" t_i, f_i "for each appearing" x_i "and pad to" n = 2^ell "variables" \ "clauses:" quad & "replace literal" x_i "by" t_i ";" not x_i "by" f_i \ @@ -18728,15 +19234,15 @@ The following table shows concrete target-variable counts for example instances, )[ This reduction uses variable digons and clause three-cycles, following the kernel hardness approach of @chvatal1973. With $a$ appearing variables, $m$ clauses and $L$ literal occurrences, the target has $2a + 3m$ vertices and $2a + 3m + L$ arcs. These are bounded by $2n + 3m$ and $2n + 6m$ on the native source domain. Each occurrence has its own clause vertex; kernels may include clause vertices as well as literals. ][ - _Construction._ Collect the sorted original indices $J$ of appearing variables, with $a = |J|$. For each compact variable $i$, create literal vertices $p_i, n_i$ and both digon arcs. Each native clause has zero through three literals. Create three vertices $c_(j,0), c_(j,1), c_(j,2)$ and the directed cycle in that order, then add $(c_(j,t), v(ell_(j,t)))$ only for its actual literal positions. Repeated literals keep separate occurrence vertices. An empty clause therefore produces a three-cycle with no outgoing literal arcs, which has no kernel; an empty formula produces an empty graph, whose empty selection is a kernel. No padding is needed. + _Construction._ Collect the sorted original indices $J$ of appearing variables, with $a = |J|$. For each compact variable $i$, create literal vertices $p_i, n_i$ and both digon arcs. For each clause create three vertices $c_(j,0), c_(j,1), c_(j,2)$ and the directed cycle in that order, then add $(c_(j,t), v(ell_(j,t)))$ for its three literal positions. Repeated literals keep separate occurrence vertices. An empty formula produces an empty graph, whose empty selection is a kernel. - _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, choose its true literal in each digon. Let $t_r$ indicate whether the literal at clause position $r$ is selected, with missing positions set to false. Select clause vertex $r$ exactly when $not t_r and t_((r+1) mod 3)$. A selected vertex points to no selected literal, and its successor cannot be selected, so independence holds. An unselected vertex with $t_r$ true is absorbed through its literal arc. Otherwise both $t_r$ and $t_((r+1) mod 3)$ are false. Since the clause is satisfied, $t_((r+2) mod 3)$ is true; its cycle successor is therefore selected and absorbs it. Unselected literal vertices are absorbed by their digon partners. + _Correctness._ ($arrow.r.double$) Given a satisfying source assignment, choose its true literal in each digon. Let $t_r$ indicate whether the literal at clause position $r$ is selected. Select clause vertex $r$ exactly when $not t_r and t_((r+1) mod 3)$. A selected vertex points to no selected literal, and its successor cannot be selected, so independence holds. An unselected vertex with $t_r$ true is absorbed through its literal arc. Otherwise both $t_r$ and $t_((r+1) mod 3)$ are false. Since the clause is satisfied, $t_((r+2) mod 3)$ is true; its cycle successor is therefore selected and absorbs it. Unselected literal vertices are absorbed by their digon partners. - ($arrow.l.double$) Each literal vertex has only its digon partner as an outgoing neighbor. Independence and absorption force exactly one selected endpoint per variable. If a clause has no selected literal, absorption must occur entirely within its directed three-cycle. Independence permits at most one selected cycle vertex, which cannot absorb both others. This contradiction proves that every clause is satisfied, including the native short-clause semantics. This proof does not require distinct variables or a particular literal order. + ($arrow.l.double$) Each literal vertex has only its digon partner as an outgoing neighbor. Independence and absorption force exactly one selected endpoint per variable. If a clause has no selected literal, absorption must occur entirely within its directed three-cycle. Independence permits at most one selected cycle vertex, which cannot absorb both others. This contradiction proves that every clause is satisfied. This proof does not require distinct variables or a particular literal order. _Solution extraction._ Validate the target selection once using the formal target evaluator and reject $"Or(false)"$. Initialize a length-$n$ false vector and restore each original position $J_i$ from the selection of $p_i$. Unused variables remain false; selected clause vertices are ignored. The concrete value types are $"Or" arrow.r "Or"$. - _Bounds and native arithmetic._ Since $a <= L <= 3m$, the target has at most $9m$ vertices and $12m$ arcs. The registered relations use upper bounds in the declared source parameters, covering sparse variables and short clauses. Counts are checked before allocation, and every vertex index is bounded by the checked total. A successfully allocated native clause vector also bounds $m$ by its element layout and the address space; original sparse indices are never doubled. Allocation limits do not represent mathematical infeasibility. + _Bounds and native arithmetic._ Since $a <= L <= 3m$, the target has at most $9m$ vertices and $12m$ arcs. The registered relations use upper bounds in the declared source parameters, covering sparse variables. Counts are checked before allocation, and every vertex index is bounded by the checked total. A successfully allocated native clause vector also bounds $m$ by its element layout and the address space; original sparse indices are never doubled. Allocation limits do not represent mathematical infeasibility. ] @@ -19025,6 +19531,8 @@ The following table shows concrete target-variable counts for example instances, _Size bound._ There are $sum_(i=1)^n (p_i-2)+m$ forbidden pairs, where $p_i$ is the $i$th odd prime. For the ordinary $k$th prime $q_k$, the standard estimate $q_k < k(ln k+ln ln k)$ for $k >= 6$ @axler2019, together with the first five primes, implies $q_k <= 2k^2$ for every $k >= 1$. Consequently $p_i=q_(i+1) <= 2(n+1)^2$ and $2n(n+1)^2+m$ bounds the pair count. + Every clause modulus divides $product_(i=1)^n p_i$, and every variable prime occurs as a modulus, so the target period is $L = product_(i=1)^n p_i$. Since $n+1 <= 2^n$, we have $p_i <= 2(n+1)^2 <= 2^(2n+1)$ and hence `lcm_bits` $<= n(2n+1)+1$. For $n=0$, the empty product is 1 and its bit length is 1. Thus the reduction has polynomial parameter growth while exhaustive target solving still has an exponential bound. + _Correctness._ ($arrow.r.double$) A satisfying assignment $tau$ defines residues $r_i in {1,2}$ per variable. By CRT, some integer $x$ has these residues. It avoids all variable-forbidden classes and all clause-forbidden classes (since at least one literal is true, the residue triple differs from the falsifying triple). ($arrow.l.double$) Any feasible $x$ has $x mod p_i in {1,2}$ for all $i$. Define $tau(x_i) = "TRUE"$ if residue 1, FALSE if 2. If a clause were false, $x$ would match its forbidden CRT class -- contradiction. _Solution extraction._ Set $tau(x_i) = "TRUE"$ if $x mod p_i = 1$, FALSE if $x mod p_i = 2$. @@ -19453,6 +19961,8 @@ The following table shows concrete target-variable counts for example instances, _Correctness._ ($arrow.r.double$) A valid 3-partition fills each slot of width $B$ with exactly 3 elements; fillers are placed in their tight windows. ($arrow.l.double$) Fillers pinned to unit windows create $m$ slots of width $B$; total element work $m B$ fills all slots exactly; size constraints force 3 elements per slot. + _Size._ Every release time and deadline lies in $[0, m(B+1)-1]$, so no task has more than $m(B+1)$ start times. + _Solution extraction._ Decode the Lehmer code, simulate the schedule tracking start times; assign elements to groups by $floor("start" / (B+1))$. ] @@ -19529,15 +20039,13 @@ The following table shows concrete target-variable counts for example instances, *Multiplicity:* The fixture stores one canonical witness. The form is invariant under $f arrow.r -f$, so the complementary assignment $(-1, +1, -1, +1)$ (config $(0, 1, 0, 1)$) is equally optimal. ], )[ - @garey1979 (MS13) The construction takes $A$ to be the weighted adjacency matrix of $G$. The identity $sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 dot "cut"(S)$ — where $S = {i : f(i) = +1\}$ and $W = sum_(e in E) w(e)$ — converts MaxCut maximization into MinimumMatrixCover minimization with $O(n^2)$ overhead. + @garey1979 (MS13) The construction takes $A$ to be the weighted adjacency matrix of $G$. The identity $sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 dot "cut"(S)$ — where $S = {i : f(i) = +1\}$ and $W = sum_(e in E) w(e)$ — converts MaxCut maximization into MinimumMatrixCover minimization with $O(n^2)$ overhead for nonnegative weights. Each negative edge first becomes a two-edge gadget through one auxiliary vertex, giving $O((n + |E|)^2)$ overhead. ][ - _Construction._ Given a MaxCut instance $(G, w)$ with $G = (V, E)$, $|V| = n$, and nonnegative integer edge weights $w$, build the $n times n$ matrix $A$ with $a_(i j) = w(\{i, j\})$ for $\{i, j\} in E$, $a_(i j) = 0$ otherwise, and $a_(i i) = 0$. $A$ is symmetric, zero-diagonal, and nonnegative, hence a valid MinimumMatrixCover instance. - - _Correctness._ For any $f in \{-1, +1\}^n$ with $S = \{i : f(i) = +1\}$, each edge $\{i, j\} in E$ appears twice in $sum_(i, j) a_(i j) f(i) f(j)$. A non-cut edge contributes $+2 w(\{i, j\})$ (same signs, $f(i) f(j) = +1$); a cut edge contributes $-2 w(\{i, j\})$. Summing yields $sum_(i, j) a_(i j) f(i) f(j) = 2 (W - "cut"(S)) - 2 "cut"(S) = 2 W - 4 "cut"(S)$. Since $2 W$ is a constant, $min_f sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 max_S "cut"(S)$, so the two problems share the same optimal partitions. ($arrow.r.double$) A maximum cut $S^*$ defines $f^*$ minimizing the quadratic form. ($arrow.l.double$) A minimizing $f^*$ defines $S^* = \{i : f^*(i) = +1\}$ achieving the maximum cut. + _Construction._ Given a MaxCut instance $(G, w)$ with $G = (V, E)$ and $|V| = n$, first remove negative weights. Replace each edge $\{u, v\}$ with $w(\{u, v\}) < 0$ by a fresh vertex $t$ and edges $\{t, v\}$ of weight $|w| + 1$ and $\{t, u\}$ of weight $|w|$. The resulting graph $G'$ has $n' <= n + |E|$ vertices and nonnegative weights $w'$. Build the $n' times n'$ matrix $A$ with $a_(i j) = w'(\{i, j\})$ for edges of $G'$, $a_(i j) = 0$ otherwise, and $a_(i i) = 0$. $A$ is symmetric, zero-diagonal, and nonnegative, hence a valid MinimumMatrixCover instance. - _Precondition._ Nonnegative edge weights. Negative-weight MaxCut instances are out of scope; a separate weight-shifting reduction would be required. + _Correctness._ For any $f in \{-1, +1\}^n$ with $S = \{i : f(i) = +1\}$, each edge $\{i, j\} in E$ appears twice in $sum_(i, j) a_(i j) f(i) f(j)$. A non-cut edge contributes $+2 w(\{i, j\})$ (same signs, $f(i) f(j) = +1$); a cut edge contributes $-2 w(\{i, j\})$. Summing yields $sum_(i, j) a_(i j) f(i) f(j) = 2 (W - "cut"(S)) - 2 "cut"(S) = 2 W - 4 "cut"(S)$. Since $2 W$ is a constant, $min_f sum_(i, j) a_(i j) f(i) f(j) = 2 W - 4 max_S "cut"(S)$ on $G'$. Each gadget preserves maximum cuts: moving $t$ to the side opposite $v$ gains $|w| + 1$ and loses at most $|w|$, so every maximum cut of $G'$ separates $t$ from $v$. Then $\{t, u\}$ is cut exactly when $u$ and $v$ share a side, and $|w| dot [u, v "together"] = w dot [u, v "cut"] + |w|$. Each gadget therefore adds the constant $2|w| + 1$, and maximum cuts of $G'$ restrict to maximum cuts of $G$; every maximum cut of $G$ extends to one of $G'$. Hence the two problems share the same optimal partitions on $V$. ($arrow.r.double$) A maximum cut $S^*$ defines $f^*$ minimizing the quadratic form. ($arrow.l.double$) A minimizing $f^*$ defines $S^* = \{i : f^*(i) = +1\}$ achieving the maximum cut. - _Solution extraction._ Both encodings agree that $"config"[i] = 1$ means vertex $i in S$, so extraction is the identity. The complementary witness $f arrow.r -f$ is equally optimal because the quadratic form is invariant under this sign flip. + _Solution extraction._ Both encodings agree that $"config"[i] = 1$ means vertex $i in S$, so extraction keeps the original vertices' bits and drops the auxiliary ones. The complementary witness $f arrow.r -f$ is equally optimal because the quadratic form is invariant under this sign flip. ] // 14. HamiltonianPath → IsomorphicSpanningTree (#912) diff --git a/docs/paper/references.bib b/docs/paper/references.bib index a65104787..640774531 100644 --- a/docs/paper/references.bib +++ b/docs/paper/references.bib @@ -2332,3 +2332,14 @@ @article{axler2019 year = {2019}, url = {https://www.maths.tcd.ie/EMIS/journals/JIS/VOL22/Axler/axler17.pdf} } + +@article{een2006, + author = {Niklas E{\'e}n and Niklas S{\"o}rensson}, + title = {Translating Pseudo-Boolean Constraints into {SAT}}, + journal = {Journal on Satisfiability, Boolean Modeling and Computation}, + year = {2006}, + volume = {2}, + number = {1--4}, + pages = {1--26}, + doi = {10.3233/SAT190014}, +} diff --git a/docs/website/graph-scene.schema.json b/docs/website/graph-scene.schema.json index 7510f608a..90cb68e8e 100644 --- a/docs/website/graph-scene.schema.json +++ b/docs/website/graph-scene.schema.json @@ -23,12 +23,27 @@ "type": "array", "items": { "type": "object", "additionalProperties": false, - "required": ["source", "target", "witness", "turing"], + "required": ["source", "target", "witness", "aggregate", "turing", "fields"], "properties": { "source": {"type": "integer", "minimum": 0, "maximum": 9007199254740991}, "target": {"type": "integer", "minimum": 0, "maximum": 9007199254740991}, "witness": {"type": "boolean"}, - "turing": {"type": "boolean"} + "aggregate": {"type": "boolean"}, + "turing": {"type": "boolean"}, + "fields": { + "type": "object", + "additionalProperties": { + "type": "object", "additionalProperties": false, + "required": ["certificate", "accuracy"], + "properties": { + "certificate": {"type": ["string", "null"], "minLength": 1}, + "accuracy": { + "type": "object", "required": ["kind"], + "properties": {"kind": {"enum": ["exact", "upper_bound", "unavailable"]}} + } + } + } + } } } }, diff --git a/docs/website/graph.html b/docs/website/graph.html index dcb029482..1ddb292ad 100644 --- a/docs/website/graph.html +++ b/docs/website/graph.html @@ -8,8 +8,13 @@ Reduction Paths — Problem Reductions - - + @@ -33,24 +38,45 @@
-
-

Reduction paths

-
-
- -
+
+ +
+

Reduction graph

+
+ +
-
- -
+
+
+
+ -
-
+

Routes alone do not establish complexity or solver availability. Colours summarize variants.

+
+ +
+
+
Growth
+
+
+