{"id":"f5050f0a-4d4e-497c-b46c-60a1d617b76a","arxiv_id":"2507.21752","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Bounded fitting in ALC fragments with existential or universal restrictions is NP-complete even for a single positive and negative example, and a SAT-based implementation, ALC-SAT+, performs competitively with existing concept learners.","lead":"This paper proves that learning the smallest ALC description logic concept that separates positive from negative examples is NP-complete for every fragment with existential or universal restrictions, even with just one example of each type. It also introduces a SAT-based system, ALC-SAT+, that finds such concepts and matches or beats existing learning tools on standard benchmarks.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The normalization step in the reverse direction of the Hitting Set reduction is unsound as written: replacing ∃r.F1⊓∃s.F2 by ∃s.∃s.F1 at d=a_l can produce a concept that fits the negative example. The main NP-hardness proof needs repair.","rationale":"The reader identified the reverse direction of the Hitting Set reduction as the weakest assumption, specifically the intricate size-preserving normalization in Appendix B. My analysis confirms this is the load-bearing point, and it locates a concrete unsound step. The reduction's forward directions and the NP upper bound are fine; the issue is purely in the proof that every small ALC fitting concept can be normalized to an L({∃}) concept of the form ∃r.∃w.A. The counterexample above does not disprove Theorem 1, since the chosen instance has a hitting set and hence the theorem's conclusion still holds; however, it shows that the published proof of Proposition 1 contains a genuine logical gap. Because the main novelty of the paper is the NP-completeness result for all quantifier-containing fragments, this gap affects the central claim. The theorem is plausibly recoverable with a different normalization argument, so the appropriate outcome is conditional acceptance pending a corrected proof, rather than outright rejection. The reader's moderate confidence and ACCEPT verdict should be lowered until the normalization lemma is repaired or independently machine-checked.","tokens_in":27232,"tokens_out":31459,"duration_ms":361946,"concrete_test":"Implement the reduction for S = {{1},{2}} (n = 2, k = 8, k' = 12). Check that C = ∃r.∃s.∃s.(∃r.(∃r.⊤) ⊓ ∃s.(∃s.A)) fits (I,a) and (J,b), and that the concept obtained by applying the d=a_l replacement, namely ∃r.∃s.∃s.∃s.∃s.∃r.⊤, is satisfied in (J,b). The expected outcome is that the transformed concept labels b positively, contradicting the claim that the normalization preserves fitting. A minimal evaluation: c and b_{2,1} satisfy ∃s.∃s.(∃r.⊤) but not ∃r.(∃r.⊤)⊓∃s.(∃s.A), so the key implication in the proof step fails.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"In Appendix B, final claim of Proposition 1, the case d = a_l replaces D_i = ∃r.F1 ⊓ ∃s.F2 by ∃s.∃s.F1, asserting that all elements of R_{w_i}(J,b) fail the replacement because they fail the original conjunction. This implication is false: an R-element can fail the conjunction by failing only ∃s.F2 while satisfying ∃r.F1, and then it may satisfy ∃s.∃s.F1. Concrete witness: take S = {{1},{2}}, n = 2, and the L({∃,⊓,¬}) concept C = ∃r.∃s.∃s.(∃r.(∃r.⊤) ⊓ ∃s.(∃s.A)). C fits the constructed (I,a) and (J,b): after w_i = rss the witness is a_1, and R_{w_i}(J,b) = {c, b_{2,1}}; both elements fail D_i (the s-conjunct fails at the sink), yet both satisfy ∃s.∃s.(∃r.⊤). The transformed concept ∃r.∃s.∃s.∃s.∃s.∃r.⊤ is satisfied at b, so Property 2 is not preserved. Since this normalization is exactly the step that extracts a pure L({∃}) fitting of the required shape, the proof of (iii)⇒(i), and hence of Theorem 1, is not established as written. The theorem may still be true, but the presented argument has a real gap.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies bounded fitting for ALC and its syntactic fragments L(O). The decision problem is size-restricted fitting: given positive and negative examples and a size bound k, is there an L(O) concept of size at most k separating the examples. The main theoretical result is Theorem 1, NP-completeness for every O containing ∃ or ∀, even for one positive and one negative example over a fixed signature of two roles and one concept name. The hardness proof reduces Hitting Set to fitting and includes a normalization argument in Appendix B intended to show that any fitting ALC concept of bounded size can be brought into a pure existential form. The paper also gives PAC lower bounds (Theorems 2 and 3), proves that some natural fitting algorithms are not sample-efficient, and presents a SAT-based implementation with optimizations and experiments on SML benchmarks. The implementation is released.","tokens_in":27554,"tokens_out":24652,"duration_ms":265221,"significance":"If Theorem 1 is correct, the paper makes a strong contribution: it settles the complexity of size-restricted fitting for all quantifier-containing ALC fragments, with a surprisingly strong hardness regime (singleton sample, fixed signature), and it provides a usable SAT-based tool. The PAC results and the discussion of most-specific/most-general algorithms are also valuable. The released implementation and reproducible benchmark setup are credit-worthy. However, the central hardness proof currently contains a real gap, and some transfer arguments in the PAC section are not fully justified, so the paper cannot be accepted in its present form.","major_comments":[{"comment":"In the last claim of the proof of Proposition 1 (Appendix B), the case d = a_ℓ replaces D_i = ∃r.F1 ⊓ ∃s.F2 by ∃s.∃s.F1 and justifies Property 2 by saying that all elements of R_{w_i}(J,b) 'do not satisfy ∃s.∃s.F1, by the assumption that they do not satisfy ∃r.F1 ⊓ ∃s.F2.' This inference is invalid: an element can fail the conjunction by failing only the ∃s.F2 conjunct. A concrete witness within the size bound is obtained for S = {{1},{2},{3}} (n = k = 3, k' = 8). The concept C = ∃r.∃s.∃s.(∃r.⊤ ⊓ ∃s.A) has size 8 and fits (I,a) and (J,b): after the prefix rss the witness in I is a_1, while R_{rss}(J,b) = {c, b_{2,1}, b_{3,1}}; each of these elements fails ∃r.⊤ ⊓ ∃s.A (the ∃s.A conjunct fails), yet each satisfies ∃s.∃s.⊤. The claimed replacement yields ∃r.∃s.∃s.∃s.∃s.⊤, which is satisfied at b, so Property 2 is not preserved. Since this normalization is exactly the step that extracts a pure L({∃}) fitting from which a hitting set is read off, the proof of (iii)⇒(i), and hence of Theorem 1, is not established as written.","section":"Appendix B, final claim in the proof of Proposition 1"},{"comment":"The proof of Point 1 says that Lemma 6 proves NP-hardness of fitting for L({∀}), L({∀,⊓}), and L({∀,∃,⊓}), and that 'Applying Lemma 1 then yields the same lower bounds for all other fragments from Point 1.' This does not cover fragments containing negation, such as L({∀,¬}) and L({∃,∀}), nor their duals. NP-hardness for a sublanguage does not automatically transfer to a superlanguage, because additional constructors can only make fitting easier. The authors should either extend Lemma 6 to all fragments covered by Point 1 or spell out the additional argument.","section":"Section 4, proof of Theorem 2"},{"comment":"Point 1 is said to follow from [10, Theorem 6] for every fragment containing EL, and Point 2 is proved for L({∃,⊔}), L({∃,⊔,⊓}), and L({∃,∀,⊓}). The parenthetical remark that adding negation to these operator sets leads to full ALC does not transfer the lower bounds to full ALC: an algorithm that returns a most specific (or most general) fitting in the larger language may return a concept outside the subfragment, and the uniqueness/most-general arguments in Lemmas 3, 7, and 8 are stated only for the subfragments. The full-ALC cases of Theorem 3 therefore need an explicit proof or a precise reduction.","section":"Section 4, proof of Theorem 3"}],"minor_comments":[{"comment":"The text 'a ∈ C^I for each (I, a) ∈ C' should read '∈ P'.","section":"Section 2, definition of 'fits'"},{"comment":"The clause 'xi,⊓ → W i<ℓ<k v2,i,ℓ' appears to use the undefined variable v2,i,ℓ; it should be y2,i,ℓ.","section":"Section 5, formula for φ1"},{"comment":"The phrase 'returns always a most general' should be 'always returns a most general'.","section":"Appendix C, Lemma 7"},{"comment":"The expression 'Qℓ−1 i=0 (N − i)' should be written as a product \\(\\prod_{i=0}^{\\ell-1}(N-i)\\).","section":"Appendix B, Equation (7)"},{"comment":"The entry '3.2, ±1.03' contains a stray comma, and 'Nctrer' appears to be a typo for the benchmark name.","section":"Table 1"}],"recommendation":"major_revision","confidential_remarks":"The main theorem is likely true, but the Appendix B gap is in the central proof and cannot be waved away; the authors should be asked to provide a corrected normalization argument. I would not accept in the current form. The implementation and experiments are a strength and appear reproducible."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Let me cut to the chase: the paper's main NP-hardness proof has a real gap, and I want you to know before you invest time. The claimed theorem — size-restricted fitting is NP-complete for every ALC fragment containing ∃ or ∀, even with one positive and one negative example — is exactly the kind of result that would settle a natural open question. The reduction from Hitting Set is clever, and the single-example strengthening is genuinely surprising. The PAC section is careful, and the SAT-based tool ships with code and honest evaluation. Those parts deserve credit.\n\nThe gap is in Appendix B, the final claim of Proposition 1, the step that eliminates conjunctions. When the concept is D_i = ∃r.F1 ⊓ ∃s.F2 and the witness in the positive example sits at d = a_ℓ, the proof replaces D_i with ∃s.∃s.F1, asserting that every element in R_{w_i}(J,b) fails this replacement because it fails the original conjunction. That implication is false. An element can fail the conjunction by failing only the s-conjunct; if the r-conjunct holds, it may well satisfy ∃s.∃s.F1. I checked the concrete witness from the stress-test: for S = {{1},{2}}, n = 2, the concept C = ∃r.∃s.∃s.(∃r.(∃r.⊤) ⊓ ∃s.(∃s.A)) fits the constructed positive and negative examples. With w_i = rss, R_{w_i}(J,b) = {c, b_{2,1}}; both fail the conjunction but both satisfy ∃s.∃s.(∃r.⊤). So the transformed concept is satisfied at b. This is not a minor typo — it's the step that extracts a pure L({∃}) fitting of the required shape from an arbitrary ALC fitting. As written, (iii)⇒(i) is not proved, and the NP-completeness theorem rests on that direction.\n\nI should stress what this doesn't mean. The theorem may well be true; the reduction is otherwise carefully built, and the upper bound is trivial. The PAC non-sample-efficiency results and the SAT-based system stand on their own and are not affected by this gap. The reader's report flagged this exact step as intricate; I'd go further and call it wrong as written.\n\nWho should read this? Anyone working on concept learning in DLs, or on bounded fitting for temporal/database logics, will want to see the single-example hardness claim and the SAT encoding. The paper deserves a serious referee, but the referee must push hard on the normalization. I'd send it out, with the expectation that the authors either repair the proof or weaken the claim.","headline":"The main NP-hardness proof has a real gap in the normalization step; the paper is still worth serious review, but the theorem is not established as written.","tokens_in":28067,"tokens_out":6180,"would_cite":false,"duration_ms":63913,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Finding a smallest ALC concept that separates given positive from negative examples is NP-complete for every fragment containing an existential or universal quantifier, even with a single example of each kind, and efficient PAC learning…","keywords":["description logic ALC","bounded fitting","size-restricted fitting","NP-completeness","PAC learning","SAT solving","concept learning","syntactic fragments"],"falsifier":"Build the two example interpretations from the reduction for a small Hitting Set instance, then exhaustively enumerate all ALC concepts over the signature $\\{r,s,A\\}$ of size at most $n+k+2$. If any concept fits the positive and negative examples yet is not equivalent to a concept of the form $\\exists r.w.A$ with $w\\in\\{r,ss\\}^n$ and at most $k$ occurrences of $ss$, the normalization step underlying Proposition 1 is false and the NP-hardness proof collapses.","tokens_in":27026,"feed_emoji":"🧩","tokens_out":17034,"duration_ms":175846,"temperature":0.7,"pith_summary":"The paper studies bounded fitting for the description logic ALC (class expressions built from conjunction, disjunction, negation, and existential or universal role restrictions): given positive and negative examples, find the smallest concept that separates them. Its main theorem is that this size-restricted fitting problem is NP-complete for ALC and for every syntactic fragment containing an existential or universal restriction, and hardness already occurs with a single positive and a single negative example. It also shows that no such fragment admits an efficient PAC learning algorithm unless $\\mathrm{NP}=\\mathrm{RP}$ or RSA-style encryption can be inverted in polynomial time, and that algorithms which always return the most specific, most general, or minimal-quantifier-depth fitting concept are not sample-efficient, with two exceptions. On the constructive side, it reports a SAT-based implementation with encoding optimizations and an approximation scheme, and gives experiments in which it finds exact fits quickly and matches or exceeds existing concept-learning tools in accuracy. The practical upshot is that exact minimal-concept learning is computationally hard in the worst case, yet feasible enough for real learning tasks.","feed_headline":"One example pair already makes ALC concept fitting NP-complete","feed_subtitle":"Even the simplest separation task in this description logic is hard, so learners must search with SAT solvers.","key_machinery":"Three mechanisms carry the argument. The first is a reduction from Hitting Set: from a collection of sets $S_1,\\dots,S_m$ and a bound $k$, the proof builds two example interpretations $I$ and $J$ made of $r$-paths of length $n$ with $s$-detours that encode which indices each set contains, plus a sink $c$; a fitting concept of size $k' = n+k+2$ exists exactly when a hitting set of size $k$ exists, because any fitting concept must follow one path shape per index and mark the chosen hitting-set elements. The second is the duality lemma: replacing conjunction with disjunction, existential with universal restrictions, and complementing concept-name extensions in the examples transfers fitting problems between dual fragments, so hardness and sample-complexity results for existential fragments automatically apply to universal fragments. The third is the SAT encoding: Boolean variables represent syntax-tree node labels, successor pointers, and whether each node's concept holds at each domain element; clauses enforce well-formed syntax trees and evaluate them over the example interpretation, and the fitting condition is a conjunction of positive and negative literals. The optimizations replace per-concept-name clauses with type variables and canonicalize syntax-tree topologies to break symmetries in the search space.","core_discovery":"The central discovery is Theorem 1: for every set $O$ of ALC constructors that contains at least one of $\\exists$ or $\\forall$, size-restricted fitting for the fragment $L(O)$ is NP-complete. The hardness direction, Proposition 1, is stronger: it holds already for exactly one positive and one negative example, over a signature with two role names and one concept name, and the reduction uses only existential restrictions even when the fragment in question has more constructors. The paper further proves that no fragment $L(O)$ with an existential or universal quantifier admits an efficient PAC learning algorithm under standard assumptions ($\\mathrm{NP} = \\mathrm{RP}$ when the fragment lacks either conjunction or disjunction; otherwise polynomial-time inversion of RSA-style encryption), and that fitting algorithms returning most specific, most general, or minimal-quantifier-depth concepts are not sample-efficient, except that bounded fitting for $L(\\{\\exists,\\sqcup\\})$ is most specific and for $L(\\{\\forall,\\sqcap\\})$ is most general. The implementation contribution is a SAT encoding of syntax trees and their evaluation over a finite interpretation, with type-based clause reduction and syntax-tree-topology symmetry breaking, plus an approximation scheme that maximizes example coverage when no exact fit exists.","pith_inferences":["Editorial inference: the same path-and-detour gadget could give NP-completeness for bounded fitting in richer description logics with inverse roles or number restrictions, since the gadget uses only two functional roles and one concept name.","Editorial inference: the type-based clause reduction suggests that on knowledge bases with few distinct types relative to individuals, SAT-based bounded fitting may scale to much larger data instances than reported; a direct test would fix the type count and grow the domain size.","Editorial inference: the sample-efficiency results imply that concept-learning tools that gravitate toward logically extreme concepts (most specific or most general) may be systematically over- or under-generalizing; a minimal-size objective is a more conservative inductive bias even though computing it is NP-hard."],"forward_implications":["No polynomial-time algorithm can solve size-restricted fitting for any quantifier-containing fragment unless $\\mathrm{P}=\\mathrm{NP}$, so bounded fitting must rely on SAT solvers or other backtracking methods.","The one-positive-one-negative hardness means the difficulty is inherent to choosing the right concept shape, not to gathering many examples.","The duality lemma transfers every complexity and sample-complexity result between existential and universal fragments, making results for existential fragments immediately available for their dual universal fragments.","Unless $\\mathrm{NP}=\\mathrm{RP}$ and RSA-style encryption is secure, no ALC fragment with an existential or universal quantifier has an efficient PAC learning algorithm; bounded fitting's sample guarantees do not come with polynomial runtime.","For most fragments, algorithms that always return the most specific, most general, or minimal-quantifier-depth fitting concept are not sample-efficient; the exceptions are exactly the fragments where bounded fitting is the most-specific learner ($L(\\{\\exists,\\sqcup\\})$) or the most-general learner ($L(\\{\\forall,\\sqcap\\})$)."],"supporting_citations":[{"why":"Gives the EL hardness and most-specific/most-general non-sample-efficiency proofs that this paper generalizes to all ALC fragments.","marker":"[10]"},{"why":"Provides the SAT-based bounded-fitting method and the simulation-dual construction used in the generalization lower-bound proofs.","marker":"[9]"},{"why":"Connects efficient PAC learnability to the fitting problem being in RP, the bridge used to prove Theorem 2.","marker":"[31]"},{"why":"Supplies the cryptographic hardness of learning monotone Boolean formulas, used for fragments containing both conjunction and disjunction.","marker":"[21]"},{"why":"Establishes the Occam-algorithm/PAC generalization guarantee that motivates bounded fitting.","marker":"[4]"},{"why":"Supplies the benchmark data sets used in the approximate-fitting accuracy evaluation.","marker":"[39]"},{"why":"Supplies the SAT solver interface used in the implementation.","marker":"[19]"}],"fun_headline_variants":["Single example pair suffices to make ALC fitting NP-complete","ALC fitting is NP-complete even with a single example pair","Bounded fitting for ALC: NP-hard from just one example pair","SAT solver for ALC fitting, but problem is NP-complete","Even one positive and one negative example makes ALC fitting NP-complete"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that every small concept fitting the two constructed examples can be rewritten, without growing, into the exact path-shaped formula that encodes a hitting set; this rewriting relies on the roles being deterministic functions everywhere except at the starting points and on any subconcept satisfied in the sink also being satisfied throughout the negative example.","fun_headline_variants_meta":{"raw":{"variants":["Single example pair suffices to make ALC fitting NP-complete","ALC fitting is NP-complete even with a single example pair","Bounded fitting for ALC: NP-hard from just one example pair","SAT solver for ALC fitting, but problem is NP-complete","Even one positive and one negative example makes ALC fitting NP-complete"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001042,"raw_usage":{"total_tokens":4367,"prompt_tokens":917,"completion_tokens":3450,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":533,"completion_tokens_details":{"reasoning_tokens":3357}},"tokens_in":533,"tokens_out":3450,"duration_ms":24668,"temperature":1.0,"reasoning_tokens":3357,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T12:25:12.148458+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build the two example interpretations from the reduction for a small Hitting Set instance, then exhaustively enumerate all ALC concepts over the signature $\\{r,s,A\\}$ of size at most $n+k+2$. If any concept fits the positive and negative examples yet is not equivalent to a concept of the form $\\exists r.w.A$ with $w\\in\\{r,ss\\}^n$ and at most $k$ occurrences of $ss$, the normalization step underlying Proposition 1 is false and the NP-hardness proof collapses.","supporting_citations":[{"cited_title":"SAT-Based PAC Learning of Description Logic Concepts","cited_arxiv_id":"2305.08511","evidence_quote":"Gives the EL hardness and most-specific/most-general non-sample-efficiency proofs that this paper generalizes to all ALC fragments."},{"cited_title":"Journal of the ACM (JACM)41(1), 67–95 (1994)","cited_arxiv_id":null,"evidence_quote":"Supplies the cryptographic hardness of learning monotone Boolean formulas, used for fragments containing both conjunction and disjunction."},{"cited_title":"Semantic Web10(2), 231–245 (2019)","cited_arxiv_id":null,"evidence_quote":"Supplies the benchmark data sets used in the approximate-fitting accuracy evaluation."}],"review_version":1}