Asymptotically Smaller Encodings for Graph Problems and Scheduling

Bernardo Subercaseaux

REVIEW 2 major objections 6 minor 37 references

Asymptotically Smaller Encodings for Graph Problems and Scheduling

T0 review · 2 major / 6 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2506.14042 v1 pith:CMQRTQXG submitted 2025-06-16 cs.LO cs.AIcs.DS

Bernardo Subercaseaux This is my paper · ORCID

classification cs.LOcs.AIcs.DS MSC 03B0505C6905C7068Q1768Q25

keywords CNFencodingsbicliquecoveringindependent-setpropertyintervalgraphsSATboundedvariableadditionschedulingat-most-oneconstraints

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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 ℓ

What 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.

Proportionate 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.

Referee Report

2 major / 6 minor

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.

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 (2)

[Section 4.2, Theorem 22, x-edges paragraph] 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 2.2, k-coloring bullet] 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.

minor comments (6)

[Section 3.2, Proposition 17] 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 4.3, Theorem 23 proof] 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.
[Abstract and Section 4.3] There is a typo in the abstract: "Mayank and Modal" should be "Mayank and Mondal" to match the reference and the main text.
[Appendix B, Code 1] 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 2.1, Proposition 6 proof] 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 2.2, Theorem 9] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the main claims are derived from stated external theorems and self-contained constructions; self-citations are contextual rather than load-bearing.

full rationale

The derivation chain is not circular. The subquadratic encoding (Theorem 10) is obtained by combining the self-contained Proposition 8 (BC-ISP encodings have size equal to the sum of biclique vertex counts) with Theorem 9, an explicitly cited external theorem of Chung, Erdős, and Spencer; the paper proves Proposition 8 and does not define biclique coverings in terms of the encoding size. Theorem 22 is proved by strong induction with direct-encoding base cases and self-contained lemmas (Lemma 21, Proposition 20), and its recursive calls are on strictly smaller instances (I_b or I_{2b}). Proposition 16 gives a formal proof of an empirical BVA observation, which is the opposite of importing a fitted claim. The self-citations (Subercaseaux and Heule 2022/2023; Bannai et al. 2025 under review) are contextual or supported by the experiments in Table 2, and none is used to justify the main theorems. Any concern that Theorem 9 as quoted might not match the original statement, or that the x-edge accounting in Theorem 22 is unsound, is a correctness or verification issue rather than a circularity, because the paper's equations would not reduce to its outputs by construction even if those objections were correct.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper introduces no new physical entities or fitted parameters. The central results rest on cited external theorems (biclique covering bounds and efficient covering algorithms) plus unproven compositionality in the interval encoding.

assumptions (5)

standard math Chung-Erdős-Spencer biclique covering theorem (Theorem 9)
Every graph has a biclique covering with total vertex count O(n^2/lg n); cited without proof and load-bearing for Theorem 10.
standard math Chen's product encoding of AMO uses O(n) clauses
Used as the atomic encoding for cliques in CC-ISP and for the BVA linear encoding; cited from literature.
standard math Dong and Liu (2007) lower bound on biclique coverings of K_n
Used in Proposition 11 to show any BC-ISP encoding for K_n uses Omega(n lg n) clauses.
standard math Mubayi and Turan (2010) polynomial-time deterministic biclique covering algorithm
Invoked to make Theorem 10 constructive; algorithm cited, not implemented.
ad hoc to paper Compositional correctness of the block decomposition in Theorem 22
The proof bounds clause counts but does not fully prove that conjoining encodings of the five edge types with auxiliary variables exactly captures the independent-set property of I_n.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Asymptotically Smaller Encodings for Graph Problems and Scheduling." pith.science (2026). https://pith.science/paper/CMQRTQXG

@misc{pith2026250614042,
  author       = {Pith},
  title        = {Pith review of: Asymptotically Smaller Encodings for Graph Problems and Scheduling},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CMQRTQXG}},
  note         = {Machine review of arXiv:2506.14042}
}

abstract

