Answer: \(\mathrm{NP}\)-hard: a polynomial-time constructor exists if and only if \(\mathrm{P}=\mathrm{NP}\). For satisfiable inputs, a polynomial-time construction exists with \(\tau=1\).
Theorem 10 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateAny KB K is L2CNF -simplifiable w.r.t. ∆H µ .
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a target knowledge base \(K\) over a finite vocabulary \(U\), can one construct a finitely supported rational distribution \(\nu\) over \(2\mathrm{CNF}\) knowledge-base types, allowing fresh auxiliary atoms, and a \(2\mathrm{CNF}\) integrity constraint \(\mu\), such that the interpretations minimizing \(\sum_t \nu_t \min_{\omega'\models K_t} d_H(\omega,\omega')\) among models of \(\mu\) project onto \(U\) as exactly \(\operatorname{Mod}(K)\)?
Input: a finite propositional knowledge base \(K\), encoded as a list of formulas over \(U\), with \(m=|U|\) and input bit length \(L\).
Construct a finite set \(A\) of fresh atoms, a rational distribution \(\nu\) over satisfiable \(2\mathrm{CNF}\) knowledge bases \(K_t\) on \(V=U\cup A\), and a \(2\mathrm{CNF}\) integrity constraint \(\mu\) on \(V\).
A society is given by its support: the list of its \(\tau\) types with positive mass, each mass encoded as a binary rational; \(\tau\) is the support size, not the number of possible types. Require \(\sum_{t=1}^{\tau}\nu_t=1\).
For \(\omega\subseteq V\), let \(F_\nu(\omega)=\sum_{t=1}^{\tau}\nu_t\min_{\omega'\in\operatorname{Mod}_V(K_t)}d_H(\omega,\omega')\), using Hamming distance on all atoms of \(V\).
Require \(\{\omega\cap U:\omega\in\arg\min_{\eta\in\operatorname{Mod}_V(\mu)}F_\nu(\eta)\}=\operatorname{Mod}_U(K)\). Retain all minimizers; the minimizing set is empty when \(\mu\) is unsatisfiable.
There are no prescribed bounds on \(|A|\), \(\tau\), or representation length. State running times in \(m,\tau,L,|A|\) and total output bit length \(B\).
Is this construction problem solvable in time polynomial in \(m+L\), or is it \(\mathrm{NP}\)-hard?
Known: with auxiliary atoms, every finite knowledge base admits reconstruction by Hamming-distance minimization from a single \(2\mathrm{CNF}\) base under a \(2\mathrm{CNF}\) constraint; this is an existence result, and construction complexity was left open. [Published result](https://www.ijcai.org/Proceedings/16/Papers/161.pdf)
No complexity classification for the stated rational-mass construction problem was located in the literature search.
The construction problem is \(\mathrm{NP}\)-hard in the precise sense that a polynomial-time constructor would give a polynomial-time algorithm for SAT. In fact, a polynomial-time constructor exists if and only if \(\mathrm{P}=\mathrm{NP}\).
The inconsistency case gives the hardness argument immediately. To address the substantive reconstruction question as well, I prove that satisfiable inputs admit a polynomial-time construction with \(\tau=1\). Consequently, the unrestricted problem can be solved using one SAT decision followed by polynomial-time construction.
The proof below is independent of the model-enumerating existence construction in [Haret, Mailly, and Woltran, Theorem 10](https://www.ijcai.org/Proceedings/16/Papers/161.pdf).
Let \((A,\nu,\mu)\) be any valid output, and put \(V=U\cup A\).
Each \(K_t\) is satisfiable, so for every interpretation \(\omega\subseteq V\), its distance to \(K_t\) is a finite integer between \(0\) and \(|V|\). Thus \(F_\nu(\omega)\) is finite.
If \(\mu\) is satisfiable, its model set is finite and nonempty. A finite real-valued function on such a set attains its minimum. Therefore its minimizing set, and hence its projection onto \(U\), is nonempty. If \(\mu\) is unsatisfiable, the minimizing set is empty by the stipulated convention.
The required reconstruction equality consequently implies
\(\operatorname{Mod}_U(K)\neq\varnothing\quad\Longleftrightarrow\quad\operatorname{Mod}_V(\mu)\neq\varnothing.\)
The standard 2-SAT theorem decides satisfiability of a conjunction of clauses of length at most two using strongly connected components of its implication graph. Its hypotheses apply directly to the output constraint \(\mu\), including unit clauses.
Thus, given a constructor, we can decide SAT by:
For explicit output of bit length \(B\), this postprocessing takes polynomial time in \(B+m+|A|+\tau\). If the constructor runs in polynomial time in \(m+L\), its explicit output length is also polynomial in \(m+L\). The resulting SAT algorithm is therefore polynomial-time.
This proves the claimed hardness implication. Because outputs have no prescribed size bound, the reduction is understood with postprocessing polynomial in the explicit output length; it does not assume that every valid output is small.
Assume throughout this section that \(K\) is satisfiable.
Construct a CNF formula \(D\) over \(U\cup Z\), where \(Z\) consists of fresh atoms, such that every clause has at most three literals and
\(\operatorname{Mod}_U(K)=\{y\cap U:y\in\operatorname{Mod}_{U\cup Z}(D)\}.\)
Here is an explicit standard construction. Represent the input formulas by a Boolean circuit with negation and binary conjunction and disjunction gates, and introduce an atom for each gate output. Enforce each gate equivalence by clauses:
Require each input formula’s output to be true by a unit clause. Constants can likewise be represented by atoms fixed through unit clauses.
For conjunction gates, the first two clauses enforce \(z\Rightarrow a\land b\), and the third enforces \(a\land b\Rightarrow z\). The disjunction and negation clauses enforce their respective equivalences by the same direct implications. Induction through the circuit therefore forces every gate atom to equal its evaluated output. This proves the projection equality.
Write
\(D=\bigwedge_{i=1}^{r}C_i,\qquad C_i=\bigvee_{j=1}^{k_i}\ell_{ij},\qquad 1\leq k_i\leq3.\)
The construction has \(|Z|=O(L+1)\) and \(r=O(L+1)\). An empty input list can instead use \(D=\top\), with \(r=0\).
Introduce a fresh selector \(s_{ij}\) for every literal occurrence \(\ell_{ij}\). Let
\(S=\{s_{ij}:1\leq i\leq r,\ 1\leq j\leq k_i\},\qquad A=Z\cup S,\qquad N=|S|.\)
Use one type, of mass \(\nu_1=1\), with base
\(K_1=\bigwedge_{i=1}^{r}\bigwedge_{j=1}^{k_i}s_{ij}.\)
This is a satisfiable \(1\mathrm{CNF}\), hence a satisfiable \(2\mathrm{CNF}\).
Define the integrity constraint by
\(\mu=\left(\bigwedge_{i=1}^{r}\bigwedge_{1\leq j<h\leq k_i}(\neg s_{ij}\lor\neg s_{ih})\right)\land\left(\bigwedge_{i=1}^{r}\bigwedge_{j=1}^{k_i}(\neg s_{ij}\lor\ell_{ij})\right).\)
Every clause has length two. The first group permits at most one true selector per clause; the second requires a selected literal to be true. Setting every selector false satisfies \(\mu\), regardless of the other atoms.
For every \(\omega\subseteq V\),
\(F_\nu(\omega)=d_H(\omega,\operatorname{Mod}_V(K_1))=N-|\omega\cap S|.\)
Indeed, every false selector in \(\omega\) must become true in any model of \(K_1\), giving this lower bound. It is attained by changing exactly those selectors and leaving every atom outside \(S\) unchanged. Thus the calculation uses Hamming distance on all atoms of \(V\).
For every \(\omega\models\mu\), at most one selector per clause is true, so
\(|\omega\cap S|\leq r,\qquad F_\nu(\omega)\geq N-r.\)
Because \(K\) is satisfiable, so is \(D\). Given a model of \(D\), choose one true literal from each clause and make precisely its selector true. This satisfies \(\mu\), has exactly \(r\) true selectors, and attains distance \(N-r\). Hence the minimum is exactly \(N-r\).
First, let \(x\in\operatorname{Mod}_U(K)\). The encoding property gives an extension \(y\models D\). Choosing one true literal per clause as above produces an extension \(\omega\models\mu\) with distance \(N-r\). Thus \(x\) is the projection of a minimizer.
Conversely, let \(\omega\) be any minimizer. Its distance is \(N-r\), so exactly \(r\) selectors are true. Since \(\mu\) permits at most one per clause, each clause has exactly one true selector. The corresponding implication clause forces its literal to be true. Therefore \(\omega\cap(U\cup Z)\models D\), and the encoding property implies \(\omega\cap U\models K\).
Both inclusions hold, establishing
\(\{\omega\cap U:\omega\in\arg\min_{\eta\models\mu}F_\nu(\eta)\}=\operatorname{Mod}_U(K).\)
This argument retains every minimizer and requires no tie-breaking.
For an arbitrary input, first decide whether \(K\) is satisfiable.
Thus one SAT decision suffices.
Put \(n=m+L+1\). The constructed outputs satisfy \(\tau=1\), \(|A|=O(L+1)\), and have \(O(L+1)\) clauses and literal occurrences. With indexed atom names, their total bit length is \(B=O(n\log(n+1))\).
Conservative running-time bounds are:
For an arbitrary constructor taking time \(T\) and producing output length \(B\), the satisfiability reduction runs in \(T+\operatorname{poly}(m+|A|+\tau+B)\). These bounds depend on the listed support, not on the number of possible types.
If \(\mathrm{P}=\mathrm{NP}\), the initial SAT decision is polynomial-time, so the unrestricted construction is polynomial-time. Section 1 proves the converse. This completes the classification.
⟨structured verdict parsed — rendered above⟩
The prover’s classification is correct. The construction and reduction resolve the stated task; I found no major or minor mathematical issues.
Each supported base is satisfiable, so its distance from every interpretation is finite. The rational weighted sum is consequently finite everywhere.
If the integrity constraint is satisfiable, its feasible set is finite and nonempty, so a minimum exists. Projecting a nonempty minimizing set cannot produce an empty set. If the constraint is unsatisfiable, the minimizing set is empty by the task’s convention. The required reconstruction equality therefore establishes exactly
\[
\operatorname{Mod}_U(K)\neq\varnothing
\quad\Longleftrightarrow\quad
\operatorname{Mod}_V(\mu)\neq\varnothing.
\]
Neither implication requires computing distances or finding minimizers.
Applying a constructor to a singleton knowledge base containing an arbitrary propositional formula is a valid input transformation. Its output constraint is explicitly represented \(2\mathrm{CNF}\), so the stated polynomial-time \(2\mathrm{SAT}\) theorem applies, including to unit clauses.
A polynomial-time constructor can write only polynomially many output bits. Consequently, testing its output constraint yields a polynomial-time SAT algorithm. The absence of prescribed output-size bounds does not invalidate this implication.
The prover appropriately qualifies its hardness claim: this is a reduction to producing a valid construction, with postprocessing polynomial in the explicit output size. It does not assert that all valid outputs have polynomial size.
All three displayed gate encodings correctly enforce their respective equivalences. Requiring each formula’s output to be true enforces satisfaction of the whole knowledge base.
The circuit induction establishes both necessary directions: satisfying original assignments extend to satisfying gate assignments, and every satisfying encoded assignment evaluates each input formula to true. No uniqueness of extensions is needed for the subsequent argument.
For the conventional propositional formula encoding intended by the task, the stated linear bounds on gate atoms and clauses are valid. Representing constants by fixed atoms avoids empty clauses. The empty knowledge base is explicitly handled.
The selector atoms are fresh and distinct for each literal occurrence. The single base is a conjunction of positive unit clauses and is satisfiable. Its sole mass is the positive rational \(1\), so the distribution is normalized and its support size is exactly \(1\).
Every integrity clause has at most two literals. Within each encoded clause, the first group prohibits two simultaneously true selectors; the second group requires every selected literal to hold. Setting all selectors false indeed satisfies the constraint for every assignment to the remaining atoms.
Every selector false in the candidate must change in any model of the base. Conversely, changing precisely those selectors produces a base model while leaving every other atom unchanged. Thus
\[
F_\nu(\omega)=N-|\omega\cap S|
\]
is both a lower bound and an attained distance.
Feasibility permits at most one true selector per clause, giving the bound
\[
F_\nu(\omega)\geq N-r.
\]
Under the satisfiability assumption, a model of the encoding supplies one true literal per clause. Selecting those occurrences attains the bound. The claimed minimum follows without any unverified optimization assumption.
Every original model extends to an encoded model and then to a feasible assignment attaining the minimum.
Conversely, every minimizer has exactly \(r\) true selectors. Since each of the \(r\) clause groups contributes at most one, each contributes exactly one. Its implication clause forces a true literal in that encoded clause. Therefore every minimizer satisfies the encoded formula on the nonselector atoms, and its original projection satisfies the input knowledge base.
This establishes equality for the entire minimizing set, including all ties.
For an inconsistent input, the contradictory unit constraint has no models, while the empty base remains satisfiable. Both sides of the reconstruction equality are empty.
When \(r=0\), also \(N=0\); the selector construction has constant zero objective and imposes no restrictions, correctly reconstructing the empty knowledge base. Unused original atoms remain unrestricted. Constants and an empty original vocabulary introduce no failure.
There are at most three selectors per encoded clause and at most three pairwise exclusion clauses per clause. Hence the auxiliary vocabulary and output clause counts have the stated linear bounds. Indexed names give the stated conservative output-bit bound.
The polynomial construction bounds and exhaustive-evaluation bound are consistent with these sizes. The reduction also accounts for the listed support and explicit output length.
Assuming \(\mathrm{P}=\mathrm{NP}\), the initial SAT decision and subsequent construction are polynomial-time. The converse follows from item 2. The reference to the model-enumerating existence construction is accurate, but the argument does not depend on [Theorem 10 of the cited paper](https://www.ijcai.org/Proceedings/16/Papers/161.pdf).
No additional clarification is needed to make the mathematical argument verifiable.
⟨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.