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