Decision Heuristics [5 points]

Add a nontrivial decision heuristic to your solver. Implement at least two nontrivial heruistics and compare them with each other and with a random choice of branching literal.

For comparison, use again some of the SATLIB Benchmark Problems. Write a report with the results

Assumptions

Implement possibility to pass an assumption with a CNF to your solver. The assumption is a list of literals. There are two possibilities how to incorporate the assumptions into the search.

1. Just add the literals as unit clauses and run the search
2. Use the literals from the list for decisions before any heuristic is used

Implement the second approach which better for incremental use of the SAT solver, because the learned clauses can be kept for the next run of the solver with different assumptions.