As discussed with Nils Christian Froleyks, it's be nice if CaDiBack output the equivalent literals it has found. This can (and should) be best-effort basis. The system has already found a bunch of binary clauses due to all the things that it runs (CDCL but also inprocessing). There's no reason why not to run SCC on them, and output a best-effort set of equivalent literals of them. It's a linear algorithm [1] so super-duper cheap to run.
As discussed with Nils Christian Froleyks, it's be nice if CaDiBack output the equivalent literals it has found. This can (and should) be best-effort basis. The system has already found a bunch of binary clauses due to all the things that it runs (CDCL but also inprocessing). There's no reason why not to run SCC on them, and output a best-effort set of equivalent literals of them. It's a linear algorithm [1] so super-duper cheap to run.
Would be really nice if this was possible,
Mate
[1] https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm