The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
Bug when mixing constraint removal and constraints satisfied by unit propagation
Hi Daniel,
I am triggering buggy behavior in the OPB solver by mixing constraint removal with constraints that get satisfied by unit propagation. In particular, the bug is triggered by the following sequence of operations:
- add constraints (x1 + x2 + x3 <= 2), (x1 + x2 >= 2) and (not(x2) v not(x3))
- check satisfiability: formula is SAT, as expected
- remove (x1 + x2 >= 2)
- add (x2 + x3 >= 2): this should contradict (not(x2) v not(x3)), but no exception is thrown
- check satisfiability: formula should be UNSAT, but SAT is returned instead
I have attached a small Java program that follows this sequence of operations, triggering the bug.
Best regards,
Miguel Neves