NP問題に対するヒントに基づくCDCLアルゴリズムの高速化

• Item type: SIG Technical Reports(1)
• 公開日: 2026-01-06
• タイトル / 言語: ja
• タイトル: NP問題に対するヒントに基づくCDCLアルゴリズムの高速化
• タイトル / 言語: en
• タイトル: Accelerating CDCL Algorithms for NP Problems Using Hints
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: AL17
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 電気通信大学
• 著者名: 戸田,貴久
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 多くのNP問題には，効率的なSAT符号化とSATソルバーの組合わせによる実践的解法が活用されている一方で，SATソルバーの基礎をなすアルゴリズムの枠組みCDCLには理論的な限界があることが古くから知られている．CDCLの限界を乗り越えることを目指した研究はSAT分野において困難な挑戦のひとつとして長く認識されている．本研究は，論理式そのものだけでなく，元となるNP問題の「ヒント」をアルゴリズムに取り入れることで，CDCLにとって困難な例への代替となりうる統一的解法を提案し，特定の種類の論理式に対して最新のSATソルバーに対して桁違いに高速化できることを実験により確認する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN1009593X
• 書誌情報: 研究報告アルゴリズム（AL）; 巻 2026-AL-206, 号 17, p. 1-8, 発行日 2026-01-06
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-8566
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会