文献

J-GLOBAL ID：202202282725530958   整理番号：22A0446559

Int-Bursingによるビット-プレシス推論【JST・京大機械翻訳】

Bit-Precise Reasoning via Int-Blasting

著者 (9件)： Zohar Yoni (Bar-Ilan University, Ramat Gan, Israel) ,  Irfan Ahmed (Stanford University, Stanford, USA) ,  Mann Makai (Stanford University, Stanford, USA) ,  Niemetz Aina (Stanford University, Stanford, USA) ,  Notzli Andres (Stanford University, Stanford, USA) ,  Preiner Mathias (Stanford University, Stanford, USA) ,  Reynolds Andrew (The University of Iowa, Iowa City, USA) ,  Barrett Clark (Stanford University, Stanford, USA) ,  Tinelli Cesare (The University of Iowa, Iowa City, USA)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13182  ページ： 496-518  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 充足可能性モデュロ理論(SMT)の文脈におけるビットプレシス推論のための最先端技術は,入力公式が最初に単純化され,次に等充足可能な命題式に翻訳されるビットブラストと呼ばれるSATベースの技術である。この技術の主な限界は,特に大きなビット幅と算術演算子の存在下でスケーラビリティである。命題論理ではなく整数演算の拡張への翻訳に基づいて,イントブラストと呼ぶ代替技術を導入した。いくつかの翻訳を提示し,それらの違いを議論し,ビットベクトル解のための書込み規則候補の検証から生じるベンチマークと,SMT-LIBからのベンチマークからそれらを評価した。また,スマート契約検証から生じる35のベンチマークに関する予備的結果を示した。評価は,この技術が,大きなビット幅を有するベンチマークに対して特に有用であり,最先端技術の状況ができないベンチマークを解決できることを示した。Copyright Springer Nature Switzerland AG 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 簡素化 ,  演算 ,  命題論理 ,  命題 ,  *ベンチマーク

分類 (2件)： 論理代数  (JB03000H) ,  人工知能  (JE08000Z)

タイトルに関連する用語 (3件)： INT ,  ビット ,  推論