Improving the performance of the dReal nonlinear solver by exploring novel branching strategies
I will try to improve the dReal solver [1] for nonlinear theories over the reals. dReal can be used for instance to determine constraints on robot movements whether or not a task is feasible for a certain robotic configuration and what certain robot dimensions are suitable for a particular task.My responsibility in this project will be to studying and developing heuristics for the branching used in the ICP solver perhaps borrowing from existing strategies used in SAT solvers with hopes of improving the speed and scalability of dReal. I will be experimenting with branching heuristics adapted from strategies used in SAT solvers as well as Monte Carlo Tree Search.

I’ve studied mathematics since elementary school and I started studying computer science in early high school. I hope to build on that knowledge with this project; I think it’s very interesting to learn about the different techniques people have used with SAT solvers and other programs and how to adapt those to be used in an alternative setting.