Taming the Search Space: Solving and Generating Hitori and Binairo Puzzles

Lukas Zandomeneghi; Marc Kurz; Rainhard Dieter Findling

REVIEW 2 major objections 5 minor 14 references

For Binairo, SAT solves everything; for Hitori, backtracking wins because of connectivity.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-05 00:18 UTC pith:MN4TLW6I

load-bearing objection A clear empirical ranking of SAT vs backtracking for Binairo and Hitori, but the ranking rests on self-generated benchmarks and a confusing instance-count footnote. the 2 major comments →

arxiv 2608.00768 v1 pith:MN4TLW6I submitted 2026-08-01 cs.LO

Taming the Search Space: Solving and Generating Hitori and Binairo Puzzles

Lukas Zandomeneghi , Rainhard Dieter Findling , Marc Kurz This is my paper

classification cs.LO

keywords HitoriBinairoSAT solvingbacktrackingconstraint propagationpuzzle generationCNF encodinggrid logic puzzles

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

This paper asks which solving paradigm—optimized backtracking or SAT-based solving—better matches the structure of two logic puzzles, Binairo and Hitori. It claims the answer splits cleanly. Binairo's rules encode almost directly into propositional clauses, so a SAT-based solver solves every tested puzzle up to 26×26 with low runtime, while the best backtracking configuration solves fewer than half of the instances within the timeout. Hitori's global rule that all white cells stay connected does not encode cleanly, so the SAT approach repeatedly checks connectivity outside the solver; that refinement loop consumes most of the runtime and makes SAT time out on hard instances. Across all tested sizes, propagation-based backtracking solves every evaluated Hitori instance. If the split is real, it gives puzzle engineers a practical rule: encode local constraints in SAT, and keep global connectivity in procedural search.

Core claim

The central claim is that solver performance for these puzzles is governed by how directly each puzzle's rules translate into CNF clauses. For Binairo, the best SAT configuration solved all 201 evaluated instances per grid size from 8×8 to 26×26 with a median runtime of 0.0386 s and a 95th percentile of 0.1725 s, while the best backtracking configuration (balanced value order, cell scoring, and propagation) solved only 49.0% of all instances and needed 2.6378 s at its 95th percentile on the instances it did solve. Adding propagation to plain backtracking raised Binairo's solving rate from 20.5% to 40.0% and cut median explored nodes from 5803 to 83.5. For Hitori the result reverses: propagat

What carries the argument

The load-bearing mechanism is the contrast between two encodings of the same puzzle rules. Binairo is solved as a direct CNF formula whose clauses enforce no-three-consecutive values, row and column balance, and row/column distinctness, so each SAT call advances toward a real solution. Hitori is solved with a CNF formula that encodes only the duplicate and adjacency constraints; the white-cell connectivity rule is enforced externally by a refinement loop that checks candidate solutions, adds blocking clauses, and reruns the SAT solver. The central backtracking mechanism is deterministic constraint propagation, which immediately applies forced assignments before branching; the paper shows thi

Load-bearing premise

The empirical ranking rests on assuming that the puzzles produced by the paper's own generators, which use the same solvers being compared to verify uniqueness and which abort when ambiguities resist resolution, are representative of Hitori and Binairo difficulty rather than biased by those solvers' limitations.

What would settle it

Take an independent set of Hitori puzzles of sizes 24×24 to 54×54 that were not generated with the compared solvers. If a SAT-based solver using the same blocking-clause refinement loop solves most of them within the 5 s timeout, the claim that Hitori's connectivity constraint makes this SAT approach unsuitable would fail; if a direct CNF encoding of connectivity or incremental SAT still times out on those sizes, the paper's diagnosis would be confirmed.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

If this is right

