Machine Learning for SAT: Restricted Heuristics and New Graph Representations

要約

ブール充足可能性 (SAT) は、自動計画やスケジューリングを含む多くのアプリケーションにおける基本的な NP 完全問題です。
大規模なインスタンスを解決するには、SAT ソルバーは、DPLL および CDCL ソルバーで分岐変数を選択するなど、ヒューリスティックに依存する必要があります。
このようなヒューリスティックは、機械学習 (ML) モデルを使用して改善できます。
ステップ数を減らすことはできますが、有用なモデルは比較的大きくて遅いため、通常は実行時間が妨げられます。
トレーニングされた ML モデルを使用していくつかの初期ステップを実行し、その後、制御を古典的なヒューリスティックに解放するという戦略を提案します。
これにより、SAT 解決のコールド スタートが簡素化され、ステップ数と全体的な実行時間の両方を短縮できますが、ソルバーに制御を解放するタイミングを個別に決定する必要があります。
さらに、他の領域から変換された SAT 問題 (オープン ショップ スケジューリング問題など) に合わせた Graph-Q-SAT の修正を導入します。
ランダムな産業用 SAT 問題に対するアプローチの実現可能性を検証します。

要約(オリジナル)

Boolean satisfiability (SAT) is a fundamental NP-complete problem with many applications, including automated planning and scheduling. To solve large instances, SAT solvers have to rely on heuristics, e.g., choosing a branching variable in DPLL and CDCL solvers. Such heuristics can be improved with machine learning (ML) models; they can reduce the number of steps but usually hinder the running time because useful models are relatively large and slow. We suggest the strategy of making a few initial steps with a trained ML model and then releasing control to classical heuristics; this simplifies cold start for SAT solving and can decrease both the number of steps and overall runtime, but requires a separate decision of when to release control to the solver. Moreover, we introduce a modification of Graph-Q-SAT tailored to SAT problems converted from other domains, e.g., open shop scheduling problems. We validate the feasibility of our approach with random and industrial SAT problems.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google