--- title: "「Z3とSymPyを用いた数学入試整数問題自動求解システムの作成」" authors: "岡本優生" seo: description: "本研究では、入試の整数問題を解くことができるシステムの作成を行った。本システムは、変数・制約式を入力することにより、その制約式を満たす解の列挙を行う。その際、Z3という数理理論や論理式の探索を行うことができるソルバを使用した。また、SymP…" sidebar: hidden: true --- 本研究では、入試の整数問題を解くことができるシステムの作成を行った。本システムは、変数・制約式を入力することにより、その制約式を満たす解の列挙を行う。その際、Z3という数理理論や論理式の探索を行うことができるソルバを使用した。また、SymPyという数式処理ライブラリを用いることにより解くことができる問題の幅を広げた。さらに、システムのGUI化を行い、入力した式を理解しやすいように数学的記法表記でグラフィカルに表示を行うことで直観的に理解し、操作を行うことを可能にした。解が無限に存在したり、求解に長時間を要したときのためにタイムアウト機能も搭載した。