Minimizing Pentagons in the Plane through Automated Reasoning

We study $\mu_5(n)$, the minimum number of convex pentagons induced by $n$ points in the plane in general position. Despite a significant body of research in understanding $\mu_4(n)$, the variant concerning convex quadrilaterals, not much is known about $\mu_5(n)$. We present two explicit constructions, inspired by point placements obtained through a combination of Stochastic Local Search and a program for realizability of point sets, that provide $\mu_5(n) \leq \binom{\lfloor n/2 \rfloor}{5} + \binom{\lceil n/2 \rceil}{5}$. Furthermore, we conjecture this bound to be optimal, and provide partial evidence by leveraging a MaxSAT encoding that allows us to verify our conjecture for $n \leq 16$.