我々は以前，制約ソルバを用いて，自動生成した述語の組み合せからなるプログラムの事前条件で最弱なもの（準最弱事前条件）を推定する手法を提案した．これには minimal unsatisfiable core (MUC) の列挙を利用していたが，計算コストが高いことが主な課題であった． MUCの列挙は minimal correction subset (MCS) の列挙を介して実現できるが，MUCの列挙が高コストである要因の１つは，このMCS列挙の高コスト性にある．<br />
<br />
我々は本手法を通じて得られるMCSが (1)サイズを一定値に設定できる (2) MUC の一部を先に求めておくことで列挙を効率化できる，の２性質を持つことに着目し，それら性質を活かした高速化アルゴリズムを３種類提案する．<br />
<br />
3アルゴリズムそれぞれについて性能評価を行ったところ，いずれも既存手法と比較して速度向上が確認でき，MUC列挙にかかる速度比は最大10.7倍程度であった．本論文ではその結果を報告し，また各アルゴリズムの得失について考察する．