Making a CNF Prime and Irredundant

Primality and Irredundancy

Assume a CNF \(\varphi\) and a clause \(C\).

• We say that \(C\) is an implicate of \(\varphi\) if \(\varphi\models C\).
• We say that \(C\) is a prime implicate if there is no implicate \(C'\subsetneq C\)
  • \(C\) is a minimal implicate with respect to the inclusion,
  • we can also say that if any literal is removed from \(C\), then \(C\) ceases to be an implicate
• We say that CNF \(\varphi\) is prime if it consists only of prime implicates
  • no clause in \(\varphi\) can be shortened without changing the function
• We say that \(\varphi\) is irredundant if dropping any clause from \(C\) changes the function represented by \(\varphi\). In other words for every clause \(C\in\varphi\) we have that \(\varphi\) is not equivalent to \(\varphi\setminus\{C\}\).

Note that if \(C\) is an implicate of \(\varphi\) which is not prime, we can replace it with a prime subimplicate \(C'\) without changing the function represented by \(\varphi\). This way, we can turn \(\varphi\) into a prime CNF.

The Task

Write a program which given a CNF outputs an equivalent CNF which is prime and irredundant (make any of these optional).

Input and output

Both input and output are expected in DIMACS format which was also described in the first task.

Experimental evaluation

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