文献

J-GLOBAL ID：202202256262681325   整理番号：22A1105012

定量化Boole公式における移動定義変数【JST・京大機械翻訳】

Moving Definition Variables in Quantified Boolean Formulas

著者 (3件)： Reeves Joseph E. (Carnegie Mellon University, Pittsburgh, Pennsylvania, United States) ,  Heule Marijn J. H. (Carnegie Mellon University, Pittsburgh, Pennsylvania, United States) ,  Bryant Randal E. (Carnegie Mellon University, Pittsburgh, Pennsylvania, United States)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13243  ページ： 462-479  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 定義変数による定量化Boole式における問題変数は,クラーサール形式におけるコンパクトな表現を可能にした。一般的に,これらの定義変数を最内量子化器レベルに置いた。いくつかの構造情報を回復するために,定義変数を,それらを定義する変数に最も近い量子化器レベルに移動させる前処理技術を導入した。QRAT証明システムにおける動きを表現し,独立証明チェッカーによる検証を可能にした。QBFEVAL’20競争ベンチマークにおける定義変数移動を評価した。運動は競争のトップソルバの性能を著しく改善した。可変運動をプレプロセッサBloqqerと組合せることは,Bloqqer単独使用と比較してソルバ性能を改善した。Copyright The Author(s) 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 前処理 ,  量子化器 ,  応用プログラム ,  問題 ,  *プリプロセッサ ,  ベンチマーク
準シソーラス用語： ソルバ , 【Automatic Indexing@JST】

分類 (2件)： 論理代数  (JB03000H) ,  計算理論  (JB02000A)

タイトルに関連する用語 (3件)： 定量化 ,  定義 ,  変数