論文の概要: Encoding Linear Constraints into SAT

• arxiv url: http://arxiv.org/abs/2005.02073v1
• Date: Tue, 5 May 2020 11:37:43 GMT
• ステータス: 処理完了
• システム内更新日: 2022-12-06 14:27:06.976086
• Title: Encoding Linear Constraints into SAT
• Title（参考訳）: 線形制約をSATにエンコードする
• Authors: Ignasi Ab\'io, Valentin Mayer-Eichberger, Peter Stuckey
• Abstract要約: 複数値決定ダイアグラムとソートネットワークに基づく新しいSATエンコーディングを定義する。 線形整数解法 (MIP) よりも優れており, 適切な問題に対して LCG や SMT より優れている場合もある。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encodings to Boolean satisfiability (SAT) format of conjunctive normal form perform poorly in problems with these constraints in comparison with SAT modulo theories (SMT), lazy clause generation (LCG) or mixed integer programming (MIP) solvers. In this paper we explore and categorize SAT encodings for linear integer constraints. We define new SAT encodings based on multi-valued decision diagrams, and sorting networks. We compare different SAT encodings of linear constraints and demonstrate where one may be preferable to another. We also compare SAT encodings against other solving methods and show they can be better than linear integer (MIP) solvers and sometimes better than LCG or SMT solvers on appropriate problems. Combining the new encoding with lazy decomposition, which during runtime only encodes constraints that are important to the solving process that occurs, gives the best option for many highly combinatorial problems involving linear constraints.
• Abstract（参考訳）: 線形整数制約は、多くの実用的な応用で一般的に見られるため、組合せ問題において最も重要な制約の一つである。 通常、接続正規形式のブール満足度(SAT)形式への符号化は、SATモジュロ理論(SMT)や遅延節生成(LCG)、混合整数プログラミング(MIP)の解法と比較すると、これらの制約で問題となる。 本稿では,線形整数制約に対するSAT符号化の検討と分類を行う。 複数値決定図とソートネットワークに基づく新しいSAT符号化を定義する。 線形制約の異なるsat符号化を比較し、他の制約よりも望ましい場所を示す。 また、SATエンコーディングを他の解法と比較し、線形整数(MIP)ソルバよりも良い値を示し、時にはLCGやSMTソルバよりも良い値を示す。 新しいエンコーディングと遅延分解の組み合わせは、実行時に発生する解決プロセスにおいて重要な制約のみをエンコードするものであり、線形制約を含む多くの高組合せ問題に対して最適な選択肢となる。

関連論文リスト

• General Method for Solving Four Types of SAT Problems [12.28597116379225]
  既存の方法は、様々なタイプのブール適合性問題(SAT)に対して様々なアルゴリズムを提供する。 本研究では,整数計画法と強化学習法(RL)に基づく統合フレームワークDCSATを提案する。
  論文  参考訳（メタデータ） (2023-12-27T06:09:48Z)
• Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints [1.1371889042789218]
  本稿では,制約問題に対する標準的な特徴セットを用いて,効率よく符号化を選択することができることを示す。 擬似ブール制約と線形制約に特化して設計された,新しい機能セットにより,性能が向上する。 結果は、同じ機能セットを使用する場合、AutoFolioと良好に比較されます。
  論文  参考訳（メタデータ） (2023-07-18T15:26:46Z)
• Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints [39.96302127802424]
  量子コンピューティングで発生するハイブリッドブール制約の新しい応用について検討する。 この問題は、エッジカラーグラフにおける制約付き完全マッチングに関連している。 本稿では,ハイブリッド制約による制約マッチング問題の直接符号化が不十分であり,特殊な手法が依然として必要であることを示す。
  論文  参考訳（メタデータ） (2023-01-24T06:14:24Z)
• 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)
• 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)
• SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints [5.62245362437303]
  Pseudo-Boolean(PB)制約の符号化について検討する。 PB(AMO)エンコーディングは、より多くのインスタンスをタイムリミット内で解決し、時には1桁以上の時間改善を行う。
  論文  参考訳（メタデータ） (2021-10-15T12:53:01Z)
• 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)
• An Integer Linear Programming Framework for Mining Constraints from Data [81.60135973848125]
  データから制約をマイニングするための一般的なフレームワークを提案する。 特に、構造化された出力予測の推論を整数線形プログラミング(ILP)問題とみなす。 提案手法は,9×9のスドクパズルの解法を学習し,基礎となるルールを提供することなく,例からツリー問題を最小限に分散させることが可能であることを示す。
  論文  参考訳（メタデータ） (2020-06-18T20:09:53Z)
• Sparsified Linear Programming for Zero-Sum Equilibrium Finding [89.30539368124025]
  我々は、この問題に対して全く異なるアプローチを示し、それは競争力があり、しばしば、以前の最先端技術よりも桁違いに優れている。 ポーカーエンドゲームの実験により、現代の線形プログラムソルバは、ゲーム固有のCFRの現代的な変種でさえも競合することを示した。
  論文  参考訳（メタデータ） (2020-06-05T13:48:26Z)

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

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