For Binairo puzzles of the sizes tested, a direct SAT encoding is the pragmatic default: it solved every evaluated instance, with a 95th-percentile runtime of 0.17 s and no timeouts.
For Hitori, propagation-based backtracking is the pragmatic default: it solved every evaluated instance up to 54×54, while the SAT approach solved none beyond 22×22 within the 5 s timeout.
Adding deterministic constraint propagation to plain backtracking is the highest-leverage optimization for both puzzle types, lifting Binairo's solving rate from 20.5% to 40.0% and Hitori's from 31.9% to 100%.
A smaller search tree does not guarantee lower runtime: the EfficientPropagation variant visits fewer Binairo nodes than full Propagation yet runs slower because of bookkeeping overhead.
Hitori SAT performance is bottlenecked by the refinement loop around the solver, not by the SAT solver itself, so a more direct connectivity encoding or incremental SAT use is the natural next improvement.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

If the structural explanation is correct, the same split should extend to other grid logic puzzles: local-rule-heavy puzzles will favor SAT, while puzzles with global connectivity or reachability constraints will favor backtracking with specialized checks, until someone finds a compact CNF encoding of connectivity.
The benchmark set was generated and verified with the same solvers under comparison; the Hitori generator aborts on unresolved ambiguities and the Binairo generator can stop early if uniqueness cannot be maintained, so the hardest instances may be missing from this distribution. An independent corpus of human-authored puzzles would test whether the paradigm ranking survives outside it.
The paper itself notes that an extended 100-instance evaluation was still running at submission, so the quantitative ratios for the largest grid sizes are provisional even though the completed smaller sizes match the reported findings.
A hybrid design—propagation-based preprocessing to fix forced cells, then SAT for the remaining local constraints, with connectivity checked procedurally as in backtracking—is a direct, testable extension implied by the paper's division of labor.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

A clear empirical ranking of SAT vs backtracking for Binairo and Hitori, but the ranking rests on self-generated benchmarks and a confusing instance-count footnote.

read the letter

Here's the short version: the paper delivers a clear empirical ranking—SAT for Binairo, propagation-based backtracking for Hitori—and backs it with a systematic ablation over optimization subsets. It also contributes a Hitori generator that resolves local ambiguities, which is a genuinely useful piece of work. But the central claim is only as strong as the benchmark set, and the benchmark set is entirely self-generated in a way that biases the comparison.

What's actually new: prior work has individual solvers and encodings; a direct head-to-head across these two puzzle types with detailed search-tree statistics is not there. The power-set evaluation is a good idea, and the propagation result is convincing: median nodes drop from 5803 to 83.5 for Binairo and from 310 to 18 for Hitori. The Hitori SAT analysis, showing 96% of runtime spent outside the SAT calls in the connectivity-refinement loop, is a sharp observation. Code is public, which is credit-worthy.

Where it gets soft. The generators are not neutral. The Binairo generator completes grids with a SAT solver and then digs while checking uniqueness with a modified backtracking solver. The Hitori generator uses backtracking for uniqueness and aborts when ambiguities can't be resolved by local flips. That can easily shape the difficulty distribution towards whichever solver was used in generation. The paper acknowledges generation is solver-dependent in general but doesn't address how that affects the comparison. The abstract claims 'solves all evaluated instances'—true for their generated set, but the paradigm-selection rule is presented as a general property. Also, Section 6.1 says 201 instances per size, while footnote 1 says the extended evaluation with 100 instances is in progress and matches findings for 20 instances per size. 201 vs 20 vs 100 is a real inconsistency; the benchmark composition needs to be unambiguous. Finally, runtime is wall-clock and the backtracking is Python while SAT is C—the node counts mitigate this, but the runtime numbers should be read as implementation-level.

Overall, this is a competent paper for puzzle and CSP researchers. I'm skeptical about how far the ranking generalizes, but the concerns are fixable with clearer scope claims and an honest limitation section. I'd send it to peer review, with the generator-bias issue as the key question. If those revisions land, it's citable for the empirical comparison.

Referee Report

2 major / 5 minor

