You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 

2 lines
200 B

\item In the context of DPLL, give the definition of the \textit{resolution rule} used to perform a resolution proof.
How can we use a resolution proof to show that an input formula is unsatisfiable?