plans for bex

My highest priority goal is to improve the speed of the solver(s).

[4/6] version 0.1.6 : optimization round

remove `nvars` param from `Base`

remove redundant `vindex` from `HiLoCache`

port BddSwarm to new swarm::Swarm framework

[0/4] solver optimizations

use concurrent data structures (dashmap and boxcar) for BddState to avoid copies

make debug output optional

optimization: nid-level truth tables for bottom 5 variables

have swarm workers descend lo branches on their own

This should help fully utilize each CPU

[2/3] better graphviz rendering

use command line argument instead of macro parameter to toggle solver visualizations

examples:

cargo test nano_bdd -- -- -a     # show AST
cargo test nano_bdd -- -- -r     # show result
cargo test nano_bdd -- -- -a -r  # show both
cargo test nano_bdd -- --nocapture -- -a -r  # show both, and include output logs

draw inverted top level with an extra “not” node

group bdd/anf nodes by level

some combination of these ideas:

{ edge [ style=invis ];
  rankdir=LR;
   rank=same; }

[4/4] other improvements

move `expr` macro to the base module

come up with basic decorator pattern scheme for bases

will use for things like:

toggle bookkeeping for benchmarks
toggle individual optimizations
consolidate BASE/anf normalizers
swap out work coordination strategies (swarm/etc)
swap out different kinds of normalizer (main vs ITE) (allow preserving the original expression)
toggle use of constant truth tables in the nid
configure larger constant truth tables at other levels
even toggle caching to see what it gets us

remove .i, .o, .var, vir from `Base`

Use the corresponding nid functions instead.

extract `vhl::Walkable` trait, and add `walk_up`

– backlog (unsorted) –

[0/2] better benchmarking

[2/3] collect metrics

what to collect

for each benchmark:
- original AST:
  - time to generate
  - number of nodes (broken down by type?)
  - number of cache tests/fails (not really that important, but might as well?)
- for each step:
  - time to generate
  - number of nodes at each step
  - number of xmemo cache tests/fails (we don’t care about hilos)
  - number calculations saved from short circuits

`Base::ord(nid)` for graph order (number of nodes)

record timing information at each step

I do this now in seconds. Let’s switch to millis.

track cache attempts / hits

I can’t do this in the base itself because copies are shared and therefore immutable.

So instead, use thread-local counters:

xmemo lookup
xmemo fail
hilos lookup
hilos fail
hilos create

Query, sum, and reset the counters after each round.

store the metrics

write (step#, time, ord, lookups, hits, shorts) to csv after each step

[2/3] swarm for ANF

extract basic test suite for `trait Base`

Just take the simple tests that exist for ast and bdd

Create anf.rs stub and get the simple tests passing.

Extract wip.rs from BDDSwarm

WIP = work in progress

The idea is to reify work-in-progress so that the work can be prioritized and distributed across multiple workers.

trait WIPBase : Base

Slow-running bases should be WIP.
- Q: type for queries
- W: type for work-in-progress nodes
- C: type for finished work cache

struct FWBaseW:WIPBase

This is a generic type finished work.

Finish the ANF implementation as a WIPBase.

add some more benchmarks

keep scaling the multiplication problem search space by 1 bit

and/xor tables for fns of n bits

n queens

https://github.com/chrisying/parabdd/blob/master/src/nqueens.cpp

compare benchmarks

compare to CUDD

proper sifting for bdds

more new base types

ZddBase

CnfBase

Plain CNF

Tseytin Transformation

SAT solver

Biconditional BDD (a=b decomposition)

BmpBase (raw bitmaps)

allow swarms to run across the network

web browser for bases

move tagging to a separate struct

implement visitor pattern for dot, count, etc

move walk/step to top level

linear walk of the nids (for permute/save)

implement zdd base

implement biconditional bdd base (bic.rs)?

implement cnf base

https://en.wikipedia.org/wiki/Conjunctive_normal_form

implement aig (nand) base

https://en.wikipedia.org/wiki/And-inverter_graph

integrate with other rust bdd libraries

generate vhdl/verilog

generate compute shaders

visual debugger for solver

use labels for vars when generating dot

be able to highlight certain nodes

more optimization ideas

bring relevant variables to top in solver

maintain top-level vec for variable permutation
at each step:
- bring highest numbered Vir to the top
- fetch relevant inputs to Vir in the AST
- raise relevant inputs to 2nd and 3rd layers in BDD

Files

plans.org

Latest commit

History