Soonho Kong
Soonho Kong
Thanks for the report. This bug is due to the use of IEEE-754 `double` to represent integer values and constant folding using `double`. I'll resolve the issue and ping you...
@BetsyMcPhail, I'll ping you when `[email protected]` formula is ready.
@KJongUk , can you create a small reproducible example only using IBEX? Then I'd open an issue there.
There is a known issue that can cause inefficiency when there are a lot of variables (>200). I will push a fix soon. What other solvers have you tested?
@Krayn , I have a version of dReal which can solve both instances (with and without `_ub`) in 20sec (on Intel(R) Xeon(R) CPU E5-2686 v4 @ 2.30GHz). Can you send...
Thanks for sharing the benchmark. I think I can run them over this weekend.
@Krayn , can you rewrite `y = sigmoid(\sum_i c_i x_i)` into `z = \sum_i c_i x_i` and `y = sigmoid(z)` by introducing an intermediate variable `z`?
@Krayn , ``` smt2/mnist_6_1000_0_fb2.smt2 delta-sat 48.241 sec dreal smt2/mnist_6_1500_0_b1.smt2 unsat 175.84 sec ``` CPU: Intel(R) Xeon(R) CPU E5-2686 v4 @ 2.30GHz Can you send an email to Prof. Sicun Gao?
Hi, We're aware of this issue and working on a workaround. FYI, the problems come from some dependencies of dReal. In the meantime, you need to use either intel macs...
Hi, 1) delta-sat doesn't not exclude the case where the original formula is unsatisfiable. It merely indicates that the delta-perturbation of the original formula is satisfiable. 2) If you provide...