• 馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗: 基本対象関数に基づく節を持つCNF論理式の充足可能性判定, 電子情報通信学会論文誌, Vol.J93-D, No.1, pp.1--9(2010,1).
  Yohei Umano, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari
  Solving Satisfiability of CNF Formulas with Clauses based on Elementary Symmetric Functions, IEICE Trans. on Information and Systems, Vol.J93-D, No.1, pp.1-9(2010) (in Japanese).
  
  概要
  近年，高速な充足可能性判定ツール（SATソルバ）の開発が進んでいる． これらのツールでは，BCPと呼ばれる変数値の推論とそのバックトラックが実行時間の大半を占めていることが多く，その処理を効率化できればSATソルバの高速化が可能となる． 本論文では，「$n$個の変数のうち，ちょうど$k$個が真」という基本対称関数に基づく節を導入することにより入力する論理式の大きさが減少することに注目し，SATソルバの効率化を目指す． 実際にSATソルバでよく用いられるDPLLアルゴリズムを、基本対称関数に基づく節を導入したCNFを扱えるよう拡張し，その有効性を実験により確かめた．
  ABSTRACT
  In recent years, several efficient SAT solvers, which decide satisfiability of boolean formulas, have been developed. Since most of execution time of these solvers is used for value-inferences of variables, called boolean constraint propagation (BCP), and their backtracking, improvements of BCP contribute the efficiency. This paper attempts to improve the efficiency of SAT solvers, focusing on the fact that the number of clauses of a CNF formula decreases by introducing clauses based on elementary symmetric functions. By extending DPLL algorithm, often used in SAT solvers, to treat CNFs having clauses based on elementary symmetric functions, the effectiveness of the approach is shown by experiments.
  j93-D-1.pdf Copyright(C) 2010 IEICE, on line transaction
  
  
• 西田、酒井、山本、阿草、構成子項書換え系の逆計算プログラムの生成， 電子情報通信学会論文誌 Vol.J88-D-I, No.8, pp.1171-1183(2005,8).
  
  概要
  本論文では、与えられたプログラムが定義する関数の逆演算を定義するプログラムの生成法を与えることにより、項書換え系(TRS)の逆計算に取り組む。本生成法では、与えられた構成子TRSが定義する関数の逆計算を定義する条件付TRSを生成し、それを条件部をもたないEV-TRS（書換え規則に右辺のみに現れる変数を許したTRS）に変換する。本手法により生成したEV-TRSの書換えをナローイングにより模倣することで逆計算が行えることを示す。
  
  
• 長島正徳、酒井正彦、坂部俊樹、草刈圭一朗：限量子付き等式理論の 変換に基づく仕様からのプログラム生成、コンピュータソフトウェア, Vol.21, No.4, pp.49-54(2004)
  
  
• 西田直樹、酒井正彦、坂部俊樹：右辺のみに現れる変数を持つ線形構 成子項書換え系の計算の効率化、コンピュータソフトウェア, Vol.21, No.3, pp.40-47(2004)
  
  
• 西田直樹、酒井正彦、坂部俊樹：右辺のみに現れる変数を持つ項書換 え系の計算モデル、コンピュータソフトウェア, Vol.20, No.5, pp.85-89(2003,9)
  
  
• 堀江美保子、酒井正彦、坂部俊樹：オブジェクト指向計算モデルにおける例外 処理機能の型付、コンピュータソフトウェア, Vol.20, No.2, pp.54-58(2003,3).
  
  
• 西田直樹, 酒井正彦, 坂部俊樹, PT関数の逆関数を定義するTRSの生成, コンピュータソフトウエア, Vol.19, No.1, pp.29-33(2002,1).
  
  
• 洪順姫、酒井正彦、坂部俊樹：メタ項書換え計算における規則中に規則を含む 直交メタ項の合流性、コンピュータソフトウェア、Vol.17, No.6, pp.47-51(2000).
  
  
• 粕谷、酒井、山本、阿草、項集合書換え系とその合流性，電子 情報通信学会論文誌 Vol.J80-D-I, No.4, pp.325--334(1997,4).
  
  概要
  本論文では項書換え系（TRS）の書換え規則の両辺を項の集合に拡張した項集合書換え系（TSRS）を提案する．また単純TSRSを定義し，等式論理との関係を議論する．更に，停止性，線形な系における合流性を考察する．交換則などの一般には停止性をもたない場合にも，ある条件を満たせばTSRSは停止性をもつ．従ってTSRSは完備化手続きなどを拡張する手法として有効である．
  
  
• 高橋, 酒井, 外山, 条件付き項書換え系の合流性について, 電子情 報通信学会論文誌, Vol.J79-D-I, No.11, pp.1-6, 1996.
  
  
• 山本、石川、酒井、阿草、共有メモリ型並列計算機における 項書換え系の実現方式，電子情報通信学会論文誌，Vol.J78-D-I, No.6, pp.559--562(1995,6).
  
  
• 川北、酒井、山本、阿草、形式的仕様を用いた再利用モデル， 情報処理学会論文誌，Vol.36, No.5, pp.1050--1058(1995,5).
  
  
• 濱口, 酒井, 山本, 阿草, エラーつき代数的仕様とエラー記述の自動 付加, 電子情報通信学会論文誌, 電子情報通信学会論文誌, Vol.J78-D-I, No.3, pp.323-330, 1995.
  
  
• 酒井, 坂部, 稲垣, 代数的仕様の検証のための被覆集合帰納法, 電子 情報通信学会論文誌, Vol.J75-D-I, No.3, 1992.
  
  
• 酒井, 坂部, 稲垣, コンパイラの代数的仕様記述と自動生成, 電子情 報通信学会論文誌, Vol.J73-D-I, No.12, 1990.
  
  
• 酒井, 坂部, 稲垣, 代数的仕様記述法に基づく言語処理系の自動生成 システム Lass, 電子情報通信学会論文誌, Vol.J73-D-I, No.10, 1990.
  
  
• 酒井, 坂部, 稲垣, 抽象データ型の代数的仕様の直接実現系Cdimple, コンピュータソフトウエア, Vol.4, No.4, 1987.
  
  
• 水野健一、草刈圭一朗、酒井正彦、坂部俊樹：左辺が一致するオーバ レイ性を持つ左線形TRSの正規化戦略、2003年度冬のLAシンポジウム， pp.37.1--37.6(2004,2). 計算機科学基礎理論の新展開、京都大学数理解析研 究所講究録, No.1375, pp.247-252(2004).(kokyuroku2004.pdf)
  
  
• 粕谷英人、酒井正彦、山本晋一郎、阿草清滋：項集合書換え系の 完備化について、電子情報通信学会技術報告，SS98-66, pp.25-31(1998,12).
  
  

---

Last modified: Jan.06.2016 by Masahiko Sakai(mail: sakai at i.nagoya-u.ac.jp).