Satisfiability modulo theories and chiral heterotic string vacua with positive cosmological constant



Faraggi, Alon E ORCID: 0000-0001-7123-6414, Percival, Benjamin, Schewe, Sven ORCID: 0000-0002-9093-9518 and Wojtczak, Dominik ORCID: 0000-0001-5560-0546
(2021) Satisfiability modulo theories and chiral heterotic string vacua with positive cosmological constant. PHYSICS LETTERS B, 816. p. 136187.

Access the full-text of this item by clicking on the Open Access link.
[thumbnail of 2101.03227v1.pdf] Text
2101.03227v1.pdf - Submitted version

Download (362kB) | Preview

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.

Item Type: Article
Additional Information: 16 pages, 2 Figures
Uncontrolled Keywords: hep-th, hep-th, hep-ph
Depositing User: Symplectic Admin
Date Deposited: 25 Jan 2021 08:28
Last Modified: 18 Jan 2023 23:02
DOI: 10.1016/j.physletb.2021.136187
Open Access URL: https://doi.org/10.1016/j.physletb.2021.136187
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3114747