We show how several graph problems (e.g., vertex-cover, independent-set, $k$-coloring) can be encoded into CNF using only $O(|V|^2 / \lg |V|)$ many clauses, as opposed to the $\Omega(|V|^2)$ constraints used by standard encodings. This somewhat surprising result is a simple consequence of a result of Erd\H{o}s, Chung, and Spencer (1983) about biclique coverings of graphs, and opens theoretical avenues to understand the success of "Bounded Variable Addition'' (Manthey, Heule, and Biere, 2012) as a preprocessing tool. Finally, we show a novel encoding for independent sets in some dense interval graphs using only $O(|V| \lg |V|)$ clauses (the direct encoding uses $\Omega(|V|^2)$), which we have successfully applied to a string-compression encoding posed by Bannai et al. (2022). As a direct byproduct, we obtain a reduction in the encoding size of a scheduling problem posed by Mayank and Modal (2020) from $O(NMT^2)$ to $O(NMT + M T^2 \lg T)$, where $N$ is the number of tasks, $T$ the total timespan, and $M$ the number of machines.

Figures

Figures reproduced from arXiv: 2506.14042 by the authors.

**Figure 2.** Illustration of the interval graph I5 in two different representations, where the only two independent sets of size larger than 1 are depicted, one in red and one in cyan. Proof. First, we note that for every 𝑘 P {2, . . . , 𝑛 ´ 1}, all the intervals [𝑖, 𝑗] P 𝑉(I𝑛) with 𝑖 ď 𝑘 ď 𝑗 intersect, thus forming a clique that we denote 𝐾X𝑘. Then, observe that the collection of cliques 𝐾X𝑘, for 2 ď 𝑘 ď 𝑛 ´ 1, is a clique cove… view at source ↗

