{"id":"f2d44c2e-e01b-4353-a5cc-7d6ad3d9b694","arxiv_id":"2506.14042","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"high","formal_verification":"none","parameter_count":0,"one_line_summary":"Independent set, vertex cover, k-coloring and clique admit CNF encodings with O(n^2/log n) clauses, and the disjoint-intervals encoding needs only O(n^2 log n) clauses.","lead":"Graph problems like independent set and k-coloring can be encoded into CNF with O(n^2/log n) clauses instead of the usual quadratic number, using edge coverings by complete bipartite graphs. The same covering technique gives a compact encoding for interval scheduling, with reported applications to string compression.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 22's x-edge budget is internally inconsistent: for ℓ<r the graph G_{ℓ,r} is complete on b^2 crossing intervals, not I_{2b}, and the clause sum switches from k^2 to k; the claimed 26n^2 lg n bound is not established as written.","rationale":"The paper's central subquadratic result, Theorem 10, rests on the cited Chung-Erdős-Spencer theorem; that external dependence is worth verifying, but it is a published theorem and the stated form is plausible. The more immediate and internally checkable problem is in Theorem 22, the interval-graph encoding, which the reader also flagged in the rationale. The x-edge case has a visible inconsistency: the definition of x-edges in Lemma 21, combined with a fixed pair of blocks ℓ<r, produces a complete graph on the b^2 crossing intervals, not the interval graph I_{2b}; moreover, the proof switches from k^2 to k in the final count. A small isomorphism check and a recount of the x-edge clauses would settle whether the proof's 26n^2 lg n bound is correct or whether the constant must be larger. This does not change the overall verdict: the result should remain conditional until the x-edge accounting is repaired, but the asymptotic O(n^2 lg n) claim may well survive with a corrected constant. Therefore the reader's CONDITIONAL verdict is unchanged, and the reader's weakest-assumption choice is only partially aligned with this concern.","tokens_in":23040,"tokens_out":28474,"duration_ms":290531,"concrete_test":"Run a small script for n=60, b=10, k=6, fixing (ℓ,r)=(1,2). Enumerate the intervals intended by the x-edge bullet under both readings: (a) only intervals [i,j] with B(i)=1 and B(j)=2, and (b) all intervals whose endpoints lie in blocks 1 or 2. Build the adjacency graph for each reading and test isomorphism to I_{20} and to K_{100}. Then recompute the total x-edge clause sum over all (ℓ,r) under each reading and compare with 26·60^2·lg 60 ≈ 245,000 and with O(n^2 lg n). This settles whether G_{ℓ,r} is I_{2b} or K_{b^2}, and whether the clause count in the proof is the k^2 or k version.","verdict_should_be":"UNCHANGED","load_bearing_attack":"In Theorem 22 (Section 4.2), the x-edge case asserts that for fixed blocks ℓ<r the graph G_{ℓ,r} is isomorphic to I_{2b}, and counts k^2·(104b^2 lg b + 104) clauses. But Lemma 21 defines an x-edge by B(i1)=B(i2) and B(j1)=B(j2). For ℓ<r, that fixes every vertex to be an interval [i,j] with B(i)=ℓ and B(j)=r; there are b^2 such vertices and any two intersect, so G_{ℓ,r} is K_{b^2}, not I_{2b}. If instead G_{ℓ,r} includes all intervals with endpoints in blocks ℓ and r, then its edges are not all x-edges; the extra edges are s- and f-edges that Lemma 21 assigns to other cases, so attributing I_{2b} to x-edges double-counts. The arithmetic also switches from k^2 choices to k inside the total sum: the displayed total is k(104b^2 lg b + 104) + ... while the preceding paragraph says k^2 choices. On the k^2 reading, x-edges alone contribute 104n^2 lg b = O(n^2 lg n), so the stated constant 26n^2 lg n is not obtained; on the k reading, the count does not match the construction. Either way, the exact bound in Theorem 22 is not established as written, although the O(n^2 lg n) asymptotics may survive with repaired accounting.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies compact CNF encodings for graph problems. It proves that the independent-set property of any n-vertex graph can be encoded with O(n^2/lg n) clauses using biclique coverings (Theorem 10), and it extends this to vertex cover, clique, and, purportedly, to k-coloring. The paper then focuses on the class of full interval graphs I_n, whose disjoint-interval independent-set property is shown to be encodable with O(n^2 lg n) clauses (Theorem 22), and it applies this encoding to a non-preemptive scheduling problem, reducing the clause count to O(NMT + MT^2 lg T) (Theorem 23). It also contains a formal result on Bounded Variable Addition for at-most-one constraints (Proposition 16), a lower bound for k-CNF encodings (Proposition 17), and experimental results on string-compression via straight-line programs.","tokens_in":23400,"tokens_out":29068,"duration_ms":272269,"significance":"If the technical issues are repaired, the paper makes a solid contribution: it gives a clean, parameter-free framework for covering-based encodings, a surprising subquadratic encoding for dense graphs built on a known biclique-covering theorem, and a genuinely novel encoding for interval-graph constraints that has a concrete scheduling application. The explicit BVA proof for AMO and the discussion of practical applications add value. The manuscript is clearly written and the ideas are well motivated. The main caveat is that two load-bearing arguments currently contain errors: the x-edge accounting in Theorem 22 is internally inconsistent, and the k-coloring extension is missing a necessary constraint.","major_comments":[{"comment":"The claim that, for ℓ<r, the graph G_{ℓ,r} is isomorphic to I_{2b} is incorrect. Every vertex of G_{ℓ,r} is an interval [i,j] with B(i)=ℓ and B(j)=r, so there are b^2 vertices, and since every position in block ℓ is smaller than every position in block r, any two such intervals intersect; hence G_{ℓ,r} is the complete graph K_{b^2}, not I_{2b}, which has 2b^2−b vertices and is not complete. In the same paragraph the accounting switches from \"k^2 choices\" for (ℓ,r) to a term k(104b^2 lg b + 104) in the final sum, and the simplification 26(2b)^2 lg(2b) = 104b^2 lg b + 104 is arithmetically wrong (it should be 104b^2 lg b + 104b^2). Consequently the claimed bound 26n^2 lg n is not established as written. The asymptotic O(n^2 lg n) may survive if K_{b^2} is encoded directly with an AMO encoding of O(b^2) clauses, but the proof must be reworked and the constants recalculated.","section":"Section 4.2, Theorem 22, x-edges paragraph"},{"comment":"The proposed encoding of k-coloring as a conjunction of k formulas obtained from Theorem 10 is not sound as written. The independent-set constraints for each color class do not force every vertex to receive at least one color, so an assignment leaving some vertex uncolored satisfies the formula even when the graph is not k-colorable (e.g., K_3 with k=2). To repair this, the encoding must include at-least-one clauses (x_{v,1}∨⋯∨x_{v,k}) for each vertex v; these add O(n) clauses and preserve the claimed asymptotic bound, but the omission is a correctness error that must be corrected in the statement and proof.","section":"Section 2.2, k-coloring bullet"}],"minor_comments":[{"comment":"The assertion that after removing pure literals the number of variables m is at most the number of clauses t is only valid for 2-CNF; for general fixed k one only gets m ≤ kt/2. The counting argument still yields the Ω(n^2/lg n) bound with an adjusted constant, but the text should be corrected.","section":"Section 3.2, Proposition 17"},{"comment":"The sentence claiming that the AMOPE constraints ensure that no two tasks are assigned to the same machine during the same time interval is imprecise: the AMOPE constraints handle only tasks of identical duration starting at the same time, while general overlaps are prevented by the disjoint-interval encoding on the y-variables.","section":"Section 4.3, Theorem 23 proof"},{"comment":"There is a typo in the abstract: \"Mayank and Modal\" should be \"Mayank and Mondal\" to match the reference and the main text.","section":"Abstract and Section 4.3"},{"comment":"The Python validation script does not detect multiply-classified edges: if more than one flag is true, it returns the first matching case without reporting the ambiguity. The lemma appears correct by the decision tree in Figure 4, but the script as presented would not catch a violation of the \"exactly one case\" claim.","section":"Appendix B, Code 1"},{"comment":"The sentence about O(n^2 (lg n)^{-4}) cliques of size 2 being \"safely ignore since this is already O(n^2 lg n)\" is confusing; the intended statement is that their contribution to the sum of vertex counts is O(n^2/lg^4 n), which is absorbed by the main O(n^2/lg n) term.","section":"Section 2.1, Proposition 6 proof"},{"comment":"Theorem 9 is cited in the sum-of-vertex-counts form, whereas standard statements of the Chung–Erdős–Spencer result are usually given as bounds on the number of bicliques in a covering or partition. A brief proof sketch or a more precise citation would help the reader verify that the stronger measure follows from the known theorem.","section":"Section 2.2, Theorem 9"}],"recommendation":"major_revision","confidential_remarks":"The paper is interesting and likely correct in its main asymptotic claims after repair. The two major issues are both local: the x-edge case of Theorem 22 needs a corrected structural claim and arithmetic, and the k-coloring extension needs the at-least-one clauses. I see no reason to doubt the novelty or scope. One editorial note: a key application relies on a paper under review (Bannai et al., 2025), which makes the practical contribution somewhat contingent on an external, not yet publicly verified result; the authors may want to clarify what is available from that manuscript."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The headline: this paper is worth a referee. The biclique-covering encoding for independent set, vertex cover, coloring, and clique at O(n^2/log n) clauses is a real contribution, and the recursive block encoding for interval graphs is a clever primitive with an interesting scheduling byproduct. The central soft spot is Theorem 22: as written, the x-edge case is mishandled. For fixed blocks ℓ<r, the graph G_{ℓ,r} is a complete graph on b^2 vertices, not I_{2b}; and the arithmetic switches between k^2 and k. So the exact 26n^2 lg n bound is not established. The asymptotics may survive — a complete graph can be encoded with O(b^2) clauses, which actually improves the count — but the proof needs repair. The scheduling proof also appears to have a corrupted final sentence and attributes to the AMO constraints a property they do not have; the disjoint-interval constraint is the one doing the work. That is fixable.\n\nWhat is good: the reduction from clique coverings to biclique coverings is simple and clearly explained. Proposition 16 (BVA for AMO) gives a formal proof of an empirical observation. The interval propagation trick in Section 4.1 is a nice standalone idea. The paper is honest about its dependence on Chung–Erdős–Spencer and explicitly notes that the quoted form (sum of |V(B)|) is stronger than the usual biclique-count form; that should be checked against the original source before the main theorem is fully accepted. The counting lower bound in Proposition 17 looks plausible.\n\nProportionate verdict: the only load-bearing flaw is the proof of Theorem 22, plus the sloppy scheduling write-up. Everything else is either solid or needs minor polishing. The main biclique-covering result is likely sound and of independent interest to the SAT and proof-complexity community. This deserves a serious referee who can verify the CES theorem and patch the interval accounting; the paper should not be desk-rejected. I would not cite Theorem 22 as it stands, but I would cite the biclique-covering encoding once the external theorem is confirmed.","headline":"A genuinely new and elegant idea for compact SAT encodings, with the main theorem likely sound and a key proof in the interval section that is currently broken.","tokens_in":23954,"tokens_out":9397,"would_cite":true,"duration_ms":90645,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B05","05C69","05C70","68Q17","68Q25"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that dense graph problems such as independent set, vertex cover, $k$-coloring, and clique admit CNF encodings with $O(n^2/\\lg n)$ clauses, and that interval graphs admit encodings with $O(n^2\\lg n)$ clauses.","keywords":["CNF encodings","biclique covering","independent-set property","interval graphs","SAT","bounded variable addition","scheduling","at-most-one constraints"],"falsifier":"Check the original statement of the 1983 biclique-covering theorem to confirm it bounds $\\sum |V(B)|$ and not just the number of bicliques; if the bound only applies to the number of bicliques, compute optimal biclique coverings for all graphs up to $n=12$ by exhaustive search and see whether $\\sum |V(B)|$ can be made $O(n^2/\\lg n)$ in every case. For the interval-graph theorem, build the formula from Theorem 22 for $n=64$, conjoin clauses forcing two overlapping intervals to both be selected, and check satisfiability: if the solver says satisfiable, the encoding is unsound.","tokens_in":22823,"feed_emoji":"📉","tokens_out":16837,"duration_ms":143157,"temperature":0.7,"pith_summary":"The paper establishes that several common graph problems—independent set, vertex cover, $k$-coloring, and clique—can be turned into CNF formulas (conjunctive normal form, the standard input to SAT solvers) of size $O(n^2/\\lg n)$ for every $n$-vertex graph, even dense graphs whose direct edge-by-edge encoding costs $\\Omega(n^2)$ clauses. The mechanism is a biclique covering: cover the edges by complete bipartite subgraphs, encode each biclique with one auxiliary variable and a linear-in-its-vertices number of clauses, and invoke a known 1983 theorem that bounds the total vertex bill of such a covering by $O(n^2/\\lg n)$. The paper also proves a matching $\\Omega(n^2/\\lg n)$ lower bound for constant-width ($k$-CNF) encodings, and a separate recursive block encoding for interval graphs that encodes pairwise-disjoint intervals in $O(n^2 \\lg n)$ clauses despite the graph having $\\Omega(n^4)$ edges. If correct, the results show that the quadratic size of standard encodings is not inherent, and they yield smaller encodings for scheduling and string-compression problems.","feed_headline":"Dense graph SAT encodings drop below quadratic size","feed_subtitle":"Biclique coverings replace one clause per edge, shrinking independent-set, coloring, and scheduling encodings.","key_machinery":"The biclique-covering encoding: a family of complete bipartite subgraphs of $G$ whose edge sets cover $E(G)$, each represented by an auxiliary variable $y$ and clauses $\\neg x_v \\lor y$ for $v\\in A$ and $\\neg y \\lor \\neg x_v$ for $v\\in B$, so the cost of the covering is $\\sum |V(B)|$. The lower-bound argument counts distinct $k$-CNF formulas and shows some graph must need $\\Omega(n^2/\\lg n)$ clauses. The interval part uses a second gadget, the interval-propagation trick: auxiliary variables $z_{i,j}$ with $O(n^2)$ clauses force $z_{i,j}$ to be true exactly when some selected interval contains $[i,j]$, and a recursive block decomposition with $\\Theta(\\lg n)$ blocks classifies every edge of $I_n$ into five types ($x,y,s,f,m$), each handled by its own auxiliary variables; the recursion over blocks yields the $O(n^2\\lg n)$ bound.","core_discovery":"For every graph $G$ on $n$ vertices, the independent-set property has a CNF encoding with $O(n^2/\\lg n)$ clauses, obtained by covering the edge set with bicliques and writing, for each biclique $K_{a,b}$, the $a+b$ clauses $\\bigwedge_{v\\in A}(\\neg x_v \\lor y)\\land \\bigwedge_{v\\in B}(\\neg y \\lor \\neg x_v)$; a set is independent in $G$ exactly when its intersection with every biclique of the covering is independent in that biclique. By flipping polarities, the same construction encodes vertex cover, and by taking $k$ copies and complementation it encodes $k$-coloring and clique. The total clause count is $\\sum_B |V(B)|$, which the cited biclique-covering theorem bounds by $O(n^2/\\lg n)$; the paper notes the construction becomes algorithmic via a polynomial-time biclique-finding procedure. For interval graphs, the paper proves that the independent-set property of the graph whose vertices are all intervals $[i,j]\\subseteq [1,n]$, with edges for overlapping intervals, can be encoded in at most $26n^2\\lg n$ clauses using a block decomposition and an interval-propagation gadget, reducing a scheduling encoding from $O(NMT^2)$ to $O(NMT+MT^2\\lg T)$ clauses.","pith_inferences":["The biclique-covering reduction transfers to other NP problems encoded through pairwise-incompatibility graphs: any CSP whose conflict graph admits a cheap biclique covering inherits the subquadratic clause bound, so the result is a recipe rather than a one-off construction.","Because the interval encoding is hierarchical (blocks, then sub-blocks), it suggests a generic 'calendar' decomposition for temporal constraints: group events by coarse time windows, then refine; a practical heuristic could choose block sizes adaptively instead of the uniform $\\lg n$ used in the proof.","The lower-bound argument only applies to constant-width clauses; whether general auxiliary-variable encodings (like BVA or extended resolution) can beat $\\Omega(n^2/\\lg n)$ remains open, and the paper's BVA-on-top-of-covering experiments hint that recursion through auxiliary variables is where further compression would come from.","The gap between the $n^2/\\lg n$ covering bound and the $n\\lg n$ achievable for complete graphs suggests the true worst-case encoding size for independent sets likely lies between these two bounds; a matching general lower bound would require techniques beyond counting $k$-CNF formulas."],"forward_implications":["SAT solvers can receive dense independent-set, vertex-cover, $k$-coloring, and clique instances with asymptotically fewer clauses than the direct edge-by-edge encoding, so the quadratic barrier for those problems is not inherent.","The success of Bounded Variable Addition as a preprocessing step gets a formal explanation: BVA can re-encode pairwise at-most-one constraints into $O(n)$ clauses, and its grid-product moves subsume the biclique-covering re-encoding, so it provably compresses the direct encodings that the covering results show are wasteful.","For any fixed clause width $k$, some graphs require $\\Omega(n^2/\\lg n)$ clauses for their independent-set property, so within $k$-CNF the new encoding is asymptotically optimal.","Non-preemptive scheduling on $M$ machines with horizon $T$ moves from $O(NMT^2)$ clauses to $O(NMT+MT^2\\lg T)$, so SAT-based schedulability analysis scales to larger task counts and time horizons.","The interval-graph result improves the bottleneck of the SLP string-compression encoding, cutting clause counts by an order of magnitude on Fibonacci strings and similar benchmarks in the paper's experiments."],"supporting_citations":[{"why":"Supplies the load-bearing external theorem: every graph on $n$ vertices has a biclique covering with total vertex count $O(n^2/\\lg n)$, from which Theorem 10 follows.","marker":"Chung et al. (1983)"},{"why":"Gives a polynomial-time algorithm that computes a biclique covering with the asymptotic guarantee, making Theorem 10 constructive.","marker":"Mubayi and Turán (2010)"},{"why":"Introduces the clique-covering encodings that the paper generalizes to biclique coverings and uses as a comparison baseline.","marker":"Ignatiev et al. (2017)"},{"why":"Earliest clique/biclique covering idea for binary constraints; the paper contrasts its $\\Theta(n^2)$ clause bound with the new subquadratic result.","marker":"Rintanen (2006)"},{"why":"Defines Bounded Variable Addition, whose grid-product re-encoding the paper analyzes formally and relates to biclique-covering encodings.","marker":"Manthey et al. (2012)"},{"why":"Supplies the lower bound that any biclique covering of $K_n$ uses at least $\\lfloor \\lg n\\rfloor$ bicliques, used in Proposition 11.","marker":"Fishburn and Hammer (1996)"},{"why":"Proves that every vertex of $K_n$ appears in at least $\\lfloor \\lg n\\rfloor$ bicliques of any biclique covering, yielding the $\\Omega(n\\lg n)$ lower bound for $K_n$.","marker":"Dong and Liu (2007)"},{"why":"Poses the non-preemptive schedulability SAT encodings that Theorem 23 improves from $O(NMT^2)$ to $O(NMT+MT^2\\lg T)$.","marker":"Mayank and Mondal (2020)"},{"why":"Poses the SLP string-compression encoding whose disjoint-intervals constraint the interval-graph encoding compresses, with the paper reporting large clause reductions.","marker":"Bannai et al. (2022)"},{"why":"Provides the counting argument that the paper adapts for its $\\Omega(n^2/\\lg n)$ lower bound on constant-width CNF encodings of independent sets.","marker":"Jukna (2013)"}],"fun_headline_variants":["Biclique trick slashes graph SAT encoding size","Graph SAT encodings go subquadratic via bicliques","Subquadratic CNF encodings for vertex cover and coloring","Biclique coverings cut quadratic SAT encodings down","Dense graph problems: smaller SAT encodings via bicliques"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The subquadratic bound stands or falls with an external theorem quoted without proof: every graph on $n$ vertices admits a biclique covering whose total vertex count $\\sum |V(B)|$ is $O(n^2/\\lg n)$, and if that theorem as quoted is false, the new encodings for independent set, vertex cover, $k$-coloring, and clique lose their guaranteed subquadratic size.","fun_headline_variants_meta":{"raw":{"variants":["Biclique trick slashes graph SAT encoding size","Graph SAT encodings go subquadratic via bicliques","Subquadratic CNF encodings for vertex cover and coloring","Biclique coverings cut quadratic SAT encodings down","Dense graph problems: smaller SAT encodings via bicliques"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000603,"raw_usage":{"total_tokens":2887,"prompt_tokens":1092,"completion_tokens":1795,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":708,"completion_tokens_details":{"reasoning_tokens":1707}},"tokens_in":708,"tokens_out":1795,"duration_ms":14253,"temperature":1.0,"reasoning_tokens":1707,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T19:57:50.726466+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Check the original statement of the 1983 biclique-covering theorem to confirm it bounds $\\sum |V(B)|$ and not just the number of bicliques; if the bound only applies to the number of bicliques, compute optimal biclique coverings for all graphs up to $n=12$ by exhaustive search and see whether $\\sum |V(B)|$ can be made $O(n^2/\\lg n)$ in every case. For the interval-graph theorem, build the formula from Theorem 22 for $n=64$, conjoin clauses forcing two overlapping intervals to both be selected, and check satisfiability: if the solver says satisfiable, the encoding is unsound.","supporting_citations":[{"cited_title":"Finding bipartite subgraphs efficiently","cited_arxiv_id":null,"evidence_quote":"Gives a polynomial-time algorithm that computes a biclique covering with the asymptotic guarantee, making Theorem 10 constructive."},{"cited_title":"Cardinality encodings for graph optimization problems","cited_arxiv_id":null,"evidence_quote":"Introduces the clique-covering encodings that the paper generalizes to biclique coverings and uses as a comparison baseline."},{"cited_title":"Compact representation of sets of binary constraints","cited_arxiv_id":null,"evidence_quote":"Earliest clique/biclique covering idea for binary constraints; the paper contrasts its $\\Theta(n^2)$ clause bound with the new subquadratic result."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines Bounded Variable Addition, whose grid-product re-encoding the paper analyzes formally and relates to biclique-covering encodings."},{"cited_title":"On the Decomposition of Graphs into Complete Bipartite Graphs","cited_arxiv_id":null,"evidence_quote":"Proves that every vertex of $K_n$ appears in at least $\\lfloor \\lg n\\rfloor$ bicliques of any biclique covering, yielding the $\\Omega(n\\lg n)$ lower bound for $K_n$."}],"review_version":1}