LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Last revision Both sides next revision
sav08:homework04 [2008/03/13 11:11]
vkuncak
sav08:homework04 [2008/03/13 11:12]
vkuncak
Line 13: Line 13:
 If a given formula is unsatisfiable,​ for now the SAT solver can simply say "​false"​. If a given formula is unsatisfiable,​ for now the SAT solver can simply say "​false"​.
  
-The expected level of sophistication is the simple DPLL solver with unit propagation described in [[DPLL Algorithm for SAT]], it is not required that you implement+The expected level of sophistication is the simple DPLL solver with unit propagation described in [[DPLL Algorithm for SAT]], it is not required that you implement ​advanced techniques or very efficient data structures.
  
 You will extend your solver in [[homework05]]. You will extend your solver in [[homework05]].