测量SAT实例的难度

Question

给定SAT的实例，我希望能够估计解决实例将是多么困难。

一种方法是运行现有的求解器，但这种挫败是估计难度的目的。第二种方法可能是将条款与变量的比率如随机-SAT中的相变所做的那样，但我敢肯定存在更好的方法。

给定SAT的实例，是否有一些快速的启发式方法可以衡量难度？唯一的条件是，这些启发式方法比实际运行实例上现有的SAT求解器要快。

---

相关问题

哪些SAT问题很容易？ 在cstheory.se上。这个问题询问了可访问的实例集。这是一个类似的问题，但不完全相同。我对一个启发式的启发式感兴趣，该启发式是一个实例，对这个实例是否很难解决。

Answer 1

通常，这是一个非常相关且有趣的研究问题。 “一种方法是运行现有的求解器……”这甚至可以告诉我们什么？我们可以从经验上看到，对于特定的求解器或特定算法/启发式算法，实例似乎很难，但是它真正证明了实例的硬度呢？

追求的一种方法是识别导致有效算法的实例的各种结构特性。确实，这些属性更容易被“易于识别”。一个示例是使用各种图形宽度参数测量的基础约束图的拓扑。例如，知道实例可以在多项式时间内解决，如果基础约束图的树宽是由常数界定的。

另一种方法集中在 隐藏的结构 实例。一个例子是 后门套装, ，意思是一组变量，因此当它们实例化时，其余问题简化为可拖动类。例如， Williams等，2003 1]证明，即使考虑到寻找后门变量的成本，只要集合足够小，人们仍然可以通过重点关注后门来获得总体计算优势。此外， Dilkina等，2007 2]请注意，一个求解器称为 萨茨 - 兰德 非常擅长在一系列实验域中找到小型强的后门。

最近， Ansotegui等，2008 3]提出使用类似树状的空间复杂性作为基于DPLL的求解器的度量。他们证明，恒定的空间也意味着存在多项式时间决策算法，其空间为多项式的程度（本文中的定理6）。而且，它们显示了空间是 较小 比周期切割的大小。实际上，在某些假设下，该空间也小于后门的大小。

他们还正式化了我认为您所追求的东西，也就是说：

找到一个$ psi $的度量，以及给定公式$ gamma $确定时间$ o（n^{ psi（ gamma）}）$的算法。措施越小，它的特征越好 公式的硬度.

---

1]威廉姆斯，瑞安，卡拉·P·戈麦斯和巴特·塞尔曼。 “典型案例复杂性的后门。”国际人工智能会议。卷。 18，2003。

2] Dilkina，Bistra，Carla Gomes和Ashish Sabharwal。 “在后门检测的复杂性方面的权衡。”约束编程的原则和实践（CP 2007），第256-270页，2007年。

3]Ansótegui，Carlos，Maria Luisa Bonet，Jordi Levy和Felip Manya。 “测量SAT实例的硬度。”在第23届全国人工智能会议论文集（AAAI'08），第222-228页，2008年。

Answer 2

由于您知道相位过渡，因此请允许我提及我知道的其他一些简单检查（可能由约束图分析所包含）：

• 一些早期的随机SAT发电机无意间创建了大部分简单的公式，因为它们使用了“恒定密度”，这意味着所有子句长度的比例大致相等。这些通常很容易，因为正如人们应该期望的那样，2-clauses和单位可以显着简化问题，而很长的条款也不会增加太多的分支或促进超分辨率更好。因此，最好坚持使用固定长度和其他参数。
• 同样，强大的简化规则是纯粹的文字消除。显然，一个公式实际上只有不纯正的文字数量。因为分辨率创建了新的子句编号 $ | x |*| lnot x | $ （意思是，发生的产物 $ x $ 及其否定），当每个变量有相等数量的正和负文字数量时，分解数量将最大化。因此，平衡的SAT发电机。
• 还有一种称为“无三角形SAT”的技术，它似乎很新鲜[1]，这是一种禁止“三角形”的硬性生成器。三角形是包含3个变量的一组子句 $ v_1，v_2，v_3 $ 这些在某些子句中的所有组合中成对发生（即 $ {v_1，v_2，... }， {v_2，v_3，... }， {v_1，v_3，... } $）。显然，三角形倾向于使已知求解器的公式更容易。

[1] https://arxiv.org/pdf/1903.03592.pdf

Answer 3

除了Juho的出色答案之外，这是另一种方法：

Ercsey-Ravasz＆Toroczkai， 在模拟方法中，优化硬度作为瞬态混乱，以限制满意度, ，《自然物理》第7卷，第966-970页（2011年）。

这种方法是将SAT问题重写为动态系统 吸引子 系统的解决方案是解决SAT问题的解决方案。由于问题变得更加困难，系统吸引力的盆地更加分形，因此可以通过检查系统收敛之前的瞬变如何混乱来测量SAT实例的“难度”。

实际上，这意味着从不同初始位置启动一堆求解器，并检查求解器在到达吸引子之前逃脱混乱的瞬变的速率。

提出一个动态系统并不难，“解决方案”是给定SAT问题的解决方案，但是要确保解决方案都是吸引者而不是驱虫者，这要有点困难。他们的解决方案是引入能量变量（类似于Lagrange乘数）来表示违反约束的严重程度，并试图使系统最小化系统的能量。

有趣的是，使用其动力学系统，您可以在模拟计算机上解决多项式时间的SAT问题，这本身就是一个了不起的结果。有一个渔获；它可能需要指数级的大电压来表示能量变量，因此不幸的是，您无法在物理硬件上意识到这一点。