Hi everyone I have this project for my programming class and would appreciate it if someone could point me in the right direction. The objective of the lab is to write a C program that will be able to solve a boolean formula and print all the satisfying assignments. This is also known as boolean satisfiability. So basically if we are given the boolean formula
f = (x1 OR 'x2 OR x3) AND ('x1 OR x2 OR x3)
this means we need to find all the assignments for the variables that make this formula true. When there is a ' before the variable that means it is in the complemented form, so a False assignment would make it evaluate to true.
So for the above formula these would be the satisfying assignnments:
x1x2x3
-----
F F F
F F T
F T T
T F T
T T F
T T T
So there are 2^n possiblities that need to be evaluated where n is the number of variables. Each clause (what's inside the brackets) will have exactly 3 variables and they will be provided by input from the user. The number of clauses and variables will be provided when the program is run. So for example, the user might run the program and say there 4 variables and 5 clauses, then they would input the following formula:
1 -2 3
3 -4 2
3 1 2
4 -2 1
3 -1 2
where each number represents a variable and if it's negative then it's in complemented form.
The formula for the first sample would be:
1 -2 3
-1 2 3
--
Each clause will have exactly three literals (variables) and no repeated variables. Also, the satisfying assignments need to be printed in an order where they first start with one where x1 is false are printed before x1 being true, and for those where x1 is false, all those with x2 being false are printed first and so on.
We must use recursion to create this program.
----
Okay, so first of all I'm not looking for anyone to give me any code, I'm just looking for some help and pointers in the right direction. Here's what I've done so far:
I've coded a way for the user to input the formula variables which are stored into a c X 3 matrix where c is the number of clauses, so if there input would be stored like this:
3 2 1
-2 3 1
just like a regular table.
Now I've thought about this problem can be satisfied recursively and here's what I came up with:
[IMG]http://i.imgur.com/H9gFE.jpg[/IMG]
So I suppose the algorithm should have two parts, one where it keeps checking the right side (= 0) first then going left. This will satisfy the requirement of printing all the assignments in the correct order. But here is where I'm stuck, first of all:
1. What would be the condition for the function to stop recursing or repeating
2. Let's say it keeps recursing and somehow I'm at x1 is FALSE, x2 is FALSE, x3 is FALSE, and x4 is FALSE, how do I substitute those assignments into all the clauses I have in my formula and make sure it satisfies them all? I mean nothing is arranged in any certain order so I am really lost here on how I would replace them and then make sure they all evaluate to true when assigning everything to false.
3. I realize that having more variables doesn't matter since the function would be the same if you had just one variable which would give you two branches or 30 variables. Because each branch just repeats, so if I just have x1, then first it will check if setting x1 to false evaluates to true, if not it will set it to true and see if that satisfies it. So even if there are many branches/variables it's just the same thing happening over and over again.
I spent an entire day trying to come up with a solution and reading tons of articles on satisfiability algorithms and the DLPP algorithm but this is a first year course so thesis papers on the subject didn't help me very much.
Any help you can give me is appericiated..and wow that is one long post. :0