Weightconstraints created with create_only_btb or create_only_bfb do not behave as expected.

[rkaminsk]

We have a project where we need weight constraints to propagate only in one direction. Weight constraints created with create_only_btb or create_only_bfb do not behave as expected. When constraints are created with create_explicit the constraint behaves as expected if only one thread is used.

With explicit disabled the result is as if bfb or btb are not given

• add_weight_constraint(a, [(b, 1), (c, 1)], 1, bfb)
  • model
  • model a c
  • model a b
  • model a b c
• add_weight_constraint(a, [(b, 1), (c, 1)], 1, btb)
  • model
  • model a c
  • model a b
  • model a b c

With explicit enabled the result is as expected

• add_weight_constraint(a, [(b, 1), (c, 1)], 1, explicit+bfb)
  • model
  • model a
  • model a c
  • model a b
  • model a b c
• add_weight_constraint(a, [(b, 1), (c, 1)], 1, explicit+btb)
  • model
  • model c
  • model b
  • model b c
  • model a b
  • model a c
  • model a b c

With threads and explicit enabled it fails completely

• add_weight_constraint(a, [(b, 1), (c, 1)], 1, explicit+bfb)
  • random results
• add_weight_constraint(a, [(b, 1), (c, 1)], 1, explicit+btb)
  • random results

Current workaround

To achieve btb, I currently add an auxiliary literal (bfb can be achieved by inverting l in the weight constraint):

l = add_literal()
add_clause([-a,l])
add_weight_constraint(l, [(b, 1), (c, 1)], 1, 0)

Of course this adds an unnecessary literal...

[BenKaufmann]

@rkaminsk
I addressed two obvious problems in dev. Could you please check whether things now work for you as expected?

[rkaminsk]

Yes, this seems to work. In your commit you wrote that you cannot transform to clauses if only one propagation direction is requested. Wouldn't it be enough to only add "half" of the clauses?

[BenKaufmann]

I'm sure you are right and the commit is probably a little lazy. However, I'm not fully convinced that it's actually worth to complicate the code even further.