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

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.

arXiv comment16 pages, 2 Figures

References in corpus (35)

• Construction of Realistic Standard--like Models in the Free Fermionic Superstring Formulation
• Perturbative and Non-Perturbative Partial Supersymmetry Breaking; N=4 -> N=2 -> N=1
• String derived MSSM and M-theory Unification
• Towards a Non-Supersymmetric String Phenomenology
• N=1 supersymmetric SU(4)xSU(2)LxSU(2)R effective theory from the weakly coupled heterotic superstring
• Z_2\times Z_2$ orbifold compactification as the origin of realistic free fermionic models
• Chiral family classification of fermionic Z2xZ2 heterotic orbifold models
• Classification of the chiral Z2XZ2 fermionic models in the heterotic superstring
• Left-Right Symmetric Heterotic-String Derived Models
• On orbifolds and free fermion constructions
• Spinor-Vector Duality in fermionic Z2XZ2 heterotic orbifold models
• Exophobic Quasi-Realistic Heterotic String Vacua
• Classification of Heterotic Pati-Salam Models
• Chiral Heterotic Strings with Positive Cosmological Constant
• Spinor-Vector Duality in Heterotic SUSY Vacua
• Flat Directions in Left-Right Symmetric String Derived Models
• Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
• Conformal Aspects of Spinor-Vector Duality
• Non-Tachyonic Semi-Realistic Non-Supersymmetric Heterotic String Vacua
• Minimal Standard Heterotic String Models
• Top Quark Mass in Exophobic Pati--Salam Heterotic String Model
• Deep learning in the heterotic orbifold landscape
• Spinor-Vector Duality in N=2 Heterotic String Vacua
• Classification of Standard-like Heterotic-String Vacua
• Classification of Flipped SU(5) Heterotic-String Vacua
• Stability, enhanced gauge symmetry and suppressed cosmological constant in 9D heterotic interpolating models
• Classification of Non-Supersymmetric Pati-Salam Heterotic String Models
• Towards the Classification of Tachyon-Free Models From Tachyonic Ten-Dimensional Heterotic String Vacua
• Stable Three Generation Standard--like Model From a Tachyonic Ten Dimensional Heterotic--String Vacuum
• Classification of Left-Right Symmetric Heterotic String Vacua
• String Phenomenology From a Worldsheet Perspective
• The Flipped SU(5) String Vacua Classification: A Variation Of The SO(10) Breaking Basis Vector
• Type $\bar{0}$ Heterotic String Orbifolds
• Doublet-Triplet Splitting in Fertile Left-Right Symmetric Heterotic String Vacua
• Computing Tropical Prevarieties with Satisfiability Modulo Theories (SMT) Solvers

Cited by in corpus (8)

• Marginal deformations of heterotic interpolating models and exponential suppression of the cosmological constant
• Breeding realistic D-brane models
• Target Space Duality of Non-Supersymmetric String Theory
• Interpolation and Exponentially Suppressed Cosmological Constant in Non-Supersymmetric Heterotic Strings with General ${\mathbb{Z}}_2$ Twists
• Towards Classification of $\mathcal{N}=1$ and $\mathcal{N}=0$ Flipped $SU(5)$ Asymmetric ${\mathbb{Z}}_2\times {\mathbb{Z}}_2$ Heterotic String Orbifolds
• Free Fermionic Constructions of Heterotic Strings
• Classification of Pati--Salam Asymmetric ${\mathbb{Z}}_2\times {\mathbb{Z}}_2$ Heterotic String Orbifolds
• Gauge Symmetry Enhancement by Wilson Lines in Twisted Compactification