Решение формы 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).

Answer 2

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