@techreport{oai:ipsj.ixsq.nii.ac.jp:02006438,
 author = {戸田,貴久},
 issue = {17},
 month = {Jan},
 note = {多くのNP問題には，効率的なSAT符号化とSATソルバーの組合わせによる実践的解法が活用されている一方で，SATソルバーの基礎をなすアルゴリズムの枠組みCDCLには理論的な限界があることが古くから知られている．CDCLの限界を乗り越えることを目指した研究はSAT分野において困難な挑戦のひとつとして長く認識されている．本研究は，論理式そのものだけでなく，元となるNP問題の「ヒント」をアルゴリズムに取り入れることで，CDCLにとって困難な例への代替となりうる統一的解法を提案し，特定の種類の論理式に対して最新のSATソルバーに対して桁違いに高速化できることを実験により確認する．, While many NP problems are practically solved by combining efficient SAT encoding with SAT solvers, the theoretical limitations of CDCL (Conflict-Driven Clause Learning), which forms the basis of these solvers, have been known for a long time. Research aiming to overcome the limits of CDCL has long been recognized as one of the most difficult challenges in the SAT domain. This study proposes a unified solution that can serve as an alternative for instances challenging for CDCL by incorporating ”hints” from the original NP problem―not just the logical formula itself― into the algorithm. Experiments confirm that, for specific types of logical formulas, this method achieves orders of magnitude acceleration compared to state-of-the-art SAT solvers.},
 title = {NP問題に対するヒントに基づくCDCLアルゴリズムの高速化},
 year = {2026}
}