Unsoundness for large formulas with integer variables in the C++ interface.

Question

Unsoundness for large formulas with integer variables in the C++ interface.

Closed this issue 3 years ago · 11 comments

In some cases when using the C++ interface, dReal will return unsat for formulas over integer variables which are actually satisfiable. For example, running this code as written yields unsat. However if I copy this formula to an SMT2 file and use the dReal executable, dReal successfully finds a satisfying assignment. Uncommenting the first line of the formula in that gist forces dReal to use the correct assignment, and in that case the C++ code does indeed return sat.

I have only seen this happen with relatively large formulas like the attached one, on smaller formulas there doesn't seem to be any issue.

This behavior was tested with dReal version 4.21.06.1, installed with the .deb package on Mint 19.3 (based on Ubuntu 18.04). I had also seen this when using dReal version 4.20.07.1.

Answer 1 · 2021-06-15T18:00:35.000Z

Thanks for the report, @gavlegoat . I'll investigate this and get back to you.

Answer 2 · 2021-06-15T21:54:40.000Z

I have been digging into this some more and I think I was wrong and this is not a C++ issue. Instead there seems to be some sensitivity to the representation of the formula. Specifically, if you look at this gist, there are two different versions of the same formula (this is also the same formula from the initial post). The only difference between these two is that in minus.smt2 there are several expressions of the form (> (+ (- (+ t1 (* c1 t2)) (* c2 t3)) (* c3 t4)) 0) where c1, c2, and c3 are constants and t1 through t4 are variables. In plus.smt2 those expressions are replaced by (> (+ (+ t1 (* c1 t2)) (* -c2 t3) (* c3 t4)) 0). These should be equivalent but plus.smt2 returns unsat while minus.smt2 returns sat.

In order to try to rule out delta-completeness issues I also tried running these with varying precision. plus.smt2 is unsat even for very large delta (as high as 1) and minus.smt2 is sat even for delta as small as 1e-9.

Answer 3 · 2021-06-16T14:47:56.000Z

@gavlegoat , could you test it using the current HEAD (b1d1341)? When I check the two SMT2 files (plus and minus), both of the return sat (precision = 0.001).

Answer 4 · 2021-06-16T14:49:04.000Z

FWIW, I fixed a bug about two weeks ago, but have not released a new version yet. I'll prepare binaries today.

08d2d6c fix(contractor/contractor_integer): Fix a bug Soonho Kong, 12 days ago

Answer 5 · 2021-06-16T15:31:51.000Z

I'm getting the same result running in HEAD (plus is unsat and minus is sat). I also tried rerunning install_prereqs to make sure I have the most recent versions of all dependencies, but that didn't fix the problem either. What OS are you using? Maybe there is an issue in the Ubuntu 18.04 dependencies.

Answer 6 · 2021-06-16T15:38:46.000Z

Thanks for the check. I was using macOS. I'll test it on an Ubuntu machine.

Answer 7 · 2021-06-16T16:56:55.000Z

I can reproduce it on my Ubuntu box. I'll let you know when I find my information about this bug.

Answer 8 · 2021-06-17T18:32:53.000Z

In case it is helpful, a colleague was able to reproduce this issue using MacOS 10.15.7, using the version of dReal from HEAD.

Answer 9 · 2021-06-17T18:41:43.000Z

@gavlegoat , thanks for the check. I was also able to reproduce it on my mac (maybe there was a glitch last time I tried). I'm still debugging the code but will get back to you when I have more info.

Answer 10 · 2021-06-19T03:14:54.000Z

@gavlegoat , I just added commits to the master branch. Can you check if they fix your issues?

Answer 11 · 2021-06-19T17:21:50.000Z

The issue seems to be resolved, thank you.