文献

J-GLOBAL ID：201802261038675384   整理番号：18A0201488

CDCL SATソルバのための相反する速度に基づく分岐発見的方法【Powered by NICT】

Conflicting rate based branching heuristic for CDCL SAT solvers

著者 (4件)： Chen Qingshan (School of Information Science and Technology, Southwest Jiaotong University, Chengdu 611756, China) ,  Xu Yang (National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Chengdu 610031, China) ,  Wu Guanfeng (School of Information Science and Technology, Southwest Jiaotong University, Chengdu 611756, China) ,  He Xingxing (National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Chengdu 610031, China)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： ISKE  ページ： 1-5  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 最新のSATソルバは通常各葛藤上のバンプ値を増加することによって対応する変数のスコアを更新した。それらの値は,通常,一定であったが,判定レベルと対立とは無関係であった。,局所衝突最適化のためのより効率的であるが大域的探索では弱かった。本論文では,CRB法(相反する速度分岐),これはVSIDSが異なる実装の変種を提案した。CRBは変数はコンフリクト解析に使用されている場合に決定レベルと紛争を統合したスコアを更新する。MiniSatソルバーとCRBを統合し,SATレース2015からインスタンスのCRBを評価した。実験結果は,提案した戦略は,EVSIDS以上例を解き,SATおよびUNSAT両事例で性能を改善できることを示した。Copyright 2018 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： *発見的方法 ,  バンプ ,  最適化
準シソーラス用語： スコア ,  *ソルバ , 【Automatic Indexing@JST】

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

タイトルに関連する用語 (4件)： SAT ,  ソルバ ,  分岐 ,  発見的方法