Satisfiability Modulo Theories and Chiral Heterotic String Vacua with Positive Cosmological Constant

TL;DR

This paper demonstrates the effectiveness of SAT/SMT solvers in rapidly identifying chiral heterotic string models with positive cosmological constant, significantly outperforming exhaustive search methods in speed and scalability.

Contribution

It introduces the application of SAT/SMT techniques to string model construction, showing substantial speed improvements and scalability for finding solutions in large parameter spaces.

Findings

SMT-based techniques are simple and effective for this problem.

Boolean SAT encoding significantly speeds up satisfiability determination.

The method scales well beyond the initial problem size.

Abstract

We apply Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers in the context of finding chiral heterotic string models with positive cosmological constant from $\mathbb{Z}_2\times \mathbb{Z}_2$ orbifolds. The power of using SAT/SMT solvers to sift large parameter spaces quickly to decide satisfiability, both to declare and prove unsatisfiability and to declare satisfiability, are demonstrated in this setting. These models are partly chosen to be small enough to plot the performance against exhaustive search, which takes around 2 hours 20 minutes to comb through the parameter space. We show that making use of SMT based techniques with integer encoding is rather simple and effective, while a more careful Boolean SAT encoding provides a significant speed-up -- determining satisfiability or unsatisfiability has, in our experiments varied between 0.03 and 0.06 seconds, while determining all models (where models exist) took 19 seconds for a constraint system that allows for 2048 models and 8.4 seconds for a constraint system that admits 640 models. We thus gain several orders of magnitude in speed, and this advantage is set to grow with a growing parameter space. This holds the promise that the method scales well beyond the initial problem we have used it for in this paper.