learnt literals not displayed in prime implicants using org.sat4j.core.jar command line (launcher)
Sat4j does not report learnt literals as part of the computed prime implicant.
Here is an example provided by a user:
p cnf 5 6
-1 -2 3 0
-1 2 3 0
1 -2 3 0
1 2 3 0
-4 5 0
4 5 0
This gives
s SATISFIABLE
c returning a prime implicant ...
c prime implicant computation statistics BRESIL (reverse = false)
c implied: 0, decision: 5, removed 4 (+0), propagated 1, time(ms):0
c removed 4 literals
c pi computation time: 4 ms
v 3 0
But literal 5 should also be in the prime.
The issue is that Sat4j inherits from Minisat 1 it's management of unit clauses, which are not real constraints: they only live on the trail, not on the list of constraints.
We need to make sure that:
- either we use a specific data structure representing UnitClause in the solver
- or we simply add learnt literals to the prime implicant