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.