可满足性模理论与具有正宇宙学常数的手征异弦真空
高能物理 - 理论
2021-03-17 v1 高能物理 - 唯象学
摘要
我们在从 轨道空间寻找具有正宇宙学常数的手征异弦模型的背景下应用布尔可满足性(SAT)和可满足性模理论(SMT)求解器。在此背景下展示了使用 SAT/SMT 求解器快速筛取大参数空间以判定可满足性的能力,既可声明并证明不可满足性,也可声明可满足性。这些模型部分被选择得足够小,以便将性能与穷举搜索对比绘图,后者耗时约 2 小时 20 分钟遍历参数空间。我们展示了使用基于整数编码的 SMT 技术相当简单有效,而更精细的布尔 SAT 编码提供了显著加速——在我们的实验中,判定可满足性或不可满足性耗时介于 0.03 至 0.06 秒之间,而确定所有模型(在存在模型时)对于允许 2048 个模型的约束系统耗时 19 秒,对于容纳 640 个模型的约束系统耗时 8.4 秒。因此我们获得了数个数量级的速度提升,且这一优势将随参数空间增大而增长。这预示着该方法可良好扩展到本文所用初始问题之外。
引用
@article{arxiv.2101.03227,
title = {Satisfiability Modulo Theories and Chiral Heterotic String Vacua with Positive Cosmological Constant},
author = {Alon E. Faraggi and Benjamin Percival and Sven Schewe and Dominik Wojtczak},
journal= {arXiv preprint arXiv:2101.03227},
year = {2021}
}
备注
16 pages, 2 Figures