Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


538 users

0 votes

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?

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


in * TF "Emb. Sys. and Rob." by (1k points)

1 Answer

+2 votes
Best answer
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.
by (166k points)
selected by
Thank you very much for the clarification.

Related questions

Imprint | Privacy Policy