文献

J-GLOBAL ID：202102275188851568   整理番号：21A0029455

動的対称性ハンドリングベースのSATソルバのUNSAT結果の認証について【JST・京大機械翻訳】

On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers

著者 (2件)： Tchinda Rodrigue Konan (Department of Mathematics and Computer Science, Faculty of Sciences, University of Dschang, Dschang, Cameroon) ,  Djamegni Clementin Tayou (Department of Mathematics and Computer Science, Faculty of Sciences, University of Dschang, Dschang, Cameroon)
資料名： Constraints  (Constraints)
巻： 25  号： 3-4  ページ： 251-279  発行年： 2020年 
JST資料番号： W4195A  ISSN： 1383-7133  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： SATソルバは,UNSAT結果が時間臨界である特別な意味を持つ多くのアプリケーションで現在使用されている。SATインスタンスは時々,解像度のみの指数である短い証明を生成するために利用できる対称性を示す。しかしながら,現在の不満足証明フォーマットは,動的対称性処理に基づく対称学習を支持しない。本論文では,DRUPの拡張であるDSRUP(Delete Symmetry Reverse University)と呼ばれる新しい証明フォーマット(Delete Reverse Universe Projectation)を提案し,対称学習を実行するSATソルバのUNSAT請求を認証するために考案した。最初に,CNF式の対称性を検証する問題は,NP-ハードのTuringであることを示した。これにより,RUP対称性と呼ばれる新しいタイプの対称性の定義,すなわち,効率的にチェックできるシンタクチック対称性より一般的な対称性のクラスを定義した。DSRUP証明フォーマットを形式的に記述して,検証アルゴリズムを提供してDSRUP証明書を検証した。最後に,DSRUP検査アルゴリズムの実装を用いて,SAT競合から引き出される不充足対称ベンチマーク上の最先端の動的対称性ハンドリングベースSATソルバで得られた実験結果を提供した。Copyright Springer Science+Business Media, LLC, part of Springer Nature 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  *対称性 ,  学習 ,  分解能 ,  臨界 ,  応用プログラム ,  *力学的対称性 ,  ベンチマーク
準シソーラス用語： 証明書 ,  *ソルバ , 【Automatic Indexing@JST】

著者キーワード (4件)： SAT解決 ,  証明書 ,  動的対称性の取り扱い ,  UNSAT証明書

分類 (3件)： 計算理論  (JB02000A) ,  論理代数  (JB03000H) ,  人工知能  (JE08000Z)

タイトルに関連する用語 (5件)： 動的対称性 ,  ハンドリング ,  SAT ,  ソルバ ,  認証