Incorrect DIMACS header for trojan benchmarks

[tanyongkiam]

The trojan benchmark CNFs list too many clauses in their DIMACS headers which would cause some solvers to reject them immediately.

This bug is visible in the CCS paper benchmarks which I downloaded from here: https://drive.google.com/open?id=1yhAX8_pm7jVo0tgx4LGsDs8xoMt_qKix

It looks like total_clauses calculated here: https://github.com/teobaluta/NPAQ/blob/master/mlp2cnf/src/bnn_prop.cpp#L722 should be changed to only count the clauses from the BNNs which are selected by 'which_bnn'.

[teobaluta]

Hi,

I think the solver we used did not have this issue - but thanks for reporting this!

[tanyongkiam]

Sure, just for the record, I used CaDiCaL, which e.g., reports:

cadical: error: card-trojan_mnist_...: parse error: clause missing

One can get around this using the -f option