  There exist various methods and tools to size solar photovoltaic systems;
however, these tools rely on simulations, which do not cover all aspects of the
design space during the search for optimal solution. In prior studies in
optimal sizing, the focus was always on criteria or objectives. Here, we
present a new sound and automated approach to obtain optimal sizing using an
unprecedented program synthesis. Our variant of counterexample guided inductive
synthesis (CEGIS) approach has two phases linking the technical and cost
analysis: first we synthesize a feasible candidate based on power reliability,
but that may not achieve the lowest cost; second, the candidate is then
verified iteratively with a lower bound cost via symbolic model checking. If
the verification step does not fail, the lower bound is adjusted; and if it
fails, a counterexample provides the optimal solution. Experimental results
using seven case studies and commercial equipment data show that our synthesis
method can produce within an acceptable run-time the optimal system sizing. We
also present a comparative with a specialized simulation tool over real
photovoltaic systems to show the effectiveness of our approach, which can
provide a more detailed and accurate solution than that simulation tool.
