論文の概要: UNSAT Solver Synthesis via Monte Carlo Forest Search
- arxiv url: http://arxiv.org/abs/2211.12581v2
- Date: Fri, 26 May 2023 00:02:42 GMT
- ステータス: 処理完了
- システム内更新日: 2023-05-29 23:19:23.552629
- Title: UNSAT Solver Synthesis via Monte Carlo Forest Search
- Title(参考訳): モンテカルロ森林探索によるUNSATソルバー合成
- Authors: Chris Cameron, Jason Hartford, Taylor Lundy, Tuan Truong, Alan
Milligan, Rex Chen, Kevin Leyton-Brown
- Abstract要約: 木MDPにおける学習ポリシーのための強化学習(RL)アルゴリズムであるモンテカルロ森林探索(MCFS)を紹介する。
そのような問題の例としては、SAT公式の不満足性の証明、SAT公式の解の数を数えることがある。
我々は,満足度(SAT)問題を解決するためにDPLL分岐ポリシーを学習するMCFSアルゴリズムであるKnuth Synthesisをダブした。
- 参考スコア(独自算出の注目度): 11.729374460065745
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We introduce Monte Carlo Forest Search (MCFS), a class of reinforcement
learning (RL) algorithms for learning policies in {tree MDPs}, for which policy
execution involves traversing an exponential-sized tree. Examples of such
problems include proving unsatisfiability of a SAT formula; counting the number
of solutions of a satisfiable SAT formula; and finding the optimal solution to
a mixed-integer program. MCFS algorithms can be seen as extensions of Monte
Carlo Tree Search (MCTS) to cases where, rather than finding a good path
(solution) within a tree, the problem is to find a small tree within a forest
of candidate trees. We instantiate and evaluate our ideas in an algorithm that
we dub Knuth Synthesis, an MCFS algorithm that learns DPLL branching policies
for solving the Boolean satisfiability (SAT) problem, with the objective of
achieving good average-case performance on a given distribution of
unsatisfiable problem instances. Knuth Synthesis leverages two key ideas to
avoid the prohibitive costs of policy evaluations in an exponentially-sized
tree. First, we estimate tree size by randomly sampling paths and measuring
their lengths, drawing on an unbiased approximation due to Knuth (1975).
Second, we query a strong solver at a user-defined depth rather than learning a
policy across the whole tree, to focus our policy search on early decisions
that offer the greatest potential for reducing tree size. We matched or
improved performance over a strong baseline on three well-known SAT
distributions (R3SAT, sgen, satfc).
- Abstract(参考訳): 我々は,モンテカルロ森林探索(MCFS)を紹介した。このアルゴリズムは,指数的規模の木を横断する政策実行を伴う,木MDPにおける政策学習のための強化学習(RL)アルゴリズムである。
そのような問題の例として、SAT式の不満足性の証明、SAT式の解の数を数えること、混合整数プログラムの最適解を見つけることが挙げられる。
MCFSアルゴリズムはモンテカルロ木探索(MCTS)の拡張と見なすことができ、木の中に良い経路(解法)を見つけるのではなく、候補木のある森の中に小さな木を見つけることが問題となる。
我々は,boolean satisfiability(sat)問題を解決するdpll分岐ポリシーを学習するmcfsアルゴリズムであるknuth synthesis(knuth synthesis)をダビングするアルゴリズムでアイデアをインスタンス化し,評価する。
クヌース合成は2つの重要なアイデアを活用し、指数関数的にサイズのツリーにおける政策評価の禁止コストを回避する。
まず,木の大きさをランダムにサンプリングし,その長さを計測し,クヌート(1975)による偏りのない近似値から推定する。
第2に、木全体のポリシーを学ぶのではなく、ユーザ定義の深さで強力な解法をクエリし、木のサイズを減らす最大の可能性を提供する早期決定にポリシー検索を集中させる。
よく知られているSAT分布(R3SAT, sgen, sfc)の強いベースライン上での性能を比較または改善した。
関連論文リスト
- Autonomous Tree-search Ability of Large Language Models [58.68735916408101]
大規模言語モデルは、高度なプロンプト技術で顕著な推論能力に優れています。
近年の研究では、LLMがより困難な推論タスクを解くために受動的木探索を行えるように、検索ロジックを定義するために外部プログラムを活用することが提案されている。
我々は,LLMの自律木探索能力という新しい概念を提案し,正しい解を求める探索軌跡を含む応答を自動生成する。
論文 参考訳(メタデータ) (2023-10-14T14:14:38Z) - On Computing Optimal Tree Ensembles [8.941441654913644]
ランダム林や、より一般的には(決定ノブレイクダッシュ-)ツリーアンサンブルは、分類と回帰の方法として広く使われている。
最近のアルゴリズムの進歩は、そのサイズや深さなどの様々な測定に最適な決定木を計算することができる。
2つの新しいアルゴリズムと対応する下位境界を提供する。
論文 参考訳(メタデータ) (2023-06-07T13:30:43Z) - Structure-Unified M-Tree Coding Solver for MathWord Problem [57.825176412485504]
従来,数式表現の2次木構造を考慮に入れたモデルでは,性能が向上した。
本稿では、出力構造を統一するために、任意のM枝(M-tree)を持つ木を適用した構造統一M-Tree符号化(S-UMCr)を提案する。
広く使われているMAWPSとMath23Kデータセットの実験結果は、SUMC-rが複数の最先端モデルを上回るだけでなく、低リソース条件下でもはるかに優れた性能を発揮することを示した。
論文 参考訳(メタデータ) (2022-10-22T12:20:36Z) - Unbiased and Efficient Sampling of Dependency Trees [0.0]
ほとんどのツリーバンクは、すべての有効な依存ツリーがROOTノードから出てくる単一のエッジを持つ必要がある。
Zmigrodらは最近、単一ルート依存ツリーの分布から置き換えることなくサンプリングするアルゴリズムを提案している。
我々は、Wilson-RCを置換したサンプリングアルゴリズムが実際にバイアスを受けていることを示す。
論文 参考訳(メタデータ) (2022-05-25T09:57:28Z) - What's Wrong with Deep Learning in Tree Search for Combinatorial
Optimization [8.879790406465556]
本稿では、NP-hard Maximum Independent Set問題に対するオープンソースのベンチマークスイートについて、その重み付けと非重み付けの両変種について述べる。
また,Li らによる木探索アルゴリズム (NeurIPS 2018) の詳細な解析を行い,小型および大規模合成および実世界のグラフ上で様々な構成を検証した。
木探索で用いられるグラフ畳み込みネットワークは,解構造の有意な表現を学ばず,実際にランダムな値に置き換えることができることを示す。
論文 参考訳(メタデータ) (2022-01-25T17:37:34Z) - How Smart Guessing Strategies Can Yield Massive Scalability Improvements
for Sparse Decision Tree Optimization [18.294573939199438]
現在のアルゴリズムは、いくつかの実世界のデータセットに対して最適な木またはほぼ最適な木を見つけるために、しばしば非現実的な時間とメモリを必要とする。
本稿では,任意の分岐とバウンダリに基づく決定木アルゴリズムに適用可能なスマート推測手法を用いてこの問題に対処する。
提案手法では, 連続的特徴量, 木の大きさ, 最適決定木に対する誤差の下位境界を推定できる。
論文 参考訳(メタデータ) (2021-12-01T19:39:28Z) - Towards Optimally Efficient Tree Search with Deep Learning [76.64632985696237]
本稿では,線形モデルから信号整数を推定する古典整数最小二乗問題について検討する。
問題はNPハードであり、信号処理、バイオインフォマティクス、通信、機械学習といった様々な応用でしばしば発生する。
本稿では, 深いニューラルネットワークを用いて, 単純化されたメモリバウンドA*アルゴリズムの最適推定を推定し, HATSアルゴリズムを提案する。
論文 参考訳(メタデータ) (2021-01-07T08:00:02Z) - Solving the Steiner Tree Problem with few Terminals [8.024778381207128]
動的プログラミングによるスタイナーツリー問題の解法として、Dijkstra-Steinerアルゴリズムがある。
我々はDijkstra-Steinerアルゴリズムを強化し、DS*と呼ばれる再検討アルゴリズムを確立する。
そこで本研究では,DS* アルゴリズムの適合性は整合性よりも弱いことを示し,許容関数を用いた場合の正当性を確立する。
論文 参考訳(メタデータ) (2020-11-09T17:46:02Z) - Convex Polytope Trees [57.56078843831244]
コンベックスポリトープ木(CPT)は、決定境界の解釈可能な一般化によって決定木の系統を拡張するために提案される。
木構造が与えられたとき,木パラメータに対するCPTおよび拡張性のあるエンドツーエンドトレーニングアルゴリズムを効率的に構築する。
論文 参考訳(メタデータ) (2020-10-21T19:38:57Z) - Efficient Computation of Expectations under Spanning Tree Distributions [67.71280539312536]
本稿では,エッジファクター,非プロジェクティブ・スパンニングツリーモデルにおいて,一階期待と二階期待の重要なケースに対する統一アルゴリズムを提案する。
我々のアルゴリズムは勾配と期待の基本的な関係を利用しており、効率的なアルゴリズムを導出することができる。
論文 参考訳(メタデータ) (2020-08-29T14:58:26Z) - MurTree: Optimal Classification Trees via Dynamic Programming and Search [61.817059565926336]
動的プログラミングと探索に基づいて最適な分類木を学習するための新しいアルゴリズムを提案する。
当社のアプローチでは,最先端技術が必要とする時間のごく一部しか使用せず,数万のインスタンスでデータセットを処理することが可能です。
論文 参考訳(メタデータ) (2020-07-24T17:06:55Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。