search

NTU-ALComLab / ssatABC

Stochastic SAT solver within ABC
Other
5 stars 2 forks source link

Possible underflow #15

Closed vuphan314 closed 3 years ago

vuphan314 commented 3 years ago

@nianzelee Could you check if erSSAT experiences underflow for this benchmark?

ABC command line: "ssat benchmarks/sdimacs/rand-3-30-150-15.57.sdimacs".

[INFO] Input sdimacs file: benchmarks/sdimacs/rand-3-30-150-15.57.sdimacs
[INFO] Starting analysis ...
[INFO] Stopping analysis ...

==== Solving results ====

  > Satisfying probability: 1.000000e+00
  > Time =     0.00 sec

My (currently unpublished) solver returns 2.04728e-05.

Thank you.

nianzelee commented 3 years ago

Hi, thank you for reporting the issue!

I could confirm your answer with the DC-SSAT solver:

$ bin/dcssat test/test-cases/benchmarks/er-random-k-CNF/rand-3-30-150-15.57.sdimacs 
    x16   -x17    x18    x19    x20    x21    x22   -x23   -x24    x25    x26   -x27   -x28   -x29   -x30     x1     x2     x3     x4    -x5     x6     x8    -x9    x10   -x11   -x13    x14    x15

solve time:              = 0.00270891
rebuild/print time:      = 8.2016e-05
   total time:           = 0.00279093

Pr[SAT]                  = 2.04728e-05

This issue is most likely related to #3. If the heuristic of minimal clause selection (the -g option below) is turned off, erSSAT computes a close answer. (Observe that the optimal assignment to the existential variables is the same. The difference in the satisfying probability is due to floating-point precision.)

abc 01> ssat -gv test/test-cases/benchmarks/er-random-k-CNF/rand-3-30-150-15.57.sdimacs 
[INFO] Input sdimacs file: test/test-cases/benchmarks/er-random-k-CNF/rand-3-30-150-15.57.sdimacs
[INFO] Invoking erSSAT solver with the following configuration:
  > Counting engine: BDD
  > Minimal clause selection (greedy): no
  > Clause subsumption (subsume): yes
  > Partial assignment pruning (partial): yes
[INFO] Starting analysis ...
  > Found a better solution , value = 0.000021
    16 -17 18 19 20 21 22 -23 -24 25 26 -27 -28 -29 -30 0
  > Time consumed =     0.00 sec
[INFO] Stopping analysis ...
  > Found an optimizing assignment to exist vars:
    16 -17 18 19 20 21 22 -23 -24 25 26 -27 -28 -29 -30 0

==== Solving results ====

  > Satisfying probability: 2.050400e-05
  > Time =     0.00 sec
nianzelee commented 3 years ago

@vuphan314: Could you please let me know if it is fine to close this issue? I have mentioned this test case er-random-k-CNF/rand-3-30-150-15.57.sdimacs in #3.

vuphan314 commented 3 years ago

Thank you. I will use ssat -g for correctness until the bug is fixed. I am closing this issue.