**Figure 3.** Illustration of Lemma 21. The type of each edge is indicated by its label, and blocks are separated by dashed blue lines. 5. 𝐵(𝑖1) ă 𝐵(𝑖2) = 𝐵( 𝑗1) ≠ 𝐵( 𝑗2), and 𝑖2 ď 𝑗1, in which case we say 𝑒 is an 𝑚-edge. Moreover, any tuple (𝑖1, 𝑗1, 𝑖2, 𝑗2) with 𝑖1 ď 𝑖2 that satisfies one of these cases implies { [𝑖1, 𝑗1], [𝑖2, 𝑗2]} P 𝐸(I𝑛). An illustration of Lemma 21 is provided in [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

Figures from the paper (1 more)

**Figure 4.** Figure 4: A decision tree for the cases of Lemma 21. 9 10 # the five predicates from the lemma 11 is x = (bi1 == bi2) and (bj1 == bj2) 12 is y = (bi1 < bi2) and (bi2 < bj1) 13 is s = (bi1 == bi2) and (bj1 != bj2) 14 is f = (bi1 < bi2) and (bj1 == bj2) and (bi2 == bj1) 15 is m = …

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

37 extracted references · 26 canonical work pages

[1]

Covering graphs by the minimum number of equivalence relations

Noga Alon. Covering graphs by the minimum number of equivalence relations. Combinatorica, 6 0 (3): 0 201--206, September 1986. ISSN 1439-6912. doi:10.1007/BF02579381

work page doi:10.1007/bf02579381 1986
[2]

Cardinality Networks : A theoretical and empirical study

Roberto As \'i n, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodr \'i guez-Carbonell . Cardinality Networks : A theoretical and empirical study. Constraints, 16 0 (2): 0 195--221, April 2011. ISSN 1572-9354. doi:10.1007/s10601-010-9105-0

work page doi:10.1007/s10601-010-9105-0 2011
[3]

Computing NP-Hard Repetitiveness Measures via MAX-SAT

Hideo Bannai, Keisuke Goto, Masakazu Ishihata, Shunsuke Kanda, Dominik K\" o ppl, and Takaaki Nishimoto. Computing NP-Hard Repetitiveness Measures via MAX-SAT . In Shiri Chechik, Gonzalo Navarro, Eva Rotenberg, and Grzegorz Herman, editors, 30th Annual European Symposium on Algorithms (ESA 2022), volume 244 of Leibniz International Proceedings in Informat...

2022
[4]

Computing NP-Hard Repetitiveness Measures via MAX-SAT (under review), 2025

Hideo Bannai, Keisuke Goto, Masakazu Ishihata, Shunsuke Kanda, Dominik K\" o ppl, Takaaki Nishimoto, and Bernardo Subercaseaux. Computing NP-Hard Repetitiveness Measures via MAX-SAT (under review), 2025

work page 2025
[5]

exactly one clauses · I ssue \#39 · arminbiere/kissat --- github.com

Armin Biere. exactly one clauses · I ssue \#39 · arminbiere/kissat --- github.com. https://github.com/arminbiere/kissat/issues/39\#issuecomment-1686043817, 2023. [Accessed 06-06-2025]

work page 2023
[6]

Successful SAT encoding techniques

Magnus Bj \" o rk. Successful SAT encoding techniques. J. Satisf. Boolean Model. Comput., 7 0 (4): 0 189--201, 2011. doi:10.3233/SAT190085. URL https://doi.org/10.3233/sat190085

work page doi:10.3233/sat190085 2011
[7]

A new sat encoding of the at-most-one constraint

Jingchao Chen. A new sat encoding of the at-most-one constraint. Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation., page 8, 2010

work page 2010
[8]

o zy, editors, Studies in Pure Mathematics : To the Memory of Paul Tur \'a n , pages 95--101. Birkh \

F. R. K. Chung, P. Erd o s, and J. Spencer. On the decomposition of graphs into complete bipartite subgraphs. In Paul Erd o s, L \'a szl \'o Alp \'a r, G \'a bor Hal \'a sz, and Andr \'a s S \'a rk \"o zy, editors, Studies in Pure Mathematics : To the Memory of Paul Tur \'a n , pages 95--101. Birkh \"a user, Basel, 1983. ISBN 978-3-0348-5438-2. doi:10.100...

doi:10.1007/978-3-0348-5438-2_10 1983

Show all 37 references

[9]

Clique covering of large real-world networks

Alessio Conte, Roberto Grossi, and Andrea Marino. Clique covering of large real-world networks. In Proceedings of the 31st Annual ACM Symposium on Applied Computing, SAC '16, page 1134–1139, New York, NY, USA, 2016. Association for Computing Machinery. ISBN 9781450337397. doi:...

2016
[10]

On the Decomposition of Graphs into Complete Bipartite Graphs

Jinquan Dong and Yanpei Liu. On the Decomposition of Graphs into Complete Bipartite Graphs . Graphs and Combinatorics, 23 0 (3): 0 255--262, June 2007. ISSN 1435-5914. doi:10.1007/s00373-007-0722-3

2007 doi
[11]

Kulikov, Ivan Mihajlin, and Nikita Slezkin

Gregory Emdin, Alexander S. Kulikov, Ivan Mihajlin, and Nikita Slezkin. CNF Encodings of Parity . In Stefan Szeider, Robert Ganian, and Alexandra Silva, editors, 47th International Symposium on Mathematical Foundations of Computer Science ( MFCS 2022) , volume 241 of Leibniz I...

2022 doi
[12]

Fishburn and Peter L

Peter C. Fishburn and Peter L. Hammer. Bipartite dimensions and bipartite degrees of graphs. Discrete Mathematics, 160 0 (1): 0 127--148, November 1996. ISSN 0012-365X. doi:10.1016/0012-365X(95)00154-O

1996 doi
[13]

Covering the edges of a random graph by cliques

Alan Frieze and Bruce Reed. Covering the edges of a random graph by cliques. Combinatorica, 15 0 (4): 0 489--497, December 1995. ISSN 1439-6912. doi:10.1007/BF01192522

1995 doi
[14]

Covering the edges of a random graph by cliques, 2011

Alan Frieze and Bruce Reed. Covering the edges of a random graph by cliques, 2011. URL https://arxiv.org/abs/1103.4870

2011 arXiv
[15]

Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule. Effective Auxiliary Variables via Structured Reencoding . In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing ( SAT 2023) , volume 271 o...

2023 doi
[16]

Marijn J. H. Heule and Manfred Scheucher. Happy Ending : An Empty Hexagon in Every Set of 30 Points . In Bernd Finkbeiner and Laura Kov \'a cs, editors, Tools and Algorithms for the Construction and Analysis of Systems , pages 61--80, Cham, 2024. Springer Nature Switzerland. I...

2024 doi
[17]

Marijn J. H. Heule and Stefan Szeider. A SAT Approach to Clique-Width . ACM Trans. Comput. Logic, 16 0 (3): 0 24:1--24:27, June 2015. ISSN 1529-3785. doi:10.1145/2736696

2015 doi
[18]

Is the smallest grammar problem over the singleton alphabet known to be np-complete or ...? Computer Science Stack Exchange, 2025

Daniel Donnelly (https://cs.stackexchange.com/users/12373/daniel donnelly). Is the smallest grammar problem over the singleton alphabet known to be np-complete or ...? Computer Science Stack Exchange, 2025. URL https://cs.stackexchange.com/q/171713. URL:https://cs.stackexchang...

2025
[19]

Cardinality encodings for graph optimization problems

Alexey Ignatiev, Antonio Morgado, and Joao Marques-Silva . Cardinality encodings for graph optimization problems. In Proceedings of the 26th International Joint Conference on Artificial Intelligence , IJCAI '17, pages 652--658, Melbourne, Australia, August 2017. AAAI Press. IS...

2017
[20]

Computational Complexity of Graphs

Stasys Jukna. Computational Complexity of Graphs . In Advances in Network Complexity , chapter 5, pages 99--153. John Wiley & Sons, Ltd, 2013. ISBN 978-3-527-67046-8. doi:10.1002/9783527670468.ch05

2013 doi
[21]

A lower bound on CNF encodings of the at-most-one constraint

Petr Ku c era, Petr Savick \'y , and Vojt e ch Vorel. A lower bound on CNF encodings of the at-most-one constraint. Theoretical Computer Science, 762: 0 51--73, 2019. ISSN 0304-3975. doi:10.1016/j.tcs.2018.09.003

2019 doi
[22]

Norbert Manthey, Marijn J. H. Heule, and Armin Biere. Automated reencoding of boolean formulas. In Haifa Verification Conference , pages 102--117. Springer, 2012

2012
[23]

Timetabling based on sat encoding: a case study

Filip Mari\'c. Timetabling based on sat encoding: a case study. https://poincare.matf.bg.ac.rs/ filip/phd/sat-timetable.pdf, 2008

2008
[24]

Efficient SAT encoding scheme for schedulability analysis of non-preemptive tasks on multiple computational resources

Jaishree Mayank and Arijit Mondal. Efficient SAT encoding scheme for schedulability analysis of non-preemptive tasks on multiple computational resources. Journal of Systems Architecture, 110: 0 101818, November 2020. ISSN 1383-7621. doi:10.1016/j.sysarc.2020.101818

2020
[25]

Finding bipartite subgraphs efficiently

Dhruv Mubayi and Gy \"o rgy Tur \'a n. Finding bipartite subgraphs efficiently. Information Processing Letters, 110 0 (5): 0 174--177, February 2010. ISSN 0020-0190. doi:10.1016/j.ipl.2009.11.015

2010 doi
[26]

Empirical study on sat-encodings of the at-most-one constraint

Van-Hau Nguyen, Van-Quyet Nguyen, Kyungbaek Kim, and Pedro Barahona. Empirical study on sat-encodings of the at-most-one constraint. In The 9th International Conference on Smart Media and Applications, SMA 2020, page 470–475, New York, NY, USA, 2021. Association for Computing ...

2020
[27]

C liquer homepage --- users.aalto.fi

Sampo Niskanen and Patric Östergård. C liquer homepage --- users.aalto.fi. https://users.aalto.fi/ pat/cliquer.html, 2002. [Accessed 09-06-2025]

2002
[28]

CNF Encodings, chapter 2

Steven Prestwich. CNF Encodings, chapter 2. IOS Press, February 2021. doi:10.3233/faia200985. URL http://dx.doi.org/10.3233/FAIA200985

2021 doi
[29]

Long Qian, Eric Wang, Bernardo Subercaseaux, and Marijn J. H. Heule. Unfolding boxes with local constraints, 2025. URL https://arxiv.org/abs/2506.01079

2025 arXiv
[30]

Compact representation of sets of binary constraints

Jussi Rintanen. Compact representation of sets of binary constraints. Frontiers in Artificial Intelligence and Applications, pages 143--147, Netherlands, 2006. IOS Press BV. ISBN 9781586036423

2006
[31]

SAT-based Decision Tree Learning for Large Data Sets

Andre Schidler and Stefan Szeider. SAT-based Decision Tree Learning for Large Data Sets . Journal of Artificial Intelligence Research, 80: 0 875--918, July 2024. ISSN 1076-9757. doi:10.1613/jair.1.15956

2024 doi
[32]

Towards an Optimal CNF Encoding of Boolean Cardinality Constraints

Carsten Sinz. Towards an Optimal CNF Encoding of Boolean Cardinality Constraints . In Peter van Beek , editor, Principles and Practice of Constraint Programming - CP 2005 , pages 827--831, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. ISBN 978-3-540-32050-0

2005
[33]

Bernardo Subercaseaux and Marijn J. H. Heule. The Packing Chromatic Number of the Infinite Square Grid is 15. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference , TACAS 20...

2023
[34]

The Packing Chromatic Number of the Infinite Square Grid Is at Least 14

Bernardo Subercaseaux and Marijn JH Heule. The Packing Chromatic Number of the Infinite Square Grid Is at Least 14. In 25th International Conference on Theory and Applications of Satisfiability Testing ( SAT 2022) . Schloss Dagstuhl-Leibniz-Zentrum f \"u r Informatik, 2022

2022
[35]

William J. Wesley. Lower Bounds for Book Ramsey Numbers , October 2024

2024
[36]

A review on algorithms for maximum clique problems

Qinghua Wu and Jin-Kao Hao. A review on algorithms for maximum clique problems. European Journal of Operational Research, 242 0 (3): 0 693--709, May 2015. ISSN 0377-2217. doi:10.1016/j.ejor.2014.09.064

2015 doi
[37]

Yet another comparison of sat encodings for the at-most-k constraint, 2020

Neng-Fa Zhou. Yet another comparison of sat encodings for the at-most-k constraint, 2020. URL https://arxiv.org/abs/2005.06274

2020 arXiv

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.

[1] [1]

Covering graphs by the minimum number of equivalence relations

Noga Alon. Covering graphs by the minimum number of equivalence relations. Combinatorica, 6 0 (3): 0 201--206, September 1986. ISSN 1439-6912. doi:10.1007/BF02579381

work page doi:10.1007/bf02579381 1986

[2] [2]

Cardinality Networks : A theoretical and empirical study

Roberto As \'i n, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodr \'i guez-Carbonell . Cardinality Networks : A theoretical and empirical study. Constraints, 16 0 (2): 0 195--221, April 2011. ISSN 1572-9354. doi:10.1007/s10601-010-9105-0

work page doi:10.1007/s10601-010-9105-0 2011

[3] [3]

Computing NP-Hard Repetitiveness Measures via MAX-SAT

Hideo Bannai, Keisuke Goto, Masakazu Ishihata, Shunsuke Kanda, Dominik K\" o ppl, and Takaaki Nishimoto. Computing NP-Hard Repetitiveness Measures via MAX-SAT . In Shiri Chechik, Gonzalo Navarro, Eva Rotenberg, and Grzegorz Herman, editors, 30th Annual European Symposium on Algorithms (ESA 2022), volume 244 of Leibniz International Proceedings in Informat...

2022

[4] [4]

Computing NP-Hard Repetitiveness Measures via MAX-SAT (under review), 2025

Hideo Bannai, Keisuke Goto, Masakazu Ishihata, Shunsuke Kanda, Dominik K\" o ppl, Takaaki Nishimoto, and Bernardo Subercaseaux. Computing NP-Hard Repetitiveness Measures via MAX-SAT (under review), 2025

work page 2025

[5] [5]

exactly one clauses · I ssue \#39 · arminbiere/kissat --- github.com

Armin Biere. exactly one clauses · I ssue \#39 · arminbiere/kissat --- github.com. https://github.com/arminbiere/kissat/issues/39\#issuecomment-1686043817, 2023. [Accessed 06-06-2025]

work page 2023

[6] [6]

Successful SAT encoding techniques

Magnus Bj \" o rk. Successful SAT encoding techniques. J. Satisf. Boolean Model. Comput., 7 0 (4): 0 189--201, 2011. doi:10.3233/SAT190085. URL https://doi.org/10.3233/sat190085

work page doi:10.3233/sat190085 2011

[7] [7]

A new sat encoding of the at-most-one constraint

Jingchao Chen. A new sat encoding of the at-most-one constraint. Proc. of the Tenth Int. Workshop of Constraint Modelling and Reformulation., page 8, 2010

work page 2010

[8] [8]

o zy, editors, Studies in Pure Mathematics : To the Memory of Paul Tur \'a n , pages 95--101. Birkh \

F. R. K. Chung, P. Erd o s, and J. Spencer. On the decomposition of graphs into complete bipartite subgraphs. In Paul Erd o s, L \'a szl \'o Alp \'a r, G \'a bor Hal \'a sz, and Andr \'a s S \'a rk \"o zy, editors, Studies in Pure Mathematics : To the Memory of Paul Tur \'a n , pages 95--101. Birkh \"a user, Basel, 1983. ISBN 978-3-0348-5438-2. doi:10.100...

doi:10.1007/978-3-0348-5438-2_10 1983