2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み

• 日野, 善信

• 酒井, 正彦

• 坂部, 俊樹

• 草刈, 圭一朗

• 西田, 直樹

• HINO, Yoshizane

• SAKAI, Masahiko

• SAKABE, Toshiki

• KUSAKARI, Keiichirou

• NISHIDA, Naoki

書誌事項

タイトル別名

• 2 リテラル カンシホウ デ ジッソウ サレタ SAT ソルバ エ ノ キホン タイショウセツ ショリ キノウ ノ クミコミ
• Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme

抄録

論理式の充足可能性判定問題(SAT問題)を解くSATソルバの高速化の一手法として,馬野らは2010年にCNFへの基本対称節の導入を提案した.彼らのSATソルバは,節中の真リテラルと偽リテラルの個数をカウンタに保持する方法による実現であるためバックトラックが重いという欠点がある.そこで, Minisatに代表される現在主流のソルバが採用する節あたり二つのリテラルを監視する方法(2リテラル監視法)に基づく実現が可能であれば,バックトラックが軽くなるため更なる高速化が期待できる.しかしながら,基本対称節の性質から二つのリテラルのみの監視では十分でなく,そのままでは高速化が期待できない.本論文では,通常の節(OR節)は二つのリテラルを監視し,基本対称節については節中のリテラルをすべて監視する方法を提案する,実際にこれをMinisatに組み込むことで,本手法の有効性を評価する.

収録刊行物

• 電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス

  電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス 111 (268), 67-72, 2011-10

  一般社団法人電子情報通信学会

キーワード

• SATソルバ
• 基本対称節
• 2リテラル監視法
• 全リテラル監視法
• SAT solver
• elementary symmetric clauses
• two watched literals
• all watched literals

詳細情報

• CRID: 1050845763734805376
• NII論文ID: 110008900205
• NII書誌ID: AA1123312X
• HANDLE: 2237/23546
• NDL書誌ID: 023343877
• ISSN: 09135685
• Web Site: https://nagoya.repo.nii.ac.jp/records/21402
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I023343877
• 本文言語コード: ja
• 資料種別: journal article
• データソース種別:
  • IRDB
  • NDL
  • CiNii Articles
  • KAKEN