{"id":"94eb55bd-633b-4766-9536-7d10709b2303","arxiv_id":"2507.09324","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Every finite relation algebra with at most four atoms has a network satisfaction problem that is either in P or NP-hard, with the paper determining which.","lead":"The paper classifies the computational difficulty of the network satisfaction problem for every finite relation algebra with at most four atoms. Each such problem is either solvable in polynomial time or NP-hard, and the paper identifies which case holds.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Unshipped computer verifications underpin the normal-representation and atom-structure classifications; a wrong verification could misclassify algebras and break the dichotomy.","rationale":"The paper's main theorem is a dichotomy for a concrete finite list of relation algebras, established through a large case analysis. Most P and NP-hard cases have explicit arguments or cited theorems, and the many explicit representations and gadget reductions are independent evidence of substantial correctness. The weakest point is where the authors delegate to unlisted computation. This is not an internal inconsistency, but a verification gap that is load-bearing because the exhaustive classification is the theorem itself: if the normal-representation computer check is wrong, some algebra's normality, and hence any hardness or tractability proof relying on that normality, could fail. Remark 6.11 is less load-bearing for the NSP dichotomy because NP-completeness of CSP(A0) alone does not imply NP-hardness of NSP(A); the explicit hardness proofs in Section 5 already cover the NP-hard algebras. However, the remark is still evidence that the atom-structure classification was not fully hand-checked. The reader's weakest assumption identifies exactly this same concern, and the appropriate disposition remains conditional: accept once the computational checks are made available or independently formalized. Therefore the reader's verdict of CONDITIONAL should stand unchanged, with the concrete test above as the condition for full acceptance.","tokens_in":66558,"tokens_out":17996,"duration_ms":217160,"concrete_test":"Release the verification programs and their full output, or independently recompute the following: for every one of the 102 integral relation algebras with four atoms (using the allowed-triple tables given in the paper), run an exhaustive check of the AP(k+1,k,k+1) criterion of Theorem 2.39, and compare the resulting set of normal-representable algebras with list (4.1) and with the counterexamples in Figure 7. Additionally, for every algebra not proved polynomial-time in Section 6, verify via Theorem 2.11 that CSP(A0) is NP-complete by enumerating binary symmetric, majority, and minority polymorphisms. If both checks reproduce the paper's tables, the concern is settled.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The classification that drives Theorem 1.4 is exhaustive only if the two computer checks are correct. Section 4.3 states that the normal-representation condition of Theorem 2.39 was 'verified in all cases by a computer program', and Remark 6.11 states, without proof, that a computer program verified NP-completeness of CSP(A0) for every atom structure not treated in Section 6. No code, data, or certificates are provided. These checks are load-bearing because the paper uses them to assign representability and complexity status to algebras; an error in either program could move an algebra from the P side to the NP-hard side (or vice versa) and invalidate Theorem 1.4. The explicit representations listed for many algebras mitigate the concern for normal representability but do not eliminate it, since the paper does not give complete hand proofs that every listed representation is normal; and Remark 6.11 is explicitly unproved. I am not alleging the checks are wrong; the issue is that the central claim is not independently verifiable from the paper as it stands.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper extends the Andreka-Maddux classification of relation algebras with at most three atoms and the Hirsch-Cristiani complexity dichotomy to all finite relation algebras with at most four atoms. The main result, Theorem 1.4, states that for every such algebra A the network satisfaction problem NSP(A) is either in P or NP-hard. The proof proceeds by reducing to simple integral algebras, using Maddux's exhaustive lists, and then classifying each algebra according to whether it has a normal, fully universal, bounded-square, or merely universal representation. Polynomial-time algorithms are given for the tractable cases, including divide-and-conquer algorithms for 24_65 and 17_37, and NP-hardness is proved by a variety of methods, including reductions from promise CSPs such as PCSP(K3,K5). The paper also proves Theorem 1.5, confirming the Bodirsky-Pinsker tractability conjecture for the normal representations of these algebras.","tokens_in":1453,"tokens_out":1601,"duration_ms":178854,"significance":"If the classification is correct, this is a substantial step beyond the three-atom case and provides a rich testbed for the infinite-domain CSP programme. The paper contains several original and reusable technical contributions: the combinatorial characterization of fully universal square representations, the use of promise CSP hardness for network satisfaction problems, the explicit representations for 51_65, 56_65, 39_65 and 62_65, and the polynomial-time algorithms for 24_65 and 17_37. The detailed tables (Tables 4 and 5) are valuable as a reference. However, the exhaustive character of the main theorem depends on two computer verifications that are not supplied to the reader, and the paper itself flags one of them as without proof. This reproducibility gap is the main obstacle to accepting the paper in its present form.","major_comments":[{"comment":"The classification of which at-most-four-atom algebras have normal representations is load-bearing for Theorem 1.4, but it is justified by the sentence 'we verified the condition in all cases by a computer program,' with no program, source code, data, or certificates supplied. Later arguments that apply only to algebras with normal representations (e.g., Theorems 5.8 and 5.10 and Propositions 5.16-5.21) inherit this classification. The counterexample rows in Figure 7 are also asserted without a displayed verification for each row. I request either a reproducible artifact (program plus output or certificates) or complete hand-verifiable proofs for the inclusions in (4.1) and for each of the fifteen counterexample rows in Figure 7.","section":"Section 4.3, list (4.1) and Figure 7"},{"comment":"The paper states, 'We mention (without proof) that the CSP of the atom structure of every relation algebra with at most four atoms not mentioned in this section is NP-complete. To check this we used a computer program to verify the conditions given in Theorem 2.11.' No proof, program, or certificates are provided. The displayed hardness proofs in Section 5 do not appear to invoke this remark, but the remark is presented as an exhaustive classification fact and should be either proved, removed, or accompanied by a reproducible verification; otherwise the reader cannot determine whether the atom-structure tractability arguments are complete.","section":"Remark 6.11"}],"minor_comments":[{"comment":"In the displayed pp-formula, the atom 'x4' appears in the conjunct '(r union Id)(z2,x4)', but x4 is not quantified and does not occur in the gadget description; this is presumably a typo for 'z4' (or the quantifier list should be amended).","section":"Section 5.6, Proposition 5.17"},{"comment":"The assertions that 39_65 fails AP(3,2,4) and 62_65 fails AP(3,2,6) are justified only by pointing to a figure. For reproducibility, please state explicitly which amalgamation instances fail and verify that the displayed labels respect the allowed triples.","section":"Section 4.6, Propositions 4.13 and 4.14"},{"comment":"The proof of representability of 56_65 verifies only the composition b composed with b equals a union b union Id and says the other cases are very similar. Since this representation is used in Corollary 5.27, I recommend including a complete composition table or an appendix with the remaining cases.","section":"Section 4.7.3, Proposition 4.26"},{"comment":"The claim that 62_65 has AP(5) but not AP(6), and that it is the unique four-atom algebra with this behavior, is stated without proof. If this remark is only about the optimality of Theorem 2.39, please label it as such; if it is used in the classification, a proof is needed.","section":"Remark 4.4"},{"comment":"The table lists NSP(56_65) as NP-complete, citing the unpublished preprint [BGPJ+25] for containment in NP. Since Theorem 1.4 only asserts NP-hardness for this case, the table should clearly mark the NP-completeness entry as relying on an external preprint, or the proof should be included.","section":"Tables 4 and 5, row for 56_65"}],"recommendation":"major_revision","confidential_remarks":"The main classification is likely correct and valuable, but the two computer verifications should be supplied as supplementary material or replaced by hand-checkable proofs before the paper can be considered complete. The dependence on [BGPJ+25] for the NP-completeness entry of 56_65 should also be made transparent. I recommend major revision rather than rejection because the concern is fixable by adding artifacts or proofs."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this paper really does the thing it says. It pushes the NSP dichotomy for relation algebras from at most three atoms to all 102 integral four-atom algebras, and it does so with substantive new tools—promise-CSP hardness reductions (PCSP(K3,K5)), pp-construction arguments for normal representations, and genuinely non-obvious polynomial-time algorithms (notably 24_65 and 17_37). The representation survey has independent value: explicit normal, fully universal, and bounded square representations for a large part of the four-atom list, with a clean combinatorial criterion for fully universal square representations. The tables in Section 8 make the classification easy to navigate.\n\nThe math looks careful. I checked several of the reductions and algorithms at random and they are detailed enough to follow. The dependence on earlier work (BK20, BK22, BK23, and Maddux's lists) is legitimate: those are published results, and the new hardness reductions start from independent NP-hard problems. I do not see a circular step.\n\nThe real soft spot is the same one the reader flagged: two computer checks are asserted but not shipped. Section 4.3 says the normal-representation condition of Theorem 2.39 was verified by a computer program; Remark 6.11 says a computer program verified NP-completeness of the remaining atom-structure CSPs. No code, data, or certificates. Since these lists feed into both the representability classification and some hardness proofs, the dichotomy as stated is not fully independently verifiable from the paper. I want to be proportionate: this is a verifiability gap, not evidence of error. The normal-representation list is partially supported by explicit representations and by the counterexample diagrams in Figure 7; the finite conditions could be certified mechanically. Remark 6.11 is a completeness statement about the atom-structure method and, as far as I can tell, less load-bearing for Theorem 1.4 than the normal-representation list. Still, both should be made checkable.\n\nTwo smaller notes. The claim for 56_65's NP-containment is deferred to a companion paper; fine, but it makes the paper not fully self-contained. And the phrase “it is easy to see (by hand; we verified the condition in all cases by a computer program)” is doing a lot of work in Section 4.3; I would prefer the verifier to be explicit.\n\nWho this is for: anyone working on relation algebras, infinite-domain CSPs, or homogeneous structures. It deserves a serious referee—the referee should ask for the computer checks as a condition, but the paper should be sent out. I would bring it to a reading group, and while I wouldn't cite it in my own work in the next year unless I move into this area, it's a solid contribution to its subfield.","headline":"Genuine boundary-crossing classification: full NSP dichotomy for four-atom relation algebras with new hardness and tractability techniques; the main caveat is unshipped computer verifications behind two classification claims.","tokens_in":67276,"tokens_out":3869,"would_cite":false,"duration_ms":46479,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03G15","68Q25"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that the network satisfaction problem of every finite relation algebra with at most four atoms is either in polynomial time or NP-hard, and it determines the representation type of each of the 102 four-atom integral…","keywords":["network satisfaction problem","relation algebra","NP-hardness dichotomy","constraint satisfaction","normal representation","fully universal representation","atom structure","polynomial-time algorithm"],"falsifier":"Re-run the two finite checks independently and compare: for each algebra claimed to have a normal representation, verify the amalgamation condition of Theorem 2.39 by hand or with a certified program, and for each atom structure claimed to have an NP-complete CSP, verify the absence of the binary symmetric, majority, or minority polymorphism required by Theorem 2.11; a single algebra failing its claimed condition would overturn the classification, as would a four-atom algebra whose network satisfaction problem is provably neither in P nor NP-hard.","tokens_in":66370,"feed_emoji":"🧮","tokens_out":11066,"duration_ms":116721,"temperature":0.7,"pith_summary":"The paper proves a dichotomy for the network satisfaction problem of relation algebras with at most four atoms: every such problem is either solvable in polynomial time or NP-hard, with no intermediate complexity. A network satisfaction problem asks whether a finite set of binary constraints, labelled by the algebra's elements, can be realised in some representation of the algebra. The proof extends the earlier three-atom classification and rests on a complete census of the 102 integral four-atom algebras, deciding for each whether it is representable and whether the representation can be chosen normal, fully universal, bounded square, or not at all. It also confirms the tractability conjecture stated in the introduction for every normal representation in the list. Along the way the paper introduces new hardness reductions from a promise graph-colouring problem and new polynomial-time divide-and-conquer algorithms for concrete algebras.","feed_headline":"Every four-atom relation algebra's network problem is P or NP-hard","feed_subtitle":"The dichotomy extends the three-atom case and pins down representations for all 102 integral algebras.","key_machinery":"The central object is the network satisfaction problem NSP(A) for a finite relation algebra A, and the argument is organized around a hierarchy of representation types: normal, fully universal square, fully universal, bounded square, and non-representable. The load-bearing mechanism is the census of all integral relation algebras with at most four atoms, matched against transfer theorems that convert representation type into complexity: Theorem 2.39 characterizes normal representability by an amalgamation property of consistent atomic networks, Corollary 2.41 characterizes fully universal square representability by the same property together with joint embedding, and Lemma 3.4 turns bounded square representations into NP-completeness. Hardness is propagated through the 2-cycle product construction, primitive-positive interpretations, and a reduction from a promise graph-coloring problem; tractability is obtained by path consistency, by polynomial-time algorithms on the atom structure, and by new divide-and-conquer procedures for two of the algebras.","core_discovery":"The central discovery is that the dichotomy between polynomial-time solvability and NP-hardness holds for the network satisfaction problem of every finite relation algebra with at most four atoms. Along the way the paper gives a complete census of the 102 integral four-atom algebras, deciding for each whether it is representable and, if so, whether the representation can be chosen normal (square, fully universal, and homogeneous), fully universal square, fully universal, or of bounded square size. Representable algebras with bounded square size get NP-complete NSP by a guessing argument; normal and fully universal cases are dispatched by existing criteria; the residual cases are settled by gadget reductions, including a reduction from the promise problem of deciding whether a graph is 3-colorable or not even 5-colorable. For normal representations, the paper confirms the tractability conjecture stated in its introduction: whenever the representation does not primitive-positively construct the Boolean not-all-equal relation, the problem is in P. It also shows that the NSP of every algebra in the list except 56 65 is in NP, with the exceptional case covered by a separate publication.","pith_inferences":["The two computer checks described in Section 4.3 and Remark 6.11 are the natural targets for independent certification; producing machine-checkable certificates for them would turn the classification into a fully verified result.","The reduction template of Proposition 5.26—two symmetric atoms p and q with (p,p,p) and (q,q,q) forbidden and (p,q,q) allowed—gives a table-lookable sufficient condition for NP-hardness that is likely to transfer to algebras with more atoms.","The paper's remark that five-atom algebras already number in the thousands suggests that a direct extension will require automated amalgamation checks with independently verifiable certificates, rather than the handwritten case analysis used here.","For fully universal representations, the NSP coincides with the CSP of the atom structure, so the boundary between P and NP-hard in this family coincides with the presence or absence of a binary symmetric, majority, or minority polymorphism on the atom structure; that reformulation may guide searches among larger algebras."],"forward_implications":["Every relation algebra with at most four atoms has an NSP that is either polynomial-time solvable or NP-hard, so no Ladner-style intermediate complexity appears in this family.","For every normal representation in the classification, failure to pp-construct the not-all-equal relation implies polynomial-time solvability, confirming the paper's tractability conjecture on this class.","Of the 102 integral four-atom algebras, 31 are non-representable and the remaining 71 are representable, with their representation type (normal, fully universal square, fully universal, or bounded square) determined.","Several previously unclassified algebras receive explicit polynomial-time algorithms, including the 3-edge-coloured clique algebra 24 65 and the quasi-transitive orientation algebra 17 37.","The NSP of every algebra in the list except 56 65 is shown to be in NP; the remaining case is covered by a separate paper cited in the text."],"supporting_citations":[{"why":"Provides the base classification of relation algebras with at most three atoms, including their representability, which the four-atom extension builds on.","marker":"[AM94]"},{"why":"Gives the previous P-or-NP-hard classification for small relation algebras that this paper extends to four atoms.","marker":"[CH04]"},{"why":"Supplies the exhaustive lists of integral relation algebras with up to four atoms that the census and case analysis are based on.","marker":"[Mad06b]"},{"why":"Provides the amalgamation criterion (Theorem 2.39) used to decide normal representability of the algebras.","marker":"[Bod18]"},{"why":"Underlies the construction of fully universal representations via amalgamation properties, as formalized in Corollary 2.41.","marker":"[Com83b]"},{"why":"Gives the promise graph-coloring hardness result used in Proposition 5.26 to prove NP-hardness for several four-atom algebras.","marker":"[BKO19]"},{"why":"Supplies hardness criteria for algebras with normal representations and finitely many equivalence classes, which are invoked in Sections 5.3 and 5.4.","marker":"[BK20]"},{"why":"Provides the decomposition theorem for quasi-transitive oriented graphs that underlies the polynomial-time algorithm for algebra 17 37.","marker":"[BJH95]"}],"fun_headline_variants":["Four-atom relation algebras: NSP always P or NP-hard","Dichotomy for four-atom relation algebras: P or NP-hard","All ≤4-atom relation algebras have NSP in P or NP-hard","NSP dichotomy for every relation algebra with ≤4 atoms","Network problem for ≤4-atom algebras: P or NP-hard"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The classification depends on two computer verifications that are described but not supplied with code, data, or certificates: the check of the normal-representability condition of Theorem 2.39 for the algebras listed in (4.1), and the check of the atom-structure polymorphism conditions reported in Remark 6.11; an error in either would undermine the lists of representations and the complexity labels built on them.","fun_headline_variants_meta":{"raw":{"variants":["Four-atom relation algebras: NSP always P or NP-hard","Dichotomy for four-atom relation algebras: P or NP-hard","All ≤4-atom relation algebras have NSP in P or NP-hard","NSP dichotomy for every relation algebra with ≤4 atoms","Network problem for ≤4-atom algebras: P or NP-hard"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000965,"raw_usage":{"total_tokens":4071,"prompt_tokens":876,"completion_tokens":3195,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":492,"completion_tokens_details":{"reasoning_tokens":3103}},"tokens_in":492,"tokens_out":3195,"duration_ms":27433,"temperature":1.0,"reasoning_tokens":3103,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T17:58:56.822977+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Re-run the two finite checks independently and compare: for each algebra claimed to have a normal representation, verify the amalgamation condition of Theorem 2.39 by hand or with a certified program, and for each atom structure claimed to have an NP-complete CSP, verify the absence of the binary symmetric, majority, or minority polymorphism required by Theorem 2.11; a single algebra failing its claimed condition would overturn the classification, as would a four-atom algebra whose network satisfaction problem is provably neither in P nor NP-hard.","supporting_citations":[],"review_version":1}