Решение 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 контейнера, но вы можете немного потерять в производительности из-за шага приращения (хотя, возможно, это можно было бы уменьшить, используя серый код вместо простого двоичного кодирования для операции приращения, но сложность этой реализации, кажется, указывает на обратное, и если вы выберете комплексное решение, оно может быть хорошим решением для sat2).

Answer 2

По этой причине мы не используем решения грубой силы:), они потребляют много ресурсов. Моим алгоритмом было бы не создавать матрицу со всеми возможностями. Но чтобы создать одно задание, а затем проверить его немедленно. Затем создайте следующий. Вы можете остановить, когда вы нашли первое решение.