| paper | d4-conf-ecai-2008-0193 |
| authors | — |
| venue | ? |
| filed under | unclassified |
| judged by | gpt-6-luna / xhigh (triple__luna__xhigh__c6r1) |
| judge confidence | medium |
| authors would recognise it | yes |
other→NP-hard discrete result → its continuous mirror
Answer: \(\mathrm{NP}\text{-hard}\), even for one guaranteed-feasible type with a singleton preference set; polynomial-time solvable if and only if \(\mathrm{P}=\mathrm{NP}\). · discrete side: other · adjudication: proved
full proof & adversarial review →
Theorem 2
statement extracted from the paper’s text layer
Given a finite set \(T\) of complete SAT task types, each with a formula \(\varphi_t\) and qualitative preference \((S_t,\prec_t)\), and rational masses \(\mu_t>0\) summing to \(1\), find an allocation \(x_{t,a}\ge 0\) over satisfying total assignments \(a\models\varphi_t\). Require \(\sum_{a\models\varphi_t}x_{t,a}=\mu_t\), with positive mass only on assignments optimal under \((S_t,\prec_t)\); report infeasibility if any positive-mass type has no satisfying model.
Each type is a repeated planning task with the same formula and preferences for every unit of its mass. The decision variables \(x_{t,a}\) assign mass to whole satisfying plans, and the requirement is that every assigned plan be qualitatively optimal for its type; there is no aggregate objective.
The mirror covers Theorem 2’s guarantee of an optimal model for each task type. It leaves aside the experimental comparisons and quantitative-preference results.
My strongest lead is Continuous Qualitative Planning Allocation, anchored on Theorem 2, proved in this paper. One qualification: the paper has no named result placing a problem in P or proving it hard. Theorem 2 is a correctness and termination result for an algorithm, not a complexity classification.
Theorem 2 says that for a formula \(\varphi\) and a qualitative preference \((S,\prec)\) on literals, \(\mathrm{PREF\text{-}DLL}(\varphi,\varnothing)\) terminates; it leaves \(\mu_{\mathrm{opt}}\) empty if \(\varphi\) is unsatisfiable, and otherwise returns a model that is optimal under \((S,\prec)\). That is the result I would mirror.
In the continuous problem, an instance is a finite set \(T\) of SAT task types with rational masses \(\mu_t>0\) summing to \(1\). Each type \(t\) specifies a full task template: Boolean variables \(P_t\), a formula \(\varphi_t\), and a qualitative preference \((S_t,\prec_t)\). A type is the complete task description, so agents of the same type have the same constraints and preferences. The decision variable is \(x_{t,a}\ge 0\), the mass of type \(t\) assigned satisfying model \(a\). Require \(\sum_{a\models\varphi_t}x_{t,a}=\mu_t\). The question is to report infeasibility if a positive-mass type has no model; otherwise return an allocation whose positive-mass assignments are all optimal under that type’s qualitative preference. As in the paper, \(a\) is preferred to \(b\) when \(a\) gains at least one preferred literal and every preferred literal lost from \(b\) is compensated by a gained literal ranked above it. A sparse output can give each type’s entire mass to one optimal model, or split it among several optimal models.
A plausible regime is a large planning service handling many repeated jobs or operational episodes. Each episode receives a satisfying plan; millions of episodes may fall into a modest number of complete task templates, including their soft goals. The episode fractions are the masses. That is a high-multiplicity setting: the number of jobs can greatly exceed the number of types. It also connects to the paper’s planning motivation, though it need not be the paper’s particular benchmark scenario.
The expected direction is hardness transfers. With one type of mass \(1\) and \(S=\varnothing\), the continuous problem has a solution exactly when \(\varphi\) is satisfiable. The masses add no relief from the SAT search. Theorem 2 supplies a terminating method for finding an optimum in each type, but gives no polynomial-time bound; applied across the support, it guarantees correctness and termination, not tractability.
This mirror covers Theorem 2’s optimal-model guarantee only. I would not use the solver benchmarks or its quantitative-preference results as anchors for this case. It raises follow-up questions about which structured planning templates admit efficient algorithms, and whether restrictions on the support size \(\tau\) help when the formulas differ by type.
The soft spot is that this is a separable workload of repeated SAT tasks: the continuum scales how many agents receive each plan, but it does not change the optimization for any one task. The paper’s SAT-planning instance may instead encode one joint plan for an entire system. Authors could regard repeated independent jobs as a useful application of their solver rather than a continuous version of their central problem. The case survives as a narrow mirror because each episode solves exactly their optimal-model problem, and the population is genuinely high-multiplicity; it should not be presented as a new continuous algorithmic phenomenon.
The strongest objection is that the paper’s formal results do not classify the complexity of an optimization problem. Theorem 2 proves termination and optimality for PREF-DLL; Theorems 1 and 3 establish properties of the preference formula. The paper’s claims about performance come from experiments on finite SAT instances. A population version can be posed, but it would extend the paper’s algorithm to a workload rather than mirror a complexity result the paper establishes.
The proposed planning-episode scenario is plausible: many episodes can share a complete task type \((\varphi_t,S_t,\prec_t)\). Grant that regime and strengthen the mirror as far as it reasonably goes: for each type, allocate its mass among satisfying models, requiring every assigned model to be optimal. But the choices are independent across episodes and types. For each type, run the paper’s procedure once and assign all its mass to one optimal model. If the formula is unsatisfiable, that type has no allocation. The masses affect neither which models qualify nor how hard it is to find one.
So the continuum carries no operative decision. Splitting a type across several optimal models changes nothing unless the problem adds an objective or constraint that couples those assignments. This is the continuum-degeneration case: the fractional allocation can always be replaced by a pure assignment, with no loss under the mirrored requirement. There is no population-level tradeoff for continuous optimization to exploit or analyze.
One could add shared resources, a collective objective, or limits on which plans the service can provide. Those may be worthwhile planning problems, but they introduce the coupling that makes the population matter; it is not forced by this paper’s task of finding an optimal model of a formula. They would be new problems, not stronger mirrors of Theorem 2.
This negative case has a real weakness: the repeated-episode regime is sensible, and the resulting batch problem is computationally well-defined. The universal claim that no worthwhile mirror exists is therefore hard to defend. The narrower claim is stronger: this paper offers little for ChoCo’s complexity-landscape programme, because its best anchor yields a separable batch of SAT solves, not a computational problem whose population-level structure is worth continuizing.
The adversarial triple: the proponent anchors on up to three named results; the opponent sees that case and must defeat every anchor; the judge decides which case convinced it. These are the pipeline’s own outputs, generated by tools/triple_run.py — no human edited them. The paper’s own text is not reproduced here beyond the quoted statement above.