Using WAPS for custom application

[snerligit]

Hi,

We want to use WAPS to sample for one of our applications. Currently, we used WAPS and it stalls indefinitely. I have a couple of questions. It would be very helpful if you (or your team members) can guide us.

If F is a CNF formula with variables X = {x_1, x_2,…, x_n} and S is the set of satisfying assignments of F. Our understanding is that WAPS makes it possible to specify any subset V of X, so that the samples returned will take the form of strings of length n such as the following: 11*1000011**1
where the variables with * are the variables not in our set of interest V. Given enough samples of the above type we can compute the joint probability distribution of the variables in V (induced by selecting uniformly from S).

In our case we don’t really care about the joint distribution of the variables in the set of interest V. The only thing we care about is whether some of the variables in V are “highly polarized.” This means that, in principle, our set V (of variables of interest) could even be as small as a single variable. That is, we run the sampler with V consisting of a single variable x, get 1000 samples (in each of which the only thing we learn is the value of x), and if x takes the same value in, say, 950 of the samples or more, we record x.

Also, we believe that asking the sampler for only one variable at a time, may make its life much easier. Is it possible to do this? If so, can we modify WAPS to achieve this?

[rahulguptakota]

I would suggest that you try and compile to d-DNNF independently using D4/Dsharp and see if that stalls as well.

Getting joint probability distribution given enough samples seems to be alright. Although, I think that you can only get probabilistic approximate guarantees given a finite number of samples.

For realizing the polarized variables, considering that our approach uses a d-DNNF of the original formula, I would instead suggest that you rather modify sharpSAT/Dsharp directly instead of getting samples via WAPS. Exact conditioned model counting can give you an exact estimate of the polarity.

A sampler would be useful if it does not uses entire search space exploration.

[snerligit]

Thank you very much for your suggestion. On an other note, I have a following cnf file from which I want to sample using the corresponding weight files. I see that WAPS doesn't move forward. Is it our problem instance that is making it hard for WAPS or something else? Any help would be great.

Thanks again.
test.zip

[rahulguptakota]

Can you please post the output of /usr/bin/time -v for a complete d-DNNF compilation of your test example -via Dsharp?

[snerligit]

cachesize Max: 2084718 kbytes
#Vars:11053
#Clauses:37223
#bin Cls:27026
BEGIN preprocessing
found UCCL965

END preprocessing
#Vars remaining:2010
#Clauses remaining:5784
#bin Cls remaining:4495
CCls (all/bin/unit): 10000/1/0
cachedComponents:50000 avg. size:86.7493
Cache: usedMem 10485976Bytes
cache hits:50000 avg size:43.6067
CCls (all/bin/unit): 20000/1/0
cache hits:100000 avg size:41.2659
Cache: usedMem 20971548Bytes
CCls (all/bin/unit): 30000/1/0
cachedComponents:100000 avg. size:95.5489
cleaned:CCls (all/bin/unit): 991/1/0
Cache: usedMem 31457552Bytes
cache hits:150000 avg size:49.5072
CCls (all/bin/unit): 10000/1/0
cachedComponents:150000 avg. size:117.932
Cache: usedMem 41943296Bytes
CCls (all/bin/unit): 20000/1/0
cache hits:200000 avg size:57.7309
CCls (all/bin/unit): 30000/1/0
Cache: usedMem 52428944Bytes
cleaned:CCls (all/bin/unit): 960/1/0
cachedComponents:200000 avg. size:129.304

...
I have posted only the first few lines. This continues for hours.

The following is what I get from WAPS:

Seperating weights from Input cnf
Extracting the Sampling Set
c WARNING: for repeatability, setting FPU to use double precision
c Problem Statistics:
c
c Benchmark Information
c Number of variables: 11053
c Number of clauses: 35064
c Number of literals: 85873
c Parse time: 0.01
c
c d-DNNF Information
c Number of nodes: 2111861
c Number of edges: 4347054
c
c Final time: 1914.994876
c
s 140064579303505920
The time taken by D4/Dsharp_PCompile is 2082.7789056301117
The time taken to parse the nnf text: 516.8805592060089

After this it just continues to stay indefinitely.

[rahulguptakota]

How much time did you wait before killing the process? It should be annotating the d-DNNF in this time.
Hard instances can occur even under just 100 variables. d-DNNF for this instance seems to be large as just parsing it took more than 500 seconds.

[snerligit]

I waited for about 2-3 hours I think. In the past, I have let WAPS run for more than 24 hours for this instance.