@article{oai:nagoya.repo.nii.ac.jp:00013051, author = {馬野, 洋平 and 酒井, 正彦 and 西田, 直樹 and 坂部, 俊樹 and 草刈, 圭一朗 and UMANO, Yohei and SAKAI, Masahiko and NISHIDA, Naoki and SAKABE, Toshiki and KUSAKARI, Keiichirou}, issue = {1}, journal = {電子情報通信学会論文誌. D, 情報・システム}, month = {Jan}, note = {近年,高速な充足可能性判定ツール(SATソルバ)の開発が進んでいる.これらのツールでは,BCPと呼ばれる変数値の推論とそのバックトラックが実行時間の大半を占めていることが多く,その処理を効率化できればSATソルバの高速化が可能となる.本論文では,「n個の変数のうち,ちょうどk個が真」という基本対称関数に基づく節を導入することにより入力する論理式の大きさが減少することに注目し,SATソルバの効率化を目指す.実際にSATソルバでよく用いられるDPLLアルゴリズムを,基本対称関数に基づく節を導入したCNFを扱えるよう拡張し,その有効性を実験により確かめた.}, pages = {1--9}, title = {基本対称関数に基づく節をもつCNF論理式の充足可能性判定}, volume = {J93-D}, year = {2010} }