Open MaxOstrowski opened 3 years ago
Isn't this the same as simply translating the original linear constraint into clauses instead of using a PB constraint ?
This depends on the translation we implement. For example, clingcon's constraint to clause translation does not introduce auxiliary variables. Some PB-translations introduce auxiliary variables to achieve more compact representations. Introducing auxiliary variables is actually also something interesting that could be considered when translating constraints to clauses.
Automagically translate some of the pb constraints into clauses, with a similar heuristic as clasp does. Isn't this the same as simply translating the original linear constraint into clauses instead of using a PB constraint ?