論文の概要: A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
- arxiv url: http://arxiv.org/abs/2101.01953v1
- Date: Wed, 6 Jan 2021 10:25:22 GMT
- ステータス: 処理完了
- システム内更新日: 2021-04-11 00:09:12.265026
- Title: A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
- Title(参考訳): 擬似ブール制約のDNNF符号化における下界
- Authors: Alexis de Colnet
- Abstract要約: 疑似ブール制約をSATにエンコーディングする際の2つの大きな考慮事項は、エンコーディングのサイズとその伝播強度である。
命令されたBDD(OBDD)表現と推論されたCNFエンコーディングがすべて指数的サイズを持つPB制約が存在することが示されている。
- 参考スコア(独自算出の注目度): 3.42658286826597
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Two major considerations when encoding pseudo-Boolean (PB) constraints into
SAT are the size of the encoding and its propagation strength, that is, the
guarantee that it has a good behaviour under unit propagation. Several
encodings with propagation strength guarantees rely upon prior compilation of
the constraints into DNNF (decomposable negation normal form), BDD (binary
decision diagram), or some other sub-variants. However it has been shown that
there exist PB-constraints whose ordered BDD (OBDD) representations, and thus
the inferred CNF encodings, all have exponential size. Since DNNFs are more
succinct than OBDDs, preferring encodings via DNNF to avoid size explosion
seems a legitimate choice. Yet in this paper, we prove the existence of
PB-constraints whose DNNFs all require exponential size.
- Abstract(参考訳): 疑似boolean(pb)制約をsatにエンコードする場合の2つの重要な考慮事項は、エンコーディングの大きさと伝播強度、すなわち単位伝搬下での振る舞いが良好であることの保証である。
伝播強度が保証されるいくつかのエンコーディングは、制約をDNNF(decomposable negation normal form)、BDD(binary decision diagram)、その他のサブバリアントに事前コンパイルする。
しかし、順序づけられたBDD(OBDD)表現を持つPB制約が存在することが示されており、従って推論されたCNFエンコーディングは指数的サイズである。
DNNFはOBDDよりも簡潔であるため、サイズ爆発を避けるためにDNNF経由のエンコーディングが好ましい。
しかし本稿では,DNNFがすべて指数的サイズを必要とするPB制約の存在を実証する。
関連論文リスト
- A shallow dive into the depths of non-termination checking for C programs [3.4144415576897624]
Unintended Non-Termination (NT) は、現実世界のソフトウェア開発において一般的である。
実世界のソフトウェアにも有効であるNTチェックのための健全で効率的な手法を提案する。
幅広いソフトウェアベンチマーク実験により、この手法が最先端のNTチェッカーより優れていることが示された。
論文 参考訳(メタデータ) (2024-09-04T22:47:46Z) - Approximate quantum error correcting codes from conformal field theory [0.0]
局所的デファス化チャネル下での汎用1+1D CFT符号について検討する。
連続対称性を持つCFT符号が共変符号の回復忠実度の境界を飽和させることを示す。
論文 参考訳(メタデータ) (2024-06-13T19:40:36Z) - Structured d-DNNF Is Not Closed Under Negation [0.0]
構造化d-DNNFとSDDはどちらも、OBDDよりも指数関数的に簡潔である。
構造化d-DNNFは、ポリ時間否定、解離、存在的操作をサポートしていないことを示す。
また、等価サイズの構造d-DNNFを持つ関数が存在するが、SDDのような表現は存在しないことを示す。
論文 参考訳(メタデータ) (2024-02-07T13:31:59Z) - Belief Propagation Decoding of Quantum LDPC Codes with Guided Decimation [55.8930142490617]
BPガイドデシミテーション(BPGD)に基づくQLDPC符号のデコーダを提案する。
BPGDは非収束によるBP故障率を著しく低下させる。
論文 参考訳(メタデータ) (2023-12-18T05:58:07Z) - Tokenization and the Noiseless Channel [71.25796813073399]
優れたトークン化器は、ある入力がモデルに伝達される手段であるチャネルの使用率を高める。
機械翻訳では、複数のトークン化器において、$alpha = 2.5$のR'enyiエントロピーがtextscBleu: $0.78$と非常に強い相関を持つことがわかった。
論文 参考訳(メタデータ) (2023-06-29T10:32:09Z) - Compacting Binary Neural Networks by Sparse Kernel Selection [58.84313343190488]
本稿は,BNNにおけるバイナリカーネルの分散化がほぼ不可能であることを示すものである。
我々は、選択過程をエンドツーエンドに最適化するだけでなく、選択したコードワードの非反復的占有を維持できる置換ストレートスルー推定器(PSTE)を開発した。
実験により,提案手法はモデルサイズとビット幅の計算コストの両方を削減し,同等の予算下での最先端のBNNと比較して精度の向上を実現する。
論文 参考訳(メタデータ) (2023-03-25T13:53:02Z) - Graph Neural Networks for Channel Decoding [71.15576353630667]
低密度パリティチェック(LDPC)やBCH符号など、様々な符号化方式の競合復号性能を示す。
ニューラルネットワーク(NN)は、与えられたグラフ上で一般化されたメッセージパッシングアルゴリズムを学習する。
提案するデコーダを,従来のチャネル復号法および最近のディープラーニングに基づく結果と比較した。
論文 参考訳(メタデータ) (2022-07-29T15:29:18Z) - Understanding Deep Learning via Decision Boundary [81.49114762506287]
決定境界(DB)の変動が低いニューラルネットワークはより一般化可能であることを示す。
アルゴリズムDBの変数と$(epsilon, eta)$-data DBの変数という2つの新しい概念が、決定境界の変数を測定するために提案されている。
論文 参考訳(メタデータ) (2022-06-03T11:34:12Z) - DPO: Dynamic-Programming Optimization on Hybrid Constraints [26.704502486686128]
ベイズ推定において、最も可能性の高い説明(MPE)問題は、いくつかの証拠から最も高い確率で変数のインスタンス化を要求する。
ブール MPE は (部分重み付き) MaxSAT への還元によって解けることが知られている。
我々はDPMC上に構築し,MPEを正確に解く動的プログラミングであるDPOを導入する。
論文 参考訳(メタデータ) (2022-05-17T21:18:54Z) - 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) - Improved Branch and Bound for Neural Network Verification via Lagrangian
Decomposition [161.09660864941603]
ニューラルネットワークの入出力特性を公式に証明するためのブランチとバウンド(BaB)アルゴリズムのスケーラビリティを改善します。
活性化に基づく新しい分岐戦略とBaBフレームワークであるブランチとデュアルネットワーク境界(BaDNB)を提案する。
BaDNBは、従来の完全検証システムを大きなマージンで上回り、対数特性で平均検証時間を最大50倍に削減した。
論文 参考訳(メタデータ) (2021-04-14T09:22:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。