Shortest Reconfiguration Paths in the Solution Space of Boolean Formulas
Shortest Reconfiguration Paths in the Solution Space of Boolean Formulas
复制标题
布尔公式解空间中的最短重构路径
DOI：
10.1137/16m1065288
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Venkatesh Raman
中科院分区：
文献类型：
--
作者：
A. E. Mouawad;N. Nishimura;Vinayak Pathak;Venkatesh Raman
给出一个布尔公式和一个令人满意的赋值，翻转是一种操作，它改变赋值中变量的值，以使结果赋值保持令人满意。我们研究了计算最短翻转序列(如果存在)的问题，它将一个给定的满意分配\(S\)转换为布尔公式的另一个满意分配\(t\)。早期的工作描述了使用Schaefer的布尔公式分类框架来确定两个给定的令人满意的赋值之间是否存在翻转序列的复杂性。我们在此基础上给出了求最短翻转序列的复杂性的三分法，并证明了它要么是P的，要么是NP-完全的，要么是PSPACE-完全的。我们的结果增加了已知的最短重构序列问题的一小部分复杂性结果，提供了一个例子，即使路径反转在\(S\)和\(t\)中具有相同值的变量，也可以在多项式时间内找到最短序列。这与迄今研究的所有重新配置问题形成对比，在这些问题中，计算最短路径的多项式时间算法仅在路径修改对称差的情况下才为人所知。我们的证明使用Birkhoff的表示定理在我们证明为分配格的集合系统上。这项技术很有见地，或许也可以用于解决其他重新配置问题。
Given a Boolean formula and a satisfying assignment, a flip is an operation that changes the value of a variable in the assignment so that the resulting assignment remains satisfying. We study the problem of computing the shortest sequence of flips (if one exists) that transforms a given satisfying assignment \(s\) to another satisfying assignment \(t\) of the Boolean formula. Earlier work characterized the complexity of deciding the existence of a sequence of flips between two given satisfying assignments using Schaefer’s framework for classification of Boolean formulas. We build on it to provide a trichotomy for the complexity of finding the shortest sequence of flips and show that it is either in P, NP-complete, or PSPACE-complete. Our result adds to the small set of complexity results known for shortest reconfiguration sequence problems by providing an example where the shortest sequence can be found in polynomial time even though the path flips variables that have the same value in both \(s\) and \(t\). This is in contrast to all reconfiguration problems studied so far, where polynomial time algorithms for computing the shortest path were known only for cases where the path modified the symmetric difference only. Our proof uses Birkhoff’s representation theorem on a set system that we show to be a distributive lattice. The technique is insightful and can perhaps be used for other reconfiguration problems as well.