[2B4] [General Session] 1. Basis / Theory

[2B4-04] Search Space Reduction in Automatically Solving Elementary Number Theory Problems in National Center Test

〇Shinya Inuzuka¹, Takuya Matsuzaki¹, Satoshi Sato¹ (1. Nagoya University)

Keywords:Todai Robot Project

We have been developing a number problem solver for National Center Test for University Admissions (NCTUA). The solver searches for a series of equivalence-preserving transformation of an input formula that results in a quantifier-free formula, from which the answer can be easily deduced. However, the increase of the search space hampered the capability of the solver. We introduced formula normalization and extended matching rules in the search in order to reduce the search space. Experimental results show that this method drastically reduces the search space and shorten the execution time.