大学における進級・卒業の可否は、履修条件だけでなく、単位の配当（時間割）の制約などもあり、非常に複雑である。そして、履修する側も配当する側も慎重な対応が求められる。この履修条件・時間割の例にあるように、与えられた制約を満たす解を求めるツールとして、背景論理付きSAT(以下SMT)問題を解くSMTSolverがある。本研究では、この履修条件・時間割を例題とし、SMTSolverのZ3py(Z3)を用いて、現在の履修状況から進級・卒業の可否を判定する。そして、この判定式を用いて、単位を落としてしまうことにより次年度に履修ができず、留年に繋がる科目を求解する。本研究で扱う履修条件・時間割問題は、通常のプログラミング言語では煩雑になる計算を簡単に記述できることおよび、SMTSolverの比較的大きな規模の例題になることを期待している。