LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:homework04 [2008/03/13 11:11]
vkuncak
sav08:homework04 [2008/03/13 11:47]
vkuncak
Line 1: Line 1:
-====== Homework 04 -DRAFT ======+====== Homework 04 - due 19 March 2008 at 11:00 ======
  
 ===== Problem 1 ===== ===== Problem 1 =====
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]].