Lower bound is 0

[mahi045]

Hi, I am running some instances. The _satClause has some minterms. But the current Lower bound = 0.000000e+00. Is it logically correct? I set -L 1000. I tried with both BDD and cachet. In both cases, the lower bound is same. The screenshot is given here below:

The input dimacs file is here

[nianzelee]

First, there are two unwanted white spaces in line 3 of the above input file, one after quantifier e and the other before the newline character. It is better to remove them because some tools might not be able to parse the file.

reSSAT uses float to store probabilities, and hence it might suffer from underflow (c.f. #15 ) if the probability is too small, which seems to be the case here.

Possible solutions include:

• Specify a larger number of SAT cubes, e.g., 100000,
• Try other SSAT solvers,
• Dump the cubes and feed them to (weighted) model counters, which usually handle numbers better.

I quickly tried the first two solutions, but they did not look promising. Specifying -L 10000 still yields trivial lower bounds, and DC-SSAT cannot solve the formula either (killed by the OS). Therefore, I would recommend the third solution to you. Take a look at this function for how to dump the cubes.

P.S. You may use the option -v to see more information during the run.

[mahi045]

Thanks for the information. I would like to inform you that the number of UNSAT clauses is always 1. It seems surprising to me.

[nianzelee]

It is common for reSSAT to have fewer UNSAT cubes and many SAT cubes because the generalization step for an UNSAT minterm is stronger (based on SAT solving), covering many minterms in one shot.

[mahi045]

The log file of cachet after adding 11000 SAT miniterm is here:

cachet version 1.21, December 2005
copyright 2005, University of Washington
incorporating code from zchaff, copyright 2004, Princeton University
Solving temp.wcnf ......
Number of unit clauses          0

Learning                ON
Approximate hashing         ON
Multiple precision          OFF
Static ordering             OFF
Dynamic heuristic           VSADS

Cache table size            5242880
Oldest age allowed          1048576
Max cache entries           20971520
Added cache entries         10477
Removed cache entries           0
Number of cache hits            1563
Number of pos hits          1218
Number of neg hits          345
Number of collisions            11

Cross component implications        ON
Number of cross implications        0
Backtrack factor            2
Number of far backtrack         0

Number of total components      12053
Number of split components      0
Number of non-split components      12053
Number of SAT residual formula      9986
Number of trivial components        13
Number of changed components        0
Number of adjusted components       0
First component split level     100000

Number of Decisions         10477
Max Decision Level          90
Number of Variables         91
Original Num Clauses            11000
Original Num Literals           1001000
Added Conflict Clauses          147
Added Conflict Literals         13230
Deleted Unrelevant clauses      0
Deleted Unrelevant literals     0
Number of Implications          21116
Total Run Time              8.03527

Satisfying probability          1
s 2475880078570760549798248448
Number of solutions 2.47588e+27

The one minus satisfying probability is 1. The corresponding wcnf file is here.

Do we need to add more miniterms to get a non-trivial probability?

[nianzelee]

The one minus satisfying probability is 1

I guess you meant 0, the trivial lower bound.

Do we need to add more minterms to get a non-trivial probability?

You could try, but Cachet would take a longer time. You could also solve the wcnf file with more advanced model counters from the competition.

[nianzelee]

I had a closer look at the wcnf file. It only consists of minterms, which means we can directly sum up their probabilities in this case.

If you have a family of benchmarks that exhibit such property, you could implement the counting part as a simple summation of probabilities.

[mahi045]

Good idea, thank you.

[mahi045]

One question to clear confusion: "you have a family of benchmarks that exhibit such property" => if some clauses are not the minterms, can we compute the probability by simple summation? (I think it is still correct)

[nianzelee]

If there are overlapping between cubes, we cannot directly sum up their respective probabilities because we will be counting the same space more than once.

If all of the cubes are mutually exclusive, we can still sum up their probabilities.