高效地确定布尔方程的可满足性——简称为 SAT 问题——在各种工业问题中至关重要。近年来，深度学习方法的出现为增强 SAT 求解带来了巨大潜力。然而，该领域发展的主要障碍是缺乏大型、现实的训练数据集。目前大多数公开数据集要么是随机生成的，要么极其有限，只包含来自无关问题族的几个示例。这些数据集不足以对深度学习方法进行有意义的训练。鉴于此，研究人员开始探索生成式技术来创建更准确地反映实际情况中遇到的 SAT 问题的训练数据。迄今为止，这些方法要么无法生成具有挑战性的 SAT 问题，要么存在时间可扩展性障碍。在本文中，我们通过识别和操作影响问题“难度”的关键因素——即核心——来解决这两个问题。虽然之前的一些工作已经解决了核心问题，但由于传统启发式核心检测技术的成本高昂，导致时间成本不可接受地高。我们引入了一种使用图神经网络的快速核心检测程序。我们的实证结果表明，我们可以有效地生成难以解决的问题，并保留原始示例问题的关键属性。我们通过实验表明，生成的合成 SAT 问题可以在数据增强设置中使用，以提供改进的求解器运行时间预测。