DNF

[lengyijun]

This pr is not ready to merge. I just want to show something. A DNF is defined as:

(x_1 & x_2 & x_3) | (!x_1 & x_2 & x_3) | (x_1 & !x_2 & !x_3)

I found that build a BDD of DNF is quite time-wasting(maybe I do something wrong). So I write a recursive way to deal with it. It visit every atom only once.

new                     time:   [31.313 ms 31.428 ms 31.562 ms]                
Found 13 outliers among 100 measurements (13.00%)
  8 (8.00%) high mild
  5 (5.00%) high severe

Benchmarking old: Warming up for 3.0000 s
Warning: Unable to complete 100 samples in 5.0s. You may wish to increase target time to 145.8s, or reduce sample count to 10.
old                     time:   [1.4519 s 1.4528 s 1.4538 s]                   
Found 7 outliers among 100 measurements (7.00%)
  4 (4.00%) high mild
  3 (3.00%) high severe

Some questions

1. If there is a better way to DNF already in biodivine-lib-bdd or in other implementation?
2. If DNF is a universal circumstance? At least for me, it's the only input format.
3. Bitset instead of Vec<Bool>?
4. CNF

Reference: https://www.cmi.ac.in/~madhavan/courses/verification-2011/andersen-bdd.pdf exercise 4.3

[daemontus]

This looks like it could be a nice addition at some point!

At the moment, your benchmark is probably the best we can do in lib-bdd. I also don't see any DNF or clause-specific API in other libraries (e.g. CUDD), but I may be missing something. So as far as I can tell, people generally don't target this specifically in implementations. But that doesn't mean we can't have a special method for it.

However, in this particular case, the design of lib-bdd is indeed quite inefficient, because there is a lot of rather trivial operations (especially the inner for loop). The BDDs still need to be allocated/deallocated for each operation, hence it takes so long. We have an experimental API that adds native operations for "cubes" (essentially clauses in DNF) - see branch cubes. This should speed things up quite a bit once released.

I have merged everything into a single branch here and added a comparison with CUDD as a "baseline". With cubes, the operation is still slower than your specialised implementation, but at least it is not as "tragic" :D

new                     time:   [70.356 ms 71.310 ms 72.283 ms]     
cudd                    time:   [227.98 ms 235.88 ms 244.69 ms]    
old-cubes               time:   [202.68 ms 211.57 ms 223.36 ms]  
old                     time:   [2.3704 s 2.4167 s 2.4676 s] 

So as a short term solution, I can merge the cube API and publish it in a new version. If you still need better performance, we can build a production ready version of your DNF algorithm - I think it is a useful feature to have.

Misc:

• Input format: We generally start with small, human-written formulas that are quick to import (the big ones are then built from that), so we generally don't care if the formula is CNF/DNF/etc. However, I wouldn't mind having a specialised methods for this.
• Vec<bool> vs. BitSet: We can test that, but I don't expect it to make much of a difference. The advantage is mostly in smaller memory footprint, so if you can fit your DNF formula into memory with Vec<bool>, I would go with what's easier to use.

[daemontus]

I've created a pull request for the cubes API here: #20. I'll try to look into it soon :)

[daemontus]

In version 0.3.0, there is now a new (more efficient) API for creating DNF/CNF formulas.

This is still not as efficient as this PR proposes (that would require lifting the Bdd node order requirement which has not happened yet). Hence I will not be closing this yet, however an issue (#24) has been created to track progress on this new implementation.

[daemontus]

It only took ... two years ... but the new CNF/DNF translation algorithms are now implemented in version 0.5.0.

If this is still (somewhat) relevant for you, please test if the new implementation performs as you would expect :)

Otherwise, I am closing this as no longer relevant.