Timeout on benchmark

[shaanvaidya]

Hello!
I have found a case where the tool times out (5000s). The file is pdtvisgray0_100.cnf in the attached zip archive: benchmark-files.zip
810 vars, 1909 clauses, 404 sampling set size.

Description
What we are trying to do is uniformly sample from the n-length traces of a symbolic transition system. To this end, we unroll an aig 'n' times and then convert it into CNF and specify the variables corresponding to the state bits as the sampling set. I have attached the cnf file corresponding to the pdtvisgray0.aig benchmark (hwmcc) with 100 unrollings.
After reducing the size of the network, the aig has 4 latches, 1 primary input, 1 primary output. This file is also attached.
First, we remove the original primary outputs (no use for it) and pull out the latch outputs as primary outputs so that on unrolling the transition system, copies of all intermediate state bits are present as primary outputs (they wouldn't on simply unrolling them). A blif file corresponding to this is attached
We then unroll it 100 times in abc as follows:
strash; frames -F 100
Convert the latch input and outputs to primary inputs and primary outputs respectively:
comb
And then write this to a cnf file:
write_cnf dump
We have found out the cnf variables corresponding to all the primary outputs and added them to the cnf file as the sampling set.
Since Unigen was timing out on this file and it uses ApproxMC, I tried using ApproxMCv3 on the file but it times out as well.

Files:
pdtvisgray0.aig
pdtvisgray0.blif - blif file with latch outputs pulled out as primary outputs
pdtvisgray0_100.cnf - 100 unrollings
pdtvisgray0_1000.cnf - 1000 unrollings

[msoos]

Hi,

So unrolling 100 times failed. There are two things here:

1. You should definitely check what the times are for different unrollings. How about 3? 5? 10? 20? 30? 50? etc. Then you know what to expect! Otherwise, you have no idea. With these data, you can draw a graph and have an idea :)

2. In order to fix the issue, you will need to add MORE constraints. Do you know any more constraints you can add? Sometimes there are some trivial ones! Things that you know follow from the constraints but the system doesn't know. Adding MORE constraints helps the speed! Really. Try it out. Think of more constraints.

3. What is the size of the independent set? Are you sure it's minimal? Can you check? I will soon be making (hopefully) a project of Kuldeep public that calculates or further minimizes an already guessed minimal independent set. I will give a link to it below once I have approval to make it public.

Good luck,

Mate

[msoos]

Also, making 100 and 1000 when the 100 already fails to compute -- really bad approach. Give 3! Give 5! GIve 10! Give 20! What can I do with something that doesn't terminate? How can I debug that?

[msoos]

I have now open-sourced the tool to find minimal independent sets. This will SERIOUSLY help you finding a solution. Please us it:

https://github.com/meelgroup/mis

I have also updated the README of ApproxMC here, to include how to use MIS :) Good luck and happy holidays!

[msoos]

I have received absolutely no feedback on this so I am closing. Let me know if you are happy to respond and then I'll happily reopen :)