Rozhodovací procedury a verifikace – NAIL094

Úkol č.3 – Watched literals

Rozšiřte řešič z úkolu 2 o datovou strukturu Watched literals. Když je některý z literálů falsifikovaný, klauzule, ve kterých se vyskytuje, se můžou stát jednotkovými. Při základním algoritmu se musím podívat na všechny takové klauzule, při použití sledovaných literálů jenom na ty, ve kterých je daný literál sledovaný. Naměřte, kolik zkoumání se tímto způsobem ušetří na napište o tom krátkou zprávu.

Opět použijte benchmarky z této stránky.

Deadline: 20.5.2018 23:59

Hodnocení: Za úkol můžete získat až 5 bodů. Hodnotí se funkčnost kódu a taky správa s naměřenými statistikami.