抄録

◎中山寛己・千代英一郎（成蹊大）

充足可能性判定問題とは, 論理式が真となるような変数への値の割り当てが存在するかどうかを判定する問題である. プログラム検査において，様々な検査問題を充足可能性判定問題に帰着して解く方法が知られているが，ループ停止性検査等で必要となる複雑な論理式の場合，判定に数日を要することもあり，実用上の課題となっている．本発表では，論理式中の変数の値域を限定することで1度の検査にかかる時間を減らし, 繰り返し検査することで論理式を満たす値を推定する方法について検討を行った結果について報告する．提案手法で課題となるのが，1度に検査する範囲を狭めることで検査にかかる時間は短くなるが， 論理式を満たす値を見つけにくくなるというトレードオフである．予備評価の結果, いくつかの論理式に対して, トレードオフの適切な解消点を得ることができた．