論文の概要: Resource-Constrained Heuristic for Max-SAT

• arxiv url: http://arxiv.org/abs/2410.09173v1
• Date: Fri, 11 Oct 2024 18:20:08 GMT
• ステータス: 処理完了
• システム内更新日: 2024-10-30 16:03:11.121514
• Title: Resource-Constrained Heuristic for Max-SAT
• Title（参考訳）: Max-SATのための資源制約型ヒューリスティック
• Authors: Brian Matejek, Daniel Elenius, Cale Gentry, David Stoker, Adam Cobb,
• Abstract要約: より大規模な問題をより小さなサブコンポーネントに繰り返し分解する,Max-SATのインスタンスに対するリソース制約を提案する。 本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。 我々は,Max-SAT評価ベンチマークを用いて,ランダムに生成されたMax-SATインスタンスと実世界の実例について実験を行った。
• 参考スコア（独自算出の注目度）: 0.848762374187855
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We propose a resource-constrained heuristic for instances of Max-SAT that iteratively decomposes a larger problem into smaller subcomponents that can be solved by optimized solvers and hardware. The unconstrained outer loop maintains the state space of a given problem and selects a subset of the SAT variables for optimization independent of previous calls. The resource-constrained inner loop maximizes the number of satisfiable clauses in the "sub-SAT" problem. Our outer loop is agnostic to the mechanisms of the inner loop, allowing for the use of traditional solvers for the optimization step. However, we can also transform the selected "sub-SAT" problem into a quadratic unconstrained binary optimization (QUBO) one and use specialized hardware for optimization. In contrast to existing solutions that convert a SAT instance into a QUBO one before decomposition, we choose a subset of the SAT variables before QUBO optimization. We analyze a set of variable selection methods, including a novel graph-based method that exploits the structure of a given SAT instance. The number of QUBO variables needed to encode a (sub-)SAT problem varies, so we additionally learn a model that predicts the size of sub-SAT problems that will fit a fixed-size QUBO solver. We empirically demonstrate our results on a set of randomly generated Max-SAT instances as well as real world examples from the Max-SAT evaluation benchmarks and outperform existing QUBO decomposer solutions.
• Abstract（参考訳）: 資源制約のあるMax-SATのインスタンスに対するヒューリスティックを提案し、最適化されたソルバとハードウェアで解けるような、より小さなサブコンポーネントに繰り返し分解する。 制約のない外ループは与えられた問題の状態空間を維持し、前の呼び出しとは無関係に最適化するためにSAT変数のサブセットを選択する。 リソース制約された内部ループは、"sub-SAT"問題における満足できる節の数を最大化する。 我々の外ループは内部ループのメカニズムに非依存であり、最適化ステップに従来の解法を使用することができる。 しかし、選択した"sub-SAT"問題を2次非制約バイナリ最適化(QUBO)に変換して、特別なハードウェアで最適化することもできる。 分解前にSATインスタンスをQUBOに変換する既存のソリューションとは対照的に、QUBO最適化の前にSAT変数のサブセットを選択する。 本研究では,所定のSATインスタンスの構造を利用するグラフベースの新しい手法を含む,変数選択手法の集合を分析する。 部分SAT問題を符号化するために必要なQUBO変数の数が異なるため、固定サイズのQUBOソルバに適合するサブSAT問題のサイズを予測するモデルも学習する。 我々は,ランダムに生成されたMax-SATインスタンスと,Max-SAT評価ベンチマークによる実例と,既存のQUBOデコンポザソリューションよりも優れた実例について実証実験を行った。

関連論文リスト

• GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection [45.222591894755105]
  インスタンスの3部グラフ表現に基づくSATソルバ自動選択のための新しいアプローチであるGraSSを提案する。 我々は、新しいノードの特徴設計のようなドメイン固有の決定でグラフ表現を豊かにします。 生の表現とドメイン固有の選択の組み合わせが実行時の改善につながることを実証する。
  論文  参考訳（メタデータ） (2024-05-17T18:00:50Z)
• AutoSAT: Automatically Optimize SAT Solvers via Large Language Models [10.359005620433136]
  本稿では,既存のCDCLソルバをベースとしたモジュール型検索空間の自動最適化フレームワークであるAutoSATを提案する。 AutoSATは12データセット中9データセットでMiniSatを上回り、4データセットで最先端のハイブリッドソルバKissatを上回ります。
  論文  参考訳（メタデータ） (2024-02-16T14:04:56Z)
• General Method for Solving Four Types of SAT Problems [12.28597116379225]
  既存の方法は、様々なタイプのブール適合性問題(SAT)に対して様々なアルゴリズムを提供する。 本研究では,整数計画法と強化学習法(RL)に基づく統合フレームワークDCSATを提案する。
  論文  参考訳（メタデータ） (2023-12-27T06:09:48Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  分解硬度(d硬度)の概念を導入する。 d-硬度が$C$ w.r.tの硬度の推定値を示すことを示す。
  論文  参考訳（メタデータ） (2023-12-16T12:44:36Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SATは、自動スケジューリングを含む多くのアプリケーションにおいて、基本的なNP完全問題である。 大きなインスタンスを解決するためには、SATソルバは、例えばDPLLとCDCLソルバの分岐変数を選択するなど、ブールアンに依存する必要がある。 我々は、訓練されたMLモデルでいくつかの初期ステップを行い、古典的なランタイムに制御をリリースする戦略を提案する。
  論文  参考訳（メタデータ） (2023-07-18T10:46:28Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。 これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。 本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
  論文  参考訳（メタデータ） (2022-11-16T18:59:54Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  LEC インスタンスの SAT 符号化の硬さは SAT パーティショニングでは textitw.r. と推定できることを示す。 そこで本研究では, SAT符号化の難易度を精度良く推定できるパーティショニング法を提案する。
  論文  参考訳（メタデータ） (2022-10-04T09:19:13Z)
• SATformer: Transformer-Based UNSAT Core Learning [0.0]
  本稿では,SAT 問題に対する Transformer ベースのアプローチである SATformer を紹介する。 SATformerは、問題を直接解決するのではなく、満足できないことに焦点をあてて、その問題を反対方向からアプローチする。 SATformerは、シングルビットの満足度結果と最小限の不満コアを使用して、マルチタスク学習アプローチでトレーニングされる。 実験の結果,SATformerは既存のソルバのランタイムを平均21.33%削減できることがわかった。
  論文  参考訳（メタデータ） (2022-09-02T11:17:39Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNFベースのSATとMaxSATは論理合成と検証システムの中心である。 そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
  論文  参考訳（メタデータ） (2021-07-15T04:47:35Z)
• Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
  本稿では,最小長の制約付き混合被覆アレイを構築するためのSAT(Satifiability)に基づくアプローチを提案する。 この問題はシステム障害検出のためのコンビネータテストの中心である。
  論文  参考訳（メタデータ） (2021-05-26T14:00:56Z)
• Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
  我々は,数千の候補アルゴリズムの固定セットを考慮に入れた,極端なアルゴリズム選択(XAS)の設定を提案する。 我々は、XAS設定に対する最先端のAS技術の適用性を評価し、Dyadic特徴表現を利用したアプローチを提案する。
  論文  参考訳（メタデータ） (2020-01-29T09:40:58Z)

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

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