Summary. This paper studies solving and generation of Hitori and Binairo. It compares plain and optimized backtracking (propagation, heuristics, incremental checks) against SAT-based solvers, and develops generators that produce uniquely solvable puzzles. A power-set ablation over backtracking optimizations is carried out on generated instances of sizes 8x8–26x26 (Binairo) and 8x8–54x54 (Hitori) with a 5 s timeout. The reported empirical findings are: constraint propagation is the most effective backtracking optimization; for Binairo, minisat22 SAT solving solves all generated instances with median runtime 0.0386 s, whereas the best backtracking configuration solves only 49%; for Hitori, propagation-based backtracking solves all instances with median 0.150 s, whereas the best SAT backend, minicard, solves 23.3% and spends most runtime in iterative connectivity refinement.

Significance. The contribution is a structured empirical comparison, not a new complexity or algorithmic proof. If the ranking generalizes, it gives a clear paradigm-selection rule for these puzzles and provides a useful ablated evaluation protocol. The paper is transparent about computing runtime statistics only on solved instances, makes solver and generator code public, evaluates every subset of backtracking optimizations, and checks multiple SAT backends. However, the test set consists solely of instances generated by the authors' pipelines, and those pipelines depend on the compared solvers for uniqueness and completion checks; this limits external validity and should be addressed before the broad paradigm-selection claim is accepted.

major comments (2)

[§6.1 and Footnote 1] The stated size of the solver benchmark is inconsistent. §6.1 says the solver evaluation uses 201 generated instances per puzzle type and grid size, while Footnote 1 says an extended evaluation with 100 instances per grid size is in progress and that current findings match those for 20 puzzle instances per grid size. These numbers cannot all be correct. Because Table 1 and Table 2 report medians, percentiles, and MADs over the benchmark, the sample size is load-bearing for the empirical claims. Please reconcile the numbers and make explicit which aggregation used which n.
[§5.1–5.2, §6.1] All benchmark instances are produced by the proposed generators, and the generators call the same solving technology under evaluation: the Binairo generator completes partial grids with a SAT solver and checks uniqueness with a modified backtracking solver; the Hitori generator aborts on unresolved non-local ambiguities. This does not create a circular derivation in the sense of fitting a formula to data, but it does create a selection effect: the difficulty distribution of the test corpus may be shaped by the very solvers being compared. The abstract's 'solves all evaluated instances' is therefore a statement about this particular generator output. I ask for a robustness check on an independent corpus of published Hitori/Binairo puzzles (or at least a generator built with an independent uniqueness oracle), and a corresponding qualification of the conclusions. Without this, the paradigm-

minor comments (5)

[Table 3] In Table 3, the row 'All analyzed sizes' reports a solved rate of 0.70, while Table 2 reports 0.233 overall. The text explains that Table 3 covers only sizes 8x8–22x22, but the row label should be changed to '8x8–22x22 subset' and the sample size should be given.
[§7.1] Typo: 'noticeable higher' should be 'noticeably higher'.
[§3] The citation 'Utomo [13]' should be 'Utomo and Makarim [13]' to match reference 13.
[Figure 4] The two y-axes (runtime and solved rate) share a plot but have different units and scales; the solved-rate curves are visually compressed. Consider separate panels or a labeled secondary axis with a clearer visual distinction.
[§6.3] The backend-selection procedure is summarized only as 'evaluated during backend selection.' Please state the criterion used to pick minisat22 for Binairo and minicard for Hitori, and whether the choice was stable across puzzle sizes.

Circularity Check

0 steps flagged

No circular derivation found; the empirical ranking is not forced by construction, though the self-generated benchmark raises external-validity concerns.

full rationale

