Answer: Always terminates with a fully evaluated assignment \(x\in\mathcal F\) satisfying \(\Phi_\mu(x)\le w\min_{y\in\mathcal F}\Phi_\mu(y)+\epsilon\).
Theorem 7.1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateDFBnB with the LUC heuristic parameterized by a user-defined relative weight w ≥1 and a user-defined additive weight ϵ ≥0 will return an IWCSP solution whose cost is bounded from above by w · FP(x∗) + ϵ, where x∗is an optimal complete IWCSP solution.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite-domain assignment space \(\mathcal F\), a finite support \(T\) of preference types with rational masses \(\mu_t\ge0\) summing to \(1\), and type-specific nonnegative cost tables with entries that can be elicited for free, let \(F_t(x)\) be type \(t\)'s completed cost and \(\Phi_\mu(x)=\sum_{t\in T}\mu_tF_t(x)\). For inputs \(w\ge1\) and \(\epsilon\ge0\), can DFBnB with a mass-weighted LUC lower bound return a feasible assignment \(x\), eliciting enough entries to evaluate its true cost, with \(\Phi_\mu(x)\le w\min_{y\in\mathcal F}\Phi_\mu(y)+\epsilon\)?
Let \(X=\{x_1,\ldots,x_m\}\) have explicitly listed, nonempty finite domains \(D_i\), and let \(\mathcal F=\prod_iD_i\).
A society is given by its support: a list of \(\tau\) types with positive binary-rational masses \(\mu_t\) summing to \(1\); \(\tau\) is the support size, not the number of possible types.
Each type has explicitly indexed local cost tables \(c_{t,j}\) with specified variable scopes \(S_{t,j}\). Entries are finite nonnegative binary rationals, initially either revealed or unknown; a free query reveals an unknown entry's fixed true value, which is then cached. Define \(F_t(x)=\sum_jc_{t,j}(x|_{S_{t,j}})\) and \(\Phi_\mu(x)=\sum_t\mu_tF_t(x)\).
Use a supplied valid common entry lower bound \(\ell\ge0\), and binary-rational parameters \(w\ge1\) and \(\epsilon\ge0\). DFBnB searches the variable-assignment tree in a fixed variable order, eliciting entries whose scopes become fully assigned before evaluating a node.
At a partial assignment \(p\), let \(g_\mu(p)\) be the mass-weighted sum of costs with fully assigned scopes. For a completion \(y\supseteq p\), let \(u_t(p,y)\) count still-unknown entries used by \(y\) in tables whose scopes are not fully assigned by \(p\). The mass-weighted LUC estimate is \(b_\mu(p)=g_\mu(p)+\ell\min_{y\in\mathcal F,\,y\supseteq p}\sum_t\mu_tu_t(p,y)\).
Maintain an incumbent of fully elicited true cost \(B\); prune precisely when an incumbent exists and \(w b_\mu(p)+\epsilon\ge B\). Explore children in increasing current estimate, break ties by fixed domain orders, update the incumbent at complete assignments, and terminate when search finishes. Express any running-time bounds in \(m,\tau,L\), domain sizes, and table counts, where \(L\) is the total encoding length, including query answers.
Does this mass-weighted LUC DFBnB always terminate with a fully evaluated assignment \(x\in\mathcal F\) satisfying \(\Phi_\mu(x)\le w\min_{y\in\mathcal F}\Phi_\mu(y)+\epsilon\), or can this approximation guarantee fail?
For discrete incomplete WCSPs with zero elicitation costs, LUC DFBnB has the corresponding multiplicative-plus-additive guarantee; no polynomial-time bound is asserted ([Tabakhi, Yeoh and Yokoo, 2019](https://www.ifaamas.org/Proceedings/aamas2019/pdfs/p476.pdf)).
No result specifically addressing the support-and-mass formulation above was located.
The mass-weighted LUC DFBnB always terminates and returns a fully evaluated assignment \(x\) satisfying
\[
\Phi_\mu(x)\le w\min_{y\in\mathcal F}\Phi_\mu(y)+\epsilon.
\]
Here “incumbent” has its usual branch-and-bound meaning: a stored, fully evaluated assignment of minimum true cost among the complete assignments accepted so far. The search may start without an incumbent or with any fully evaluated feasible assignment.
The proof below directly handles the support-and-mass formulation. It does not require reducing rational masses to replicated types or assuming polynomial-time computation of the LUC estimate.
Fix a partial assignment \(p\) and the cache state when its estimate is evaluated. Let
\(A_t(p)=\{j:S_{t,j}\subseteq\operatorname{dom}(p)\}\)
be the indices of type \(t\)'s tables whose scopes are fully assigned.
By the elicitation rule, every entry contributing to
\[
g_\mu(p)=\sum_{t=1}^{\tau}\mu_t\sum_{j\in A_t(p)}
c_{t,j}(p|_{S_{t,j}})
\]
has been revealed.
Fix any completion \(y\supseteq p\). Its true cost decomposes as
\[
\Phi_\mu(y)=g_\mu(p)+
\sum_{t=1}^{\tau}\mu_t\sum_{j\notin A_t(p)}
c_{t,j}(y|_{S_{t,j}}).
\]
Among the terms in the second sum, exactly \(u_t(p,y)\) entries for type \(t\) are currently unknown. Each such entry has true cost at least \(\ell\). Every other term is nonnegative, and every mass is positive. Consequently,
\[
\Phi_\mu(y)\ge g_\mu(p)+\ell\sum_{t=1}^{\tau}\mu_tu_t(p,y).
\]
The set of completions of \(p\) is finite and nonempty. Since \(\ell\ge0\),
\[
b_\mu(p)
=g_\mu(p)+\ell\min_{z\supseteq p}\sum_{t=1}^{\tau}\mu_tu_t(p,z)
\le g_\mu(p)+\ell\sum_{t=1}^{\tau}\mu_tu_t(p,y)
\le\Phi_\mu(y).
\]
Thus at every cache state, \(b_\mu(p)\) is a lower bound on the true cost of every completion of \(p\).
This argument uses the weighted sum inside the stated minimum; it does not interchange minimization and summation. It also remains valid when queries reveal entries used by other branches. No monotonicity of the estimates is required.
At a complete assignment \(x\), all table scopes are fully assigned and their used entries have been elicited. Therefore \(u_t(x,x)=0\) for every type and
\[
b_\mu(x)=g_\mu(x)=\Phi_\mu(x).
\]
Write \(d_i=|D_i|\), numbering variables in their fixed search order. The assignment tree has
\[
N=\sum_{k=0}^{m}\prod_{i=1}^{k}d_i
\]
nodes, where the empty product is \(1\). In particular, it is finite.
Every estimate can be computed by enumerating the finitely many completions of its partial assignment. All relevant sums and comparisons involve finite binary rationals, so exact evaluation terminates.
There are also only finitely many table entries. Because queries are cached, each initially unknown entry is queried at most once. Ordinary DFBnB expands each node at most once, or discards its subtree by pruning. Hence the search terminates.
If the search starts without an incumbent, it cannot prune any node until one exists. Since every domain is nonempty, depth-first exploration reaches a complete assignment. All entries used by that assignment are elicited before its evaluation, and it supplies the first incumbent.
Every later incumbent is likewise fully evaluated. Querying has zero cost and reveals fixed values, so the true cost of a stored assignment never changes. Updating to a better incumbent makes its cost \(B\) nonincreasing.
For \(m=0\), the root itself is the unique complete assignment; the same reasoning applies, including elicitation of any empty-scope entries.
Because \(\mathcal F\) is finite and nonempty, choose an optimal assignment \(x^\star\), and write
\[
\operatorname{OPT}=\Phi_\mu(x^\star).
\]
Let \(B_{\mathrm{final}}\) be the returned incumbent's true cost.
There are two exhaustive cases.
Case 1: The optimal leaf is considered for an incumbent update.
At that point, the incumbent cost becomes at most \(\operatorname{OPT}\). Since incumbent costs are nonincreasing,
\[
B_{\mathrm{final}}\le\operatorname{OPT}
\le w\operatorname{OPT}+\epsilon,
\]
where the second inequality follows from \(\operatorname{OPT}\ge0\), \(w\ge1\), and \(\epsilon\ge0\).
Case 2: The optimal leaf is not considered for an incumbent update.
Because the finite search finishes, some node \(p\) on the path to \(x^\star\), possibly the leaf itself, must have been pruned. Let \(B_p\) be the incumbent cost at that moment. The prescribed pruning condition gives
\[
B_p\le w b_\mu(p)+\epsilon.
\]
The lower-bound result applies to the cache state at that moment and to the completion \(x^\star\), giving \(b_\mu(p)\le\operatorname{OPT}\). Since \(w\ge0\) and the incumbent cost is nonincreasing,
\[
B_{\mathrm{final}}
\le B_p
\le w b_\mu(p)+\epsilon
\le w\operatorname{OPT}+\epsilon.
\]
Both cases establish the claimed guarantee. Child ordering and tie-breaking affect the work performed, but not this argument.
The corresponding unweighted pruning argument appears in Theorem 7.1 of [Tabakhi, Yeoh and Yokoo (2019)](https://www.ifaamas.org/Proceedings/aamas2019/pdfs/p476.pdf); the lower-bound proof above supplies the required justification for the mass-weighted formulation.
Let \(k_t\) be the number of tables for type \(t\), and define
\[
C=\sum_{t=1}^{\tau}k_t,\qquad
E=\sum_{t=1}^{\tau}\sum_{j=1}^{k_t}
\prod_{x_i\in S_{t,j}}d_i,\qquad
P=\prod_{i=1}^{m}d_i,\qquad
D=\max(\{1\}\cup\{d_i:1\le i\le m\}).
\]
Here \(C\) counts tables, \(E\) counts their indexed entries, and \(P\) counts complete assignments. Empty scopes contribute one entry. The total number of queries is at most the number of initially unknown entries, hence at most \(E\).
A straightforward exact estimate computation enumerates at most \(P\) completions and scans the \(C\) tables for each completion. Table access, scope restriction, rational arithmetic, and comparisons take time polynomial in \(m,\tau,C,L\). Including query answers in \(L\) bounds the encodings of all revealed values used in these calculations.
To maintain increasing current estimates, one implementation recomputes the estimates of all remaining children whenever it selects the next child. Required queries are completed before comparing estimates in the resulting cache state. A parent with \(d\) children needs at most \(O(d^2)\) child-estimate evaluations. Summing over parents gives at most \(O(DN)\) such evaluations; node pruning checks add \(O(N)\).
Thus a conservative bit-time bound is
\[
O\!\left(
L+E+(D+1)NP\,\operatorname{poly}(m,\tau,C,L)
\right).
\]
Since \(N\le(m+1)P\), this is also bounded by
\[
O\!\left(
L+E+(D+1)(m+1)P^2\,\operatorname{poly}(m,\tau,C,L)
\right).
\]
These are finite exhaustive-search bounds, not polynomial-time guarantees. They depend on the explicitly supplied support size \(\tau\), without introducing the number of possible types.
⟨structured verdict parsed — rendered above⟩
The approximation argument is correct. The output resolves the intended task, with one minor clarification needed about the encoding of \(\ell\). No central mathematical step is false, and no additional lemma is needed.
The decomposition is valid. For each type, \(A_t(p)\) identifies exactly the tables whose scopes are fully assigned. The elicitation rule ensures their used entries are revealed before evaluation, so \(g_\mu(p)\) is their true mass-weighted contribution. Every completion agrees with \(p\) on those scopes.
The bound on the remaining contribution is valid. For a fixed completion \(y\), each of its \(u_t(p,y)\) unknown entries contributes at least \(\ell\). All remaining known entries contribute nonnegative costs. Positive masses preserve the resulting inequality.
This reasoning correctly counts table-entry occurrences contributing to the objective; it does not confuse the support size with the number of possible types.
Taking the minimum is justified. Every partial assignment in this tree has a finite, nonempty completion set because all domains are finite and nonempty. Since \(\ell\ge0\), replacing the weighted unknown count for a particular completion by its minimum preserves the required inequality. Thus \(b_\mu(p)\le\Phi_\mu(y)\) for every completion \(y\).
The prover correctly keeps the weighted sum inside the minimum. It neither exchanges minimization and summation nor assumes that each type can choose its completion independently.
Cache changes cause no gap. The argument applies separately at every cache state. Revealing an entry can change the estimate, but does not invalidate its lower-bound property. Monotonicity of estimates is unnecessary.
The complete-assignment identity is correct. At a leaf, all scopes are assigned and all used entries have been elicited. Consequently, \(u_t(x,x)=0\) and \(b_\mu(x)=g_\mu(x)=\Phi_\mu(x)\).
The node count is correct. At depth \(k\), the tree contains \(\prod_{i=1}^{k}d_i\) assignments, yielding the stated finite sum \(N\). Variables must be numbered in the supplied search order, as the prover explicitly specifies.
The query bound is correct. Every indexed entry has a fixed value, and caching prevents repeated elicitation. Therefore at most \(E\) queries occur.
Existence of an incumbent is established. Without an incumbent, pruning is forbidden. Finite depth and nonempty domains therefore lead to a complete assignment, whose used entries are revealed before evaluation. An initially supplied fully evaluated feasible incumbent also satisfies the required invariant.
Incumbent costs are nonincreasing. The prover explicitly uses the standard minimum-cost incumbent convention. Fixed query answers ensure that later elicitation does not change an incumbent’s true cost.
The treatment of \(m=0\), including empty-scope tables, is correct. Zero costs, \(\ell=0\), and empty table collections introduce no additional problem.
The claim that every estimate can be evaluated exactly in finite time needs the encoding clarification identified below.
The two cases are exhaustive under the specified finite tree search.
Case 1 is correct. If the optimal leaf is considered for an incumbent update, the incumbent thereafter has cost at most \(\operatorname{OPT}\). Subsequent updates cannot increase it. Nonnegative costs, \(w\ge1\), and \(\epsilon\ge0\) justify the final comparison.
Case 2 is correct. If the optimal leaf is never considered for an update, some node on its path must have been pruned. This includes pruning the leaf itself.
At that pruning event, the incumbent exists and satisfies
\[
B_p\le w b_\mu(p)+\epsilon.
\]
The lower-bound result applies to the actual cache state at that event, giving \(b_\mu(p)\le\operatorname{OPT}\). Multiplication preserves this inequality because \(w\ge1\), and the final incumbent costs no more than \(B_p\). The displayed chain therefore establishes the claimed guarantee.
Equality in the pruning condition causes no difficulty. Child ordering and tie-breaking are irrelevant to this proof.
The citation is accurate and supplementary. Theorem 7.1 states the corresponding LUC guarantee for nonnegative IWCSP costs, zero elicitation costs, relative weight at least one, and nonnegative additive weight. Its proof uses the same pruning argument. The present output independently establishes the weighted lower bound, so it does not improperly apply the unweighted theorem to rational masses. [Tabakhi, Yeoh and Yokoo (2019), Theorem 7.1](https://www.ifaamas.org/Proceedings/aamas2019/pdfs/p476.pdf).
The definitions of \(C\), \(E\), \(P\), and \(D\) are consistent with the explicitly indexed tables. Empty scopes correctly contribute one entry.
Enumerating at most \(P\) completions and scanning the tables provides a finite exhaustive procedure. Subject to the encoding clarification below, exact rational arithmetic has polynomial bit cost in the stated parameters; the bound need not include unknown values that are never queried.
The proposed child-selection implementation explicitly completes required queries before comparing estimates in the resulting cache state. This is necessary because eliciting entries for one child can change another child’s estimate.
The counting bounds are correct:
The resulting bounds are conservative exhaustive-search bounds. They establish neither polynomial-time solvability nor hardness.
Minor — Sections 2 and 4: the encoding of \(\ell\) is unstated.
The task explicitly specifies binary-rational costs, masses, \(w\), and \(\epsilon\), but only calls \(\ell\) a “supplied valid common entry lower bound.” The prover consequently overstates matters when it says that all relevant sums and comparisons involve finite binary rationals.
For example, one variable with a singleton domain, one unknown table entry of true cost \(2\), mass \(1\), and \(\ell=\sqrt{2}\) satisfies the stated numerical lower-bound conditions. Its root estimate is \(\sqrt{2}\), which is not binary rational.
Minimum clarification: explicitly state that the computational claims use the natural finite-input interpretation in which \(\ell\) is supplied as a binary rational and its encoding is included in \(L\).
This is a minor input-specification clarification under the task’s stated discipline. The lower-bound and approximation arguments remain valid for any valid nonnegative \(\ell\); the clarification concerns exact computation and bit-time claims.
⟨structured verdict parsed — rendered above⟩
Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.