Abstract: It is common in mathematical "solvers" to have arbitrary choices in algorithms. These choices do not affect correctness, but can have a great impact on the time/space required by the solver, and the quality of the solutions it produces. Good heuristics for making such decisions are thus very important. It is natural to consider applying machine learning to learn these heuristics, especially in situations where theory does not currently shed much light on how to develop good heuristics by hand.
This talk concerns applying machine learning to a particular choice in the algorithm for constructing Non-uniform Cylindrical Algebraic Decompositions (NuCADs), which can be used for solving systems of non-linear polynomial constraints over the reals. A NuCAD decomposes Euclidean space into cells by refinement: at each step a cell is considered, constraints are evaluated at a sample point from within the cell, and one constraint is chosen as the basis for refining that cell. This choice of constraint is what we propose to learn a heuristic for. The challenges to applying machine learning to this problem are considerable, and the novel techniques we developed to overcome them will, we hope, be applicable to many problems in the area.
