search

NTU-ALComLab / ssatABC

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

Wrong solution for ER test case `rand-3-40-160-20.71.sdimacs` #16

Open vuphan314 opened 3 years ago

vuphan314 commented 3 years ago

@nianzelee

For a random 3CNF ER-SSAT benchmark, my solver and DC-SSAT agree on the same satisfying probability:

$ bin/dcssat test/test-cases/ssatER/random/3CNF/sdimacs/rand-3-40-160-20.71.sdimacs
    x21    x22    x23   -x24    x25   -x26   -x27   -x28   -x29   -x30   -x31   -x32   -x33   -x34    x35    x36   -x37   -x38   -x39    x40    -x1    -x2    -x3    -x4    -x5    -x6    -x7    -x8    -x9   -x10    x11    x12    x13   -x14   -x15   -x16   -x18    x19   -x20

solve time:              = 0.00199795
rebuild/print time:      = 3.91006e-05
   total time:           = 0.00203705

Pr[SAT]                  = 1.83196e-05

However, greedy erSSAT gives a different probability:

$ bin/abc -c "ssat -v test/test-cases/ssatER/random/3CNF/sdimacs/rand-3-40-160-20.71.sdimacs"
ABC command line: "ssat -v test/test-cases/ssatER/random/3CNF/sdimacs/rand-3-40-160-20.71.sdimacs".

[INFO] Input sdimacs file: test/test-cases/ssatER/random/3CNF/sdimacs/rand-3-40-160-20.71.sdimacs
[INFO] Invoking erSSAT solver with the following configuration:
  > Counting engine: BDD
  > Minimal clause selection (greedy): yes
  > Clause subsumption (subsume): yes
  > Partial assignment pruning (partial): yes
[INFO] Starting analysis ...
  > Found a better solution , value = 0.007439
    21 22 -23 -24 25 -26 -27 -28 -29 -30 31 32 -33 -34 35 36 -37 38 -39 -40 0
  > Time consumed =     0.00 sec
  > Found a better solution , value = 0.058286
    21 22 23 -24 25 -26 -27 -28 -29 -30 -31 -32 -33 -34 35 36 -37 -38 -39 40 0
  > Time consumed =     0.00 sec
[INFO] Stopping analysis ...
  > Found an optimizing assignment to exist vars:
    21 22 23 -24 25 -26 -27 -28 -29 -30 -31 -32 -33 -34 35 36 -37 -38 -39 40 0

==== Solving results ====

  > Satisfying probability: 5.828595e-02
  > Time =     0.01 sec

And non-greedy erSSAT gives yet another probability:

$ bin/abc -c "ssat -gv test/test-cases/ssatER/random/3CNF/sdimacs/rand-3-40-160-20.71.sdimacs"
ABC command line: "ssat -gv test/test-cases/ssatER/random/3CNF/sdimacs/rand-3-40-160-20.71.sdimacs".

[INFO] Input sdimacs file: test/test-cases/ssatER/random/3CNF/sdimacs/rand-3-40-160-20.71.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.000004
    21 22 -23 -24 25 -26 -27 -28 -29 -30 31 32 -33 -34 35 36 -37 38 -39 -40 0
  > Time consumed =     0.00 sec
  > Found a better solution , value = 0.012666
    21 22 -23 -24 25 -26 -27 -28 -29 -30 31 32 -33 -34 35 36 -37 38 -39 40 0
  > Time consumed =     0.00 sec
  > Found a better solution , value = 0.036720
    21 22 23 -24 25 -26 -27 -28 -29 -30 -31 -32 -33 -34 35 36 -37 -38 -39 40 0
  > Time consumed =     0.00 sec
[INFO] Stopping analysis ...
  > Found an optimizing assignment to exist vars:
    21 22 23 -24 25 -26 -27 -28 -29 -30 -31 -32 -33 -34 35 36 -37 -38 -39 40 0

==== Solving results ====

  > Satisfying probability: 3.672016e-02
  > Time =     0.01 sec
nianzelee commented 3 years ago

Thank you for reporting the bug.

Unfortunately, I could not find a configuration for erSSAT to produce the correct answer now. It seems to be a problem in the counting phase: the found optimal assignment does match that of DC-SSAT. I will try to investigate this issue further.