論文の概要: An Experimental Study of Permanently Stored Learned Clauses

• arxiv url: http://arxiv.org/abs/2110.14187v1
• Date: Wed, 27 Oct 2021 05:36:16 GMT
• ステータス: 処理完了
• システム内更新日: 2021-10-28 14:44:14.744723
• Title: An Experimental Study of Permanently Stored Learned Clauses
• Title（参考訳）: 永久保存学習クロースに関する実験的研究
• Authors: Sima Jamali and David Mitchell
• Abstract要約: 本稿では,MapleLCMDistChronoBTの文節保存について検討する。 サイズやLBDを基準とした基準は, 大型の常設店舗を維持しながら, 性能の向上を図っている。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Modern CDCL SAT solvers learn clauses rapidly, and an important heuristic is the clause deletion scheme. Most current solvers have two (or more) stores of clauses. One has ``valuable'' clauses which are never deleted. Most learned clauses are added to the other, with an aggressive deletion strategy to restrict its size. Recent solvers in the MapleSAT family, have comparatively complex deletion scheme, and perform well. Many solvers store only binary clauses permanently, but MapleLCMDistChronoBT stores clauses with small LBD permanently. We report an experimental study of the permanent clause store in MapleLCMDistChronoBT. We observe that this store can get quite large, but several methods for limiting its size reduced performance. We also show that alternate size and LBD based criteria improve performance, while still having large permanent stores. In particular, saving clauses up to size 8, and adding small numbers of high-centrality clauses, both improved performance, with the best improvement using both methods.
• Abstract（参考訳）: 現代のCDCL SATソルバは、節を迅速に学習し、重要なヒューリスティックは節削除スキームである。 現在の解決者は2つ以上の節を格納している。 削除されない ``valuable''' 節がある。 ほとんどの学習された節が他方に追加され、そのサイズを制限する攻撃的な削除戦略が加えられる。 最近のMapleSATファミリーでは、比較的複雑な削除スキームがあり、よく機能している。 多くの解決者はバイナリ節のみを永久に保存するが、MapleLCMDistChronoBTは小さなLBDの節を永久に保存する。 今回,MapleLCMDistChronoBTにおける文節保存の実験的検討を行った。 このストアはかなり大きなものになるが、そのサイズを制限するいくつかの方法によって性能が低下している。 また,代替サイズとlbd基準により性能が向上すると同時に,大型店を併設することを示した。 特に、最大8までの節を保存し、少数の高集中度節を追加することで、パフォーマンスが向上し、両方のメソッドで最高の改善がなされた。

関連論文リスト

• Hierarchical Context Merging: Better Long Context Understanding for Pre-trained LLMs [61.40047491337793]
  本稿では,大規模言語モデルの制約を克服する新しいトレーニングフリースキームである階層型cOntext MERging(HOMER)を提案する。 HomeRは、長いインプットを管理可能なチャンクに分割する、分別/対数アルゴリズムを使用する。 トークン削減技術がマージ毎に先行し、メモリ使用効率が保証される。
  論文  参考訳（メタデータ） (2024-04-16T06:34:08Z)
• Truly No-Regret Learning in Constrained MDPs [61.78619476991494]
  未知のCMDPで学習するモデルベース原始双対アルゴリズムを提案する。 提案アルゴリズムは,誤差のキャンセルを伴わずにサブ線形後悔を実現する。
  論文  参考訳（メタデータ） (2024-02-24T09:47:46Z)
• The Ups and Downs of Large Language Model Inference with Vocabulary Trimming by Language Heuristics [74.99898531299148]
  本研究は,興味のある言語への埋め込みエントリを制限し,時間と記憶効率を高めることによる語彙トリミング(VT)について検討する。 Unicodeベースのスクリプトフィルタリングとコーパスベースの選択という2つの言語を異なる言語ファミリやサイズに適用する。 その結果、VTは小型モデルのメモリ使用量を50%近く削減し、生成速度が25%向上した。
  論文  参考訳（メタデータ） (2023-11-16T09:35:50Z)
• Augmenting Language Models with Long-Term Memory [142.04940250657637]
  既存の大規模言語モデル(LLM)では、入力長制限のため、固定サイズの入力しかできない。 本稿では,Long-Term Memory (LongMem) を付加した言語モデルを提案する。
  論文  参考訳（メタデータ） (2023-06-12T15:13:39Z)
• Explaining SAT Solving Using Causal Reasoning [30.469229388827443]
  本稿では、因果推論を用いて、現代のSATソルバの機能に関する洞察を得るCausalSATを紹介する。 われわれはCausalSATを用いて,これまで「親指のルール」や経験的発見と考えられていた仮説を定量的に検証した。
  論文  参考訳（メタデータ） (2023-06-09T22:53:16Z)
• SC-Block: Supervised Contrastive Blocking within Entity Resolution Pipelines [75.5113002732746]
  本稿では,教師付きコントラスト学習を利用した埋め込み空間におけるレコードの位置決め手法であるSC-Blockを提案する。 SC-Blockを8つの最先端のブロッキング手法と比較した。 全体の実行時間を測定するため、99.5%の完全性を持つ候補集合を決定し、それらをマーカに渡す。
  論文  参考訳（メタデータ） (2023-03-06T13:49:41Z)
• Building Concise Logical Patterns by Constraining Tsetlin Machine Clause Size [11.43224924974832]
  本稿では,CSC-TM(Clauuse Size Constrained TMs)の新たな変種について紹介する。 ある節が制約よりも多くのリテラルを含むとすぐに、リテラルを消し始める。 以上の結果より,CSC-TMはリテラルの最大80倍の精度を維持した。
  論文  参考訳（メタデータ） (2023-01-19T17:37:48Z)
• Incorporating Multi-armed Bandit with Local Search for MaxSAT [16.371916145216737]
  MaxSAT問題の2つの一般化: partial MaxSAT (PMS) と Weighted PMS (WPMS) そこで本稿では,BandHSと呼ばれる局所探索アルゴリズムを提案する。 これら2つの帯域は、実現不可能な解空間と実現不可能な解空間の両方において、アルゴリズムの探索能力を向上させることができる。
  論文  参考訳（メタデータ） (2022-11-29T08:19:26Z)
• Too much information: CDCL solvers need to forget and perform restarts [0.0]
  競合駆動型節学習(CDCL)は命題論理の満足度問題を解くための極めて成功したパラダイムである。 この論文は、節学習がランタイムを改善するだけでなく、それを劇的に劣化させることがあることを非常に驚くべきことに示します。
  論文  参考訳（メタデータ） (2022-02-01T10:16:04Z)
• Online Sparse Reinforcement Learning [60.44832065993122]
  固定地平線, スパース線形決定過程(MDP)におけるオンライン強化学習の難しさについて検討する。 この場合、よく条件付きデータを収集するポリシーが存在するとしても、線形後悔は一般的に避けられないことを示す。 このことは、大規模な行動において、学習の難しさは、優れた探索政策を見つけるのが困難であることに起因していることを示している。
  論文  参考訳（メタデータ） (2020-11-08T16:47:42Z)
• On the Effect of Learned Clauses on Stochastic Local Search [0.0]
  SATソルバでは、競合駆動型節学習(CDCL)と局所探索(SLS)が使用されている。 多数の正しいリテラルを持つ節がSLSのランタイムに有益であることを実験的に実証した。 我々は、前処理のステップとして高品質な節を追加する最も有益な戦略を導出する。
  論文  参考訳（メタデータ） (2020-05-07T13:33:16Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。