Solving 2Sat CNF form using brute force

Question

I'm currently studying the 2SAT problem for an exam and I don't really understand how to check if a solution exists using the brute force. I know this seems a bit strange but I understand how to implement the implication graph a bit better but I'm not too sure how to implement a brute force strategy.

Could anyone share some insight? Maybe in pseudo code or java.

Thanks

Answer 1

The variables in a formula can be encoded as bits in an integral value. The brute force method then boils down to range over all possible values that the integral "container" may take.

In other words, you have an array of integers, which represents all your formula's variables, and you increment the integers with carry, and at each step check the solution it represents against your formula. You stop when the solution is a match.

Here's a dead simple implementation for such a variable container:

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();
        }
    }
}

(Caveat emptor: code untested).

The variable array can also be more simply represented as a boolean container, but you might lose a bit in performance, because of the increment step (although that could be perhaps mitigated by using gray code instead of plain binary encoding for the increment operation, but the complexity of this implementation seems to indicate the contrary, and if you go for a complex solution, it might as well be a good sat2 solver instead).

Answer 2

This is the reason we don't use brute force solutions :) , they consume to much resources. My algorithm would be not to create a matrix with all possibilities. But to create one assignment and then test it immediately. Then create the next one. You can halt when you found the first solution.