The paper contains no derivation chain in which a predicted quantity reduces by construction to a fitted input. There are no fitted parameters, no equations equating inputs and outputs, and no load-bearing self-citations: the reference list is entirely external. The central claims are empirical comparisons of solver runtimes and solving rates on generated puzzles. The closest thing to a reflexive loop is that the generators use the very solver families under comparison for uniqueness checks and grid completion (Sections 5.1 and 5.2). Section 6.1 states that both benchmark sets consist solely of instances generated by the proposed generators. This creates a potential selection bias: the difficulty distribution of the test set may be shaped by the solvers being evaluated. However, this is a threat to external validity, not circularity. The paper does not define solver performance in terms of the generator, nor does it predict a quantity from the generator output in a way that is statistically forced. The reported runtimes are real measurements on concrete instances. Section 6.1 also contains a numerical inconsistency: it says the solver evaluation uses 201 generated instances per puzzle type and grid size, while the appended footnote refers to an extended evaluation with 100 instances and states that findings match results for 20 instances per grid size. This ambiguity in benchmark composition is a transparency/correctness concern, but it does not make the argument circular. The abstract's central comparisons (SAT dominates Binairo; propagation-based backtracking dominates Hitori) are supported by the measured data and by the explanation of why Hitori's iterative connectivity check hurts SAT performance. Even if the benchmark selection were imperfect, the claims are not true by definition. Accordingly, the circularity score is 0.

Axiom & Free-Parameter Ledger

2 free parameters · 4 axioms · 0 invented entities

No new physical or mathematical entities are introduced. The only novel objects are software methods, such as the Hitori generator's flip-pair ambiguity resolution, which are algorithmic techniques without independent falsifiable handles; they are not entities in the sense of new particles, mediators, or conserved quantities.

free parameters (2)

Binairo desired fill ratio
Generator stops removing values when a desired fill ratio is reached (Section 5.2); the ratio is not specified and controls benchmark difficulty, so it is an unstated modeling choice.
Binairo initial random fill fraction
Generator randomly assigns a 'small fraction' of cells before SAT completion; the fraction is unspecified and affects instance distribution (Section 5.2).

axioms (4)

domain assumption Puzzle rules as formalized (Hitori: no duplicate white numbers, no adjacent blacks, white cells connected; Binairo: equal counts, no triples, unique rows and columns) define the target problems.
The evaluation assumes these rule sets are the correct and complete definitions of Hitori and Binairo, as stated in Section 2.
domain assumption The implemented solvers and generators are correct given the described algorithms.
Empirical claims depend on the code behaving as described; the paper does not include formal verification or a test-suite evidence.
domain assumption The benchmark instances generated are valid and uniquely solvable, as guaranteed by the generators' uniqueness checks.
Section 5 states generators verify uniqueness using modified backtracking solvers, but the verification itself is assumed sound.
standard math The external SAT solvers (cadical, glucose, minisat, minicard, etc.) are sound and complete for CNF formulas.
The SAT backend is trusted as correct; the paper relies on PySAT and the selected solvers without verifying their internals.

pith-pipeline@v1.3.0-alltime-deepseek · 9780 in / 9867 out tokens · 103784 ms · 2026-08-05T00:18:09.418695+00:00 · methodology

0 comments

Cite this review

Pith. "Pith review of Taming the Search Space: Solving and Generating Hitori and Binairo Puzzles." pith.science (2026). https://pith.science/paper/MN4TLW6I

@misc{pith2026260800768,
  author       = {Pith},
  title        = {Pith review of: Taming the Search Space: Solving and Generating Hitori and Binairo Puzzles},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MN4TLW6I}},
  note         = {Machine review of arXiv:2608.00768}
}

Share X Bluesky LinkedIn Reddit HN

read the original abstract

This paper investigates solving and generation techniques for the logic puzzles Hitori and Binairo. Two solving paradigms are compared: backtracking with domain-specific optimizations, and SAT-based solving via conjunctive normal form encodings. An empirical evaluation analyzes runtime, explored search nodes, and branching factor across varying puzzle sizes. To support systematic benchmarking in the evaluation, generators capable of producing valid and uniquely solvable puzzle instances are developed. Results indicate that constraint propagation is the most effective backtracking optimization, substantially reducing the effective branching factor, search tree size, and thus runtime. Heuristic variable ordering and scoring strategies provide additional improvements. For Binairo, the SAT-based approach solves all evaluated instances within low runtime, while optimized backtracking fails to solve difficult puzzle instances within the timeout. For Hitori, propagation-based backtracking achieves the best results, while for the SAT-based approach the iterative connectivity check takes up the majority of the runtime, failing difficult puzzle instances.

Figures

Figures reproduced from arXiv: 2608.00768 by Lukas Zandomeneghi, Marc Kurz, Rainhard Dieter Findling.

**Figure 2.** Figure 2: Generation approach of the Hitori puzzle generator. [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗

**Figure 3.** Figure 3: Generation approach of the Binairo puzzle generator. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

**Figure 4.** Figure 4: Runtime comparison of selected backtracking and SAT-based solvers, for [PITH_FULL_IMAGE:figures/full_fig_p010_4.png] view at source ↗

**Figure 5.** Figure 5: SAT solver calls of the Hitori SAT solver by puzzle size for the selected [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗

discussion (0)

Reference graph

Works this paper leans on

14 extracted references · 13 canonical work pages · 1 internal anchor

[1]

CoRR abs/1304.1628(2013)

Berthier, D.: Pattern-based constraint satisfaction and logic puzzles. CoRR abs/1304.1628(2013)

Pith/arXiv arXiv 2013
[2]

ACM Computing Surveys (CSUR)38(4), 12–es (2006)

Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: A comparative survey. ACM Computing Surveys (CSUR)38(4), 12–es (2006)

work page 2006
[3]

In: Maple in Mathematics Education and Research

Bright, C., Gerhard, J., Kotsireas, I., Ganesh, V.: Effective problem solving us- ing sat solvers. In: Maple in Mathematics Education and Research. pp. 205–219. Springer International Publishing, Cham (2020)

work page 2020
[4]

Journal of Computing Sciences in Colleges28(3), 21–28 (2013)

Butler, Z.: On beyond Sudoku: pencil puzzles across cs. Journal of Computing Sciences in Colleges28(3), 21–28 (2013)

work page 2013
[5]

De Biasi, M.: Binary puzzle is np-complete (2012)

work page 2012
[6]

Hearn, R.A., Demaine, E.D.: Games, Puzzles, and Computation. A. K. Peters, Ltd., USA (2009)

work page 2009
[7]

Bachelor’s thesis, Radboud University (2021)

van der Knijff, G., Zantema, H., Geuvers, J.: Solving and generating puzzles with a connectivity constraint. Bachelor’s thesis, Radboud University (2021)

work page 2021
[8]

AI magazine 13(1), 32–32 (1992)

Kumar, V.: Algorithms for constraint-satisfaction problems: A survey. AI magazine 13(1), 32–32 (1992)

work page 1992
[9]

https://norvig.com/sudoku.html (2009), accessed: 2025-02-18

Norvig, P.: Solving every Sudoku puzzle. https://norvig.com/sudoku.html (2009), accessed: 2025-02-18

work page 2009
[10]

Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions

Pacheco, M.L., Somenzi, F., Srinivas, D., Trivedi, A.: Explaining Hitori puz- zles: Neurosymbolic proof staging for sequential decisions. arXiv preprint arXiv:2508.14294 (2025)

work page internal anchor Pith review Pith/arXiv arXiv 2025
[11]

Elsevier (2006) Taming the Search Space 15

Rossi, F., Van Beek, P., Walsh, T.: Handbook of constraint programming. Elsevier (2006) Taming the Search Space 15

work page 2006
[12]

Journal of Information Processing25, 695–707 (2017)

Suzuki, A., Kiyomi, M., Otachi, Y., Uchizawa, K., Uno, T.: Hitori numbers. Journal of Information Processing25, 695–707 (2017)

work page 2017
[13]

Mathematics in Computer Science11, 515–526 (2017)

Utomo, P.H., Makarim, R.H.: Solving a binary puzzle. Mathematics in Computer Science11, 515–526 (2017)

work page 2017
[14]

In: Foundations of artificial intelli- gence, vol

Van Beek, P.: Backtracking search algorithms. In: Foundations of artificial intelli- gence, vol. 2, pp. 85–134. Elsevier (2006)

work page 2006

[1] [1]

CoRR abs/1304.1628(2013)

Berthier, D.: Pattern-based constraint satisfaction and logic puzzles. CoRR abs/1304.1628(2013)

Pith/arXiv arXiv 2013

[2] [2]

ACM Computing Surveys (CSUR)38(4), 12–es (2006)

Bordeaux, L., Hamadi, Y., Zhang, L.: Propositional satisfiability and constraint programming: A comparative survey. ACM Computing Surveys (CSUR)38(4), 12–es (2006)

work page 2006

[3] [3]

In: Maple in Mathematics Education and Research

Bright, C., Gerhard, J., Kotsireas, I., Ganesh, V.: Effective problem solving us- ing sat solvers. In: Maple in Mathematics Education and Research. pp. 205–219. Springer International Publishing, Cham (2020)

work page 2020

[4] [4]

Journal of Computing Sciences in Colleges28(3), 21–28 (2013)

Butler, Z.: On beyond Sudoku: pencil puzzles across cs. Journal of Computing Sciences in Colleges28(3), 21–28 (2013)

work page 2013

[5] [5]

De Biasi, M.: Binary puzzle is np-complete (2012)

work page 2012

[6] [6]

Hearn, R.A., Demaine, E.D.: Games, Puzzles, and Computation. A. K. Peters, Ltd., USA (2009)

work page 2009

[7] [7]

Bachelor’s thesis, Radboud University (2021)

van der Knijff, G., Zantema, H., Geuvers, J.: Solving and generating puzzles with a connectivity constraint. Bachelor’s thesis, Radboud University (2021)

work page 2021

[8] [8]

AI magazine 13(1), 32–32 (1992)

Kumar, V.: Algorithms for constraint-satisfaction problems: A survey. AI magazine 13(1), 32–32 (1992)

work page 1992

[9] [9]

https://norvig.com/sudoku.html (2009), accessed: 2025-02-18

Norvig, P.: Solving every Sudoku puzzle. https://norvig.com/sudoku.html (2009), accessed: 2025-02-18

work page 2009

[10] [10]

Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions

Pacheco, M.L., Somenzi, F., Srinivas, D., Trivedi, A.: Explaining Hitori puz- zles: Neurosymbolic proof staging for sequential decisions. arXiv preprint arXiv:2508.14294 (2025)

work page internal anchor Pith review Pith/arXiv arXiv 2025

[11] [11]

Elsevier (2006) Taming the Search Space 15

Rossi, F., Van Beek, P., Walsh, T.: Handbook of constraint programming. Elsevier (2006) Taming the Search Space 15

work page 2006

[12] [12]

Journal of Information Processing25, 695–707 (2017)

Suzuki, A., Kiyomi, M., Otachi, Y., Uchizawa, K., Uno, T.: Hitori numbers. Journal of Information Processing25, 695–707 (2017)

work page 2017

[13] [13]

Mathematics in Computer Science11, 515–526 (2017)

Utomo, P.H., Makarim, R.H.: Solving a binary puzzle. Mathematics in Computer Science11, 515–526 (2017)

work page 2017

[14] [14]

In: Foundations of artificial intelli- gence, vol

Van Beek, P.: Backtracking search algorithms. In: Foundations of artificial intelli- gence, vol. 2, pp. 85–134. Elsevier (2006)

work page 2006

Taming the Search Space: Solving and Generating Hitori and Binairo Puzzles

Core claim §

What carries the argument

Load-bearing premise §

What would settle it §

If this is right

Where Pith is reading between the lines

discussion (0)

Core claim

Load-bearing premise

What would settle it