Backbones

We say that a literal \(l\) is a bacbone of \(\varphi\) if \(l\) is in every model of \(\varphi\), or in other words the value of \(l\) is implied by \(\varphi\), i.e. \(\varphi\models l\). Write a program which uses a SAT solver as an oracle and finds all backbones of a given CNF \(\varphi\). The CNF is given in DIMACS format (also described in the first task.

• Use a strategy or heuristic to minimize the number of SAT calls
• If a formula is satisfiable, the SAT solver can return a model, use he information given by the model to minimize the number of SAT calls

Evaluate your program on several SATLIB Benchmark Problems and write a report on the results.