Choosing variables for DPLL

Question

I have doubt regarding solving problems using DPLL. I did understand how Unit clause propagation works. However for case splitting, I did not understand whether the variables are chosen on a random basis or with some specific reason. 

For eg: In the below solution, you can see that in the second step x0=false. In this step, instead of choosing x0, can we choose variable X1 =true/false?

I just want to know whether the choosing of variables for case splitting is done on a random basis or whether with some reason.

 

Answer 1

If just correctness is your concern, you can choose any variable for case splitting. In practice, it would be good to select one that will give simpler clauses, and typically variables are to be preferred that have most occurrences or will generate many unit clauses. However, as said, for correctness, random choices are also fine. It is a matter of efficiency.

Comments

Thank you very much for the clarification.