We know DPLL algorithm is backtracking + unit propagation + pure literal rule.
I have an example. There is one example to solve following Satisfiability problem with DPLL. if assign of "0" to variables is prior to assign "1" to variables, Which of Unit Clause (UC) or Pure Literal (PL) is used to solve this specific example?
{~A \/ B \/ C}, {A \/ ~B \/ C}, {A \/ B \/ ~C}, {A \/ B \/ C}
Olympiad Solution is: PL and UC.
Our Solution is just UC.
any professors can judgment and say the correct solution to send it for main department for correctness? it has 50 points for this contest and it's critical for us. thanks.
- Badges
- Science topic
- Similar topics
- Computer Science and Engineering
- Artificial Intelligence
More Huimen Maisori's questions See All
Similar questions and discussions