java - 使用蛮力求解 2Sat CNF 形式

Question

我目前正在为考试研究 2SAT 问题，但我不太了解如何使用蛮力检查解决方案是否存在。我知道这看起来有点奇怪，但我了解如何更好地实现蕴涵图，但我不太确定如何实现蛮力策略。

谁能分享一些见解？也许在伪代码或 java 中。

谢谢

Answer 1

公式中的变量可以编码为整数值中的位。然后，蛮力法归结为积分“容器”可能采用的所有可能值的范围。

换句话说，您有一个整数数组，它代表您公式的所有变量，您用进位递增整数，并在每一步检查它代表您的公式的解决方案。当解决方案匹配时，您就停止了。

下面是这种可变容器的简单实现:

class OverflowException extends RuntimeException {}

public class Variables {
    int[] data;
    int size;

    public Variables(int size_){
        size = size_;
        data = new int[1 + size/32];
    }
    public boolean get(int i){
         return (data[i/32] & (1 << i%32)) != 0;
    }
    public void set(int i, boolean v){
        if (v)
            data[i/32] |= (1 << i%32);
        else
            data[i/32] &= ~(1 << i%32);
    }
    public void increment(){
         int i;
         for (i=0; i < size/32; i++){
             data[i]++;
             if (data[i] != 0) return;
         }
         if (size%32 != 0){
             data[i]++;
             if ((data[i] & ~((1 << (size%32)) - 1)) != 0)
                 throw new OverflowException();
        }
    }
}

(注意买者:代码未经测试)。

变量数组也可以更简单地表示为 boolean 容器，但由于增量步骤，您可能会损失一点性能(尽管这可能可以通过使用 gray code 来缓解)而不是用于增量操作的普通二进制编码，但是这个 implementation 的复杂性似乎表明相反的情况，如果您寻求复杂的解决方案，它也可能是一个很好的 sat2 求解器。