NAIL094Decision procedures and verification

Petr Kučera, KTIML MFF UK

Watched Literals

Add watched literals data structure to your DPLL solver with lazy watched literals data structure. If you had not done yet, use adjacency lists as an alternative and check on the benchmark examples how much does watched literals save on the number of checked clauses and running time. Write a short report on that.

Use some non-random benchmarks (e.g. easier PHOLE or All Interval Series) examples from SATLIB Benchmark Problems, random instances are not good for comparison with adjacency lists, because they do not have long clauses.