2024-03-29T05:13:07Z
https://nagoya.repo.nii.ac.jp/oai
oai:nagoya.repo.nii.ac.jp:00013051
2023-01-16T03:59:56Z
312:313:314
基本対称関数に基づく節をもつCNF論理式の充足可能性判定
Solving Satisfiability of CNF Formulas with Clauses Based on Elementary Symmetric Functions
馬野, 洋平
酒井, 正彦
西田, 直樹
坂部, 俊樹
草刈, 圭一朗
UMANO, Yohei
SAKAI, Masahiko
NISHIDA, Naoki
SAKABE, Toshiki
KUSAKARI, Keiichirou
open access
Copyright (C) 2010 IEICE
SATソルバ
充足可能性
基本対称関数
高速化
近年,高速な充足可能性判定ツール(SATソルバ)の開発が進んでいる.これらのツールでは,BCPと呼ばれる変数値の推論とそのバックトラックが実行時間の大半を占めていることが多く,その処理を効率化できればSATソルバの高速化が可能となる.本論文では,「n個の変数のうち,ちょうどk個が真」という基本対称関数に基づく節を導入することにより入力する論理式の大きさが減少することに注目し,SATソルバの効率化を目指す.実際にSATソルバでよく用いられるDPLLアルゴリズムを,基本対称関数に基づく節を導入したCNFを扱えるよう拡張し,その有効性を実験により確かめた.
社団法人電子情報通信学会
2010-01-01
jpn
journal article
VoR
http://hdl.handle.net/2237/14972
https://nagoya.repo.nii.ac.jp/records/13051
http://www.ieice.org/jpn/trans_online/index.html
1880-4535
電子情報通信学会論文誌. D, 情報・システム
J93-D
1
1
9
https://nagoya.repo.nii.ac.jp/record/13051/files/399.pdf
application/pdf
389.2 kB
2018-02-20