論文の概要: Proof Generation in CDSAT
- arxiv url: http://arxiv.org/abs/2107.02351v1
- Date: Tue, 6 Jul 2021 02:35:21 GMT
- ステータス: 処理完了
- システム内更新日: 2021-07-08 02:37:42.533902
- Title: Proof Generation in CDSAT
- Title(参考訳): CDSATにおける証明生成
- Authors: Maria Paola Bonacina (Universit\`a degli Studi di Verona, Italy)
- Abstract要約: SMTのCDSAT (Conflict-Driven Satisfiability) フレームワークの主な考え方は要約され、CDSATにおける証明生成へのアプローチへと導かれる。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The main ideas in the CDSAT (Conflict-Driven Satisfiability) framework for
SMT are summarized, leading to approaches to proof generation in CDSAT.
- Abstract(参考訳): SMTのCDSAT (Conflict-Driven Satisfiability) フレームワークの主な考え方は要約され、CDSATにおける証明生成へのアプローチにつながっている。
関連論文リスト
- SibylSat: Using SAT as an Oracle to Perform a Greedy Search on TOHTN Planning [2.2276906461400054]
本稿では,全順序付きHTN問題(TOHTN)を効率的に解くためのSATベースの新しい手法であるSibylSatを提案する。
広く普及しているSATベースのHTNプランナとは対照的に,SibylSatでは,拡張のための有望な分解を識別可能な,フレディな検索アプローチを採用している。
実験により、SybylSatは既存のSATベースのTOHTNアプローチよりも、ほとんどのIPCベンチマークで実行時と計画品質の両方において優れていることが示された。
論文 参考訳(メタデータ) (2024-11-04T12:37:59Z) - Deep Learning and Data Augmentation for Detecting Self-Admitted Technical Debt [6.004718679054704]
Self-Admitted Technical Debt (SATD)は、開発者がテキストアーティファクトを使用して、既存の実装が最適でない理由を説明する状況を指す。
SATD と BERT のバイナリ識別に BiLSTM アーキテクチャを用い,様々な SATD の分類を行った。
異なるアーティファクトから派生した様々なデータセットからSATDを識別・分類するための2段階のアプローチを提案する。
論文 参考訳(メタデータ) (2024-10-21T09:22:16Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳(メタデータ) (2024-07-14T01:43:07Z) - Certified MaxSAT Preprocessing [9.717669529984349]
MaxSATはNP-hard最適化問題の解決に有効なアプローチとなっている。
MaxSATソルバの正確性を保証することは、依然として重要な関心事である。
そこで本研究では,最新のMaxSATプリプロセッシング手法の正当性を証明するために,擬似ブール検定ロギングをどのように利用できるかを示す。
論文 参考訳(メタデータ) (2024-04-26T10:55:06Z) - Exploiting Self-Supervised Constraints in Image Super-Resolution [72.35265021054471]
本稿では,SSC-SRと呼ばれる単一画像超解像のための新しい自己監督制約を提案する。
SSC-SRは、安定性を高めるために指数移動平均によって更新された二重非対称パラダイムとターゲットモデルを用いることで、画像の複雑さのばらつきに一意に対処する。
SSC-SRフレームワークはさまざまなベンチマークデータセットに対して,EDSR平均0.1dB,SwinIR平均0.06dBの大幅な拡張を実現している。
論文 参考訳(メタデータ) (2024-03-30T06:18:50Z) - GLS-CSC: A Simple but Effective Strategy to Mitigate Chinese STM Models'
Over-Reliance on Superficial Clue [51.713301130055065]
STMモデルにおける表面的手がかりの影響を解析・緩和する。
本稿では,GLS-CSC (Superficial Clue) を含む学習サンプルをトレーニング戦略として提案する。
GLS-CSCは,中国のSTMモデルの堅牢性と一般化性の向上の観点から,既存の手法よりも優れていることを示す。
論文 参考訳(メタデータ) (2023-09-08T07:10:57Z) - A Neural Network-based SAT-Resilient Obfuscation Towards Enhanced Logic
Locking [3.076761061950216]
本稿では,ニューラルネットワークを用いた unSAT 節変換器 SATConda を提案する。
SATCondaは最小限の領域と電力オーバーヘッドを発生させ、元の機能を不必要なセキュリティで保存する。
SATCondaをISCAS85およびISCAS89ベンチマークで評価した。
論文 参考訳(メタデータ) (2022-09-13T07:59:27Z) - Semantic-Preserving Adversarial Code Comprehension [75.76118224437974]
本稿では,セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・セマンティック・アタック(SPACE)を提案する。
実験と分析により、SPACEは、コードに対するPrLMのパフォーマンスを高めながら、最先端の攻撃に対して堅牢であることを示す。
論文 参考訳(メタデータ) (2022-09-12T10:32:51Z) - DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
We present DeepSAT, a novel-to-end learning framework for the Boolean satisfiability (SAT) problem。
DeepSATは最先端の学習ベースSATソリューションに対して,大幅な精度向上を実現している。
論文 参考訳(メタデータ) (2022-05-27T03:20:42Z) - DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving [45.21499915442282]
本稿では,ハイブリッド制約を用いた一般化MaxSAT問題の解法について,新しい動的プログラミング手法を提案する。
我々の汎用フレームワークは、MaxSAT、Min-MaxSAT、MinSATといったCNF-MaxSATの多くの一般化をハイブリッド制約で認めている。
実験の結果、DPMSは様々な手法に基づく他のアルゴリズムがすべて失敗し、特定の問題を迅速に解決できることがわかった。
論文 参考訳(メタデータ) (2022-05-08T00:31:53Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。