AI 中文总结
本文研究Hitori和Binairo谜题的求解与生成，对比回溯法与SAT-based方法，开发了有效唯一可解谜题生成器，发现约束传播优化回溯法效果最优，不同方法在两类谜题上表现有差异。
AI 中文摘要
本文研究逻辑谜题Hitori和Binairo的解决与生成技术，对比两种求解范式：带领域特定优化的回溯法，以及通过合取范式编码的SAT-based求解法。为支撑评估中的系统基准测试，本文开发了能生成有效且唯一可解谜题实例的生成器。实证评估分析了不同谜题规模下的运行时间、探索的搜索节点数与分支因子。结果显示，约束传播是最有效的回溯优化方法，可大幅降低有效分支因子、搜索树规模，进而缩短运行时间；启发式变量排序与评分策略可提供额外改进。对于Binairo谜题，SAT-based方法在短时间内解决了所有评估实例，而优化后的回溯法无法在超时内解决困难实例；对于Hitori谜题，基于传播的回溯法取得最佳结果，而SAT-based方法中迭代连通性检查占用了大部分运行时间，无法解决困难实例。
英文摘要
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.
