論文の概要: Modeling and Solving Graph Synthesis Problems Using SAT-Encoded
Reachability Constraints in Picat
- arxiv url: http://arxiv.org/abs/2109.08293v1
- Date: Fri, 17 Sep 2021 01:48:32 GMT
- ステータス: 処理完了
- システム内更新日: 2021-09-21 03:08:56.055375
- Title: Modeling and Solving Graph Synthesis Problems Using SAT-Encoded
Reachability Constraints in Picat
- Title(参考訳): sat符号化到達可能性制約を用いたpicatのグラフ合成問題のモデル化と解法
- Authors: Neng-Fa Zhou (CUNY Brooklyn College & Graduate Center)
- Abstract要約: 本稿では,最近のLP/CPプログラミングコンペティションの中から選択した4つの問題に対して,Picatのプログラムを提案する。
これらのプログラムは、ピカット言語のモデリング能力と、効率的な符号化を施した最先端SATソルバの解法効率を実証する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Many constraint satisfaction problems involve synthesizing subgraphs that
satisfy certain reachability constraints. This paper presents programs in Picat
for four problems selected from the recent LP/CP programming competitions. The
programs demonstrate the modeling capabilities of the Picat language and the
solving efficiency of the cutting-edge SAT solvers empowered with effective
encodings.
- Abstract(参考訳): 多くの制約満足度問題は、ある到達可能性制約を満たす部分グラフの合成を含む。
本稿では,最近のlp/cpプログラミングコンペから選択した4つの問題に対するpicatのプログラムについて述べる。
プログラムは、picat言語のモデリング能力と効果的なエンコーディングを付与された最先端satソルバの解法効率を示す。
関連論文リスト
- Differentiable Combinatorial Scheduling at Scale [18.09256072039255]
本稿では,Gumbel-Softmax微分可能なサンプリング手法を用いて,微分可能なスケジューリングフレームワークを提案する。
スケジューリングタスクの不等式制約をエンコードするために,任意の不等式制約を積極的にエンコードするテキスト制約付きGumbel Trickを導入する。
本手法は, トレーニングデータを必要とせずに, 勾配降下による効率よく, スケーラブルなスケジューリングを容易にする。
論文 参考訳(メタデータ) (2024-06-06T02:09:39Z) - SEGO: Sequential Subgoal Optimization for Mathematical Problem-Solving [64.38649623473626]
大規模言語モデル(LLM)は人工知能の大幅な進歩を導いた。
数学的問題を解く能力を高めるために,textbfSEquential subtextbfGoal textbfOptimization (SEGO) という新しいフレームワークを提案する。
論文 参考訳(メタデータ) (2023-10-19T17:56:40Z) - 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) - Neural Improvement Heuristics for Graph Combinatorial Optimization
Problems [49.85111302670361]
本稿では,ノード,エッジ,あるいはその両方に情報をエンコードするグラフベースの問題を扱う新しいニューラル改善(NI)モデルを提案する。
提案モデルは,各地区の操作の選択を誘導する丘登頂に基づくアルゴリズムの基本的な構成要素として機能する。
論文 参考訳(メタデータ) (2022-06-01T10:35:29Z) - 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) - Transformer-based Machine Learning for Fast SAT Solvers and Logic
Synthesis [63.53283025435107]
CNFベースのSATとMaxSATは論理合成と検証システムの中心である。
そこで本研究では,Transformerアーキテクチャから派生したワンショットモデルを用いて,MaxSAT問題の解法を提案する。
論文 参考訳(メタデータ) (2021-07-15T04:47:35Z) - Neural-Symbolic Solver for Math Word Problems with Auxiliary Tasks [130.70449023574537]
我々のNS-rは、問題を読み取り、問題をエンコードする問題リーダーと、記号方程式を生成するプログラマと、答えを得るシンボリックエグゼキュータから構成される。
また, 目的表現の監督とともに, 4つの新たな補助的目的によって, 異なる記号的推論を強制的に行うように最適化した。
論文 参考訳(メタデータ) (2021-07-03T13:14:58Z) - Propositional Encodings of Acyclicity and Reachability by using Vertex
Elimination [5.482532589225551]
本稿では,非巡回性およびs-t-到達可能性制約を基礎となる有向グラフを持つ命題公式に対して符号化する新しい手法を提案する。
提案手法はこれらの制約を標準命題節として符号化し,SATソルバに直接適用する。
論文 参考訳(メタデータ) (2021-05-27T01:57:53Z) - CombOptNet: Fit the Right NP-Hard Problem by Learning Integer
Programming Constraints [20.659237363210774]
我々は、コスト項と制約の両方を学習できる層として、整数型プログラミングソルバをニューラルネットワークアーキテクチャに統合することを目指している。
結果として得られたエンドツーエンドのトレーニング可能なアーキテクチャは、生データから特徴を共同で抽出し、最先端の整数プログラミング解法で適切な(学習した)問題を解く。
論文 参考訳(メタデータ) (2021-05-05T21:52:53Z) - Efficient Incremental Modelling and Solving [1.6172800007896284]
AI計画問題を解決するための標準的なアプローチは、計画の地平線を漸進的に拡張し、特定の長さの計画を見つけようとする問題の解決である。
この研究の貢献は、SATソルバと自動モデリングシステムSaveile Rowのネイティブインタラクションを可能にすることである。
論文 参考訳(メタデータ) (2020-09-23T12:40:23Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。