fearviking
New member
- Joined
- May 12, 2021
- Messages
- 2
Hello there!
I want to check whether a formula is satisfiable or not using resolution and variable elimination.
The formula is http://prntscr.com/13h831v
So I negate the conclusion and move it to the premises. Then I can remove all clauses containing x7, since x7 is a pure literal (using pure literal elimination.)
Now there are these clauses left: (x1|x2|x6), (!x1|x3|x8), (!x2|!x3!x4), (!x4|x6|x8), (x5|!x6).
Here I can remove clauses with x5 since it's pure, and then from there I can remove all clauses with x6 since it is now pure.
Here's where I get confused. Now since there are only 2 clauses left (!x1|x3|x8), (!x2|!x3|x4), I could remove both of them since they both contain pure literals. What does this mean?
If I can prove ⊥ after moving conclusion to the premises, that should mean that the original formula is satisfiable. Does this then mean that the original formula is NOT satisfiable? I can't really use Resolution here since all clauses contain a pure literal? I'm not really sure how to think about this. Would greatly appreciate any help!
I want to check whether a formula is satisfiable or not using resolution and variable elimination.
The formula is http://prntscr.com/13h831v
So I negate the conclusion and move it to the premises. Then I can remove all clauses containing x7, since x7 is a pure literal (using pure literal elimination.)
Now there are these clauses left: (x1|x2|x6), (!x1|x3|x8), (!x2|!x3!x4), (!x4|x6|x8), (x5|!x6).
Here I can remove clauses with x5 since it's pure, and then from there I can remove all clauses with x6 since it is now pure.
Here's where I get confused. Now since there are only 2 clauses left (!x1|x3|x8), (!x2|!x3|x4), I could remove both of them since they both contain pure literals. What does this mean?
If I can prove ⊥ after moving conclusion to the premises, that should mean that the original formula is satisfiable. Does this then mean that the original formula is NOT satisfiable? I can't really use Resolution here since all clauses contain a pure literal? I'm not really sure how to think about this. Would greatly appreciate any help!