boolean satisfiability

[Tuakro]

hi, i am currently working on a program that solves boolean satisfiability (i call it BoolSAT) with recursion in C. The program is suppose to take in input as command line arguments with the first argument being number of variables and second being number of clauses.

For example in cmd start BoolSAT 4 3 would mean 4 variables and 3 clauses.

Then the user proceeds to enter in the variables for each clause i.e.
1 2 4
4 3 1
3 1 2

this would translate to (x1||x2||x4)&&(x4||x3||x1)&&(x3||x1||x2) as you can see the formula is variables are separated by "or" and each clause is separated by "and" also a negative number translate to !xn in the equation

For example 1 -2 4 would be x1||!x2||x4

the program is then suppose to find and print all possible combinations of the assigned variables that would make the equation true.

Currently i have a code that takes in the command line arguments, dynamically creates a 2d array with malloc to hold the variables and clauses, scans in the variables and puts them in the 2d array, and a dynamically allocated 1 1d array to hold the possible solutions.

I am thinking of using binary addition in order to obtain the all possibilities of Ts and Fs (i.e. with 3 variables there would be 2^3 possibilities starting from 0 0 0 to 1 1 1 [15] ) and then testing with recursion. However, i cant seem to grasp how to simultaneously create a solution and check if its true with recursion. Also i don't know how to handle the case where there is a negative in front of the number which turns the variable to !.

I would really appreciate it if someone can explain to me how recursion would be able to achieve this.

[Tony]

Tuakro @ Thu Nov 17, 2011 10:40 pm wrote:

However, i cant seem to grasp how to simultaneously create a solution and check if its true with recursion.

why simultaneously? Those are two distinct parts.

part 1 -- generate all permutations of variable assignments
part 2 -- check if a particular assignment evaluates to true

For the check you simply plug in the assignments into the equation that you have. Not sure why you would even want recursion there.