論文の概要: Towards an Understanding of Long-Tailed Runtimes of SLS Algorithms
- arxiv url: http://arxiv.org/abs/2210.13159v1
- Date: Mon, 24 Oct 2022 12:22:25 GMT
- ステータス: 処理完了
- システム内更新日: 2022-10-25 21:18:53.903352
- Title: Towards an Understanding of Long-Tailed Runtimes of SLS Algorithms
- Title(参考訳): SLSアルゴリズムの長期実行の理解に向けて
- Authors: Jan-Hendrik Lorenz and Florian W\"orz
- Abstract要約: GapSATソルバは、SLSソルバの性能を平均的に向上させる方法として、追加情報を学習した。
本稿では論理的に等価な問題定式化を生成する方法を提案する。
シュオニングのランダムウォークアルゴリズムのランタイムは約 Johnson SB であることを示す。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The satisfiability problem is one of the most famous problems in computer
science. Its NP-completeness has been used to argue that SAT is intractable.
However, there have been tremendous advances that allow SAT solvers to solve
instances with millions of variables. A particularly successful paradigm is
stochastic local search.
In most cases, there are different ways of formulating the underlying
problem. While it is known that this has an impact on the runtime of solvers,
finding a helpful formulation is generally non-trivial. The recently introduced
GapSAT solver [Lorenz and W\"orz 2020] demonstrated a successful way to improve
the performance of an SLS solver on average by learning additional information
which logically entails from the original problem. Still, there were cases in
which the performance slightly deteriorated. This justifies in-depth
investigations into how learning logical implications affects runtimes for SLS.
In this work, we propose a method for generating logically equivalent problem
formulations, generalizing the ideas of GapSAT. This allows a rigorous
mathematical study of the effect on the runtime of SLS solvers. If the
modification process is treated as random, Johnson SB distributions provide a
perfect characterization of the hardness. Since the observed Johnson SB
distributions approach lognormal distributions, our analysis also suggests that
the hardness is long-tailed. As a second contribution, we theoretically prove
that restarts are useful for long-tailed distributions. This implies that
additional restarts can further refine all algorithms employing above mentioned
modification technique. Since the empirical studies compellingly suggest that
the runtime distributions follow Johnson SB distributions, we investigate this
property theoretically. We succeed in proving that the runtimes for
Sch\"oning's random walk algorithm are approximately Johnson SB.
- Abstract(参考訳): 満足度問題はコンピュータ科学における最も有名な問題の1つである。
そのNP完全性は、SATは難解であると主張するのに使われている。
しかし、SATソルバが数百万の変数でインスタンスを解くことができるような大きな進歩があった。
特に成功したパラダイムは確率的局所探索である。
ほとんどの場合、基礎となる問題を定式化する方法は様々である。
これはソルバのランタイムに影響を与えることが知られているが、有用な定式化を見つけることは概して簡単ではない。
最近導入されたGapSATソルバ [Lorenz and W\"orz 2020] は、元の問題から論理的に関連する追加情報を学習することで、SLSソルバの性能を平均的に向上する方法を実証した。
しかし、パフォーマンスがわずかに悪化するケースもあった。
これは、論理的含意の学習がSLSのランタイムに与える影響について、詳細な調査を正当化する。
本稿では,論理的に等価な問題定式化を生成する手法を提案し,GapSATの考え方を一般化する。
これにより、slsソルバのランタイムに与える影響の厳密な数学的研究が可能になる。
修正過程がランダムに扱われる場合、ジョンソンsb分布は硬さの完全な特徴付けを提供する。
観測されたJohnson SB分布は対数正規分布に近づいたため、我々の分析は硬度が長いことも示唆している。
第2の貢献として、再起動が長期分布に有用であることを理論的に証明する。
このことは、追加の再起動が上記の修正技法を用いた全てのアルゴリズムをさらに洗練することを意味する。
実験的な研究は、ランタイム分布がJohnson SB分布に従うことを強く示唆するので、理論的にこの性質を調査する。
我々はSch\"oningのランダムウォークアルゴリズムのランタイムがおよそJohnson SBであることを証明することに成功している。
関連論文リスト
- Light Schrödinger Bridge [72.88707358656869]
我々は,軽量でシミュレーション不要で理論的に正当化されたSchr"odinger Bridgesソルバを開発した。
我々の光解法は密度推定に広く用いられているガウス混合モデルに類似している。
この類似性に着想を得て、光解法がSBの普遍近似であることを示す重要な理論的結果も証明した。
論文 参考訳(メタデータ) (2023-10-02T13:06:45Z) - Using deep learning to construct stochastic local search SAT solvers
with performance bounds [0.0]
グラフニューラルネットワークを用いてオーラクルを訓練し、2つのSLSソルバ上で、様々な難易度を持つランダムSATインスタンス上でそれらを評価する。
GNNベースのオラクルへのアクセスは,両者のパフォーマンスを著しく向上させることがわかった。
論文 参考訳(メタデータ) (2023-09-20T16:27:52Z) - Machine Learning for SAT: Restricted Heuristics and New Graph
Representations [0.8870188183999854]
SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。
大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。
我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
論文 参考訳(メタデータ) (2023-07-18T10:46:28Z) - Approximating a RUM from Distributions on k-Slates [88.32814292632675]
与えられた分布を平均で最もよく近似するRUMを求める一般化時間アルゴリズムを求める。
我々の理論的結果は、実世界のデータセットに効果的でスケール可能なものを得るという、実践的な結果も得られます。
論文 参考訳(メタデータ) (2023-05-22T17:43:34Z) - Formalizing Preferences Over Runtime Distributions [25.899669128438322]
アルゴリズムよりも好みを記述したスコアリング関数を特徴付けるために,ユーティリティ理論のアプローチを用いる。
本稿では,不特定容量分布のモデル化における最大エントロピー手法の活用法を示す。
論文 参考訳(メタデータ) (2022-05-25T19:43:48Z) - Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
本論文は, Boolean satisfiability problem (SAT) を機械学習技術で解くことに関する最近の文献をレビューする。
ML-SATソルバを手作り特徴を持つナイーブ分類器からNeuroSATのような新たなエンド・ツー・エンドSATソルバまで,進化するML-SATソルバについて検討する。
論文 参考訳(メタデータ) (2022-03-02T05:14:12Z) - Choosing the Right Algorithm With Hints From Complexity Theory [16.33500498939925]
我々は,メトロポリスのアルゴリズムが,合理的な問題サイズを考慮に入れた全てのアルゴリズムの中で,明らかに最良のものであることを示す。
このタイプの人工アルゴリズムは、$O(n log n)$ランタイムを持つので、重要度に基づくコンパクト遺伝的アルゴリズム(sig-cGA)は、高い確率で、DLB問題を解くことができる。
論文 参考訳(メタデータ) (2021-09-14T11:12:32Z) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - Evidence for Long-Tails in SLS Algorithms [0.0]
局所探索(SLS)は命題論理の満足度問題を解くためのパラダイムとして成功している。
この領域における最近の開発には、オリジナルのインスタンスではなく、修正されたが論理的に等価なインスタンスを解くことが含まれる。
本稿では,この手法がSLSソルバのランタイムに与える影響について検討する。
論文 参考訳(メタデータ) (2021-07-01T11:31:39Z) - From Checking to Inference: Actual Causality Computations as
Optimization Problems [79.87179017975235]
本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。
8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
論文 参考訳(メタデータ) (2020-06-05T10:56:52Z) - Hardness of Random Optimization Problems for Boolean Circuits,
Low-Degree Polynomials, and Langevin Dynamics [78.46689176407936]
アルゴリズムの族は高い確率でほぼ最適な解を生成できないことを示す。
ブール回路の場合、回路複雑性理論で知られている最先端境界を改善する。
論文 参考訳(メタデータ) (2020-04-25T05:45:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。