Binaries #155
Comments
|
For the progress bar feature, perhaps indicatif is the one to look at! |
mattxwang
added a commit
that referenced
this issue
Jul 23, 2023
This PR adds a minimum version of the `bottomup_cnf_to_bdd` CLI tool. Of note is that `bin` targets require the main modules (rather than `example`, which uses test-only), so I've elected to put `clap` and `serde_json` behind a feature flag to avoid bloating the main library. This requires you to use the `--features="cli"` flag to build it. To use: ``` cargo run --bin bottomup_cnf_to_bdd --features="cli" -- -f cnf/php-4-6.cnf -v > out.json ``` Or, to use a non-default option, ``` cargo run --bin bottomup_cnf_to_bdd --features="cli" -- -f cnf/php-4-6.cnf -v --order auto_force ``` To-do: - allow manual variable order - more stats - progress bar Tracking issue: #155.
This was referenced Jul 24, 2023
mattxwang
added a commit
that referenced
this issue
Jul 24, 2023
…la_to_bdd` (#159) Part of #155. Usage: ``` $ cat bloop.sexp (And (Or (Var X) (Var Y)) (Or (Not (Var X)) (Not (Var Y)))) $ cargo run --bin bottomup_formula_to_bdd --features="cli" -- -f bloop.sexp {"nodes":[{"topvar":1,"low":"False","high":"True"},{"topvar":0,"low":{"Ptr":{"index":0,"compl":true}},"high":{"Ptr":{"index":0,"compl":false}}}],"roots":[{"Ptr":{"index":1,"compl":true}}]} ``` Or, for a manual ordering, ``` $ cat bloop.sexp (And (Or (Var X) (Var Y)) (Or (Not (Var X)) (Not (Var Y)))) $ cat bloop.json { "order": ["Y", "X"] } $ cargo run --bin bottomup_formula_to_bdd --features="cli" -- -f bloop.sexp -v --ordering manual -c bloop.json === METADATA === variable mapping: {"X": 0, "Y": 1} variable ordering: [1, 0] === STATS === compilation time: 0.0033s recursive calls: 9 {"nodes":[{"topvar":0,"low":"False","high":"True"},{"topvar":1,"low":{"Ptr":{"index":0,"compl":true}},"high":{"Ptr":{"index":0,"compl":false}}}],"roots":[{"Ptr":{"index":1,"compl":true}}]} ```
mattxwang
added a commit
that referenced
this issue
Jul 24, 2023
mattxwang
added a commit
that referenced
this issue
Aug 15, 2023
Goal: unblock Lisa! Ref: #155. This PR adds a new binary, `weighted_model_count`, that allows users to perform model counts over arbitrary boolean formulas (via BDD compilation). A brief sketch of the functionality: - inputs: - a logical formula (specified with `-f`) in s-expression format; supports primitives (`And`, `Or`, `Not`) and helpers (`Ite`, `Xor`, `Iff`) - a `weights.json` (specified with `-w` that specifies `low` and `high` weights for each boolean variable. for now, they must be reals (i.e. compiled with `RealSemiring`); missing weights are inferred to be `0` (and are logged to the console) - a `config.json` (specified with `-c`) that: - optionally specifies a variable order; if none is provided, a linear one is used (inferring all variables from the formula) - optionally specifies a set of partial models to perform the WMC on; if none is provided, a WMC is done on the entire formula - output (via JSON, path specified with `-o`): - the resulting size of the (unsmoothed) BDD - smoothed WMCs over each partial model - optional flags: - `-s`: silence all output - `-v`: more verbose output, includes timing statistics You can test out the binary using `cargo run` (see below). To compile it for production use, instead run: ``` $ cargo build --bin weighted_model_count --release --features="cli" ``` This should give you a binary `weighted_model_count` in `target/release`. ## usage: single WMC To use, with: `formula.sexp` (this formula represents `X XOR Y`): ``` (And (Or (Var X) (Var Y)) (Or (Not (Var X)) (Not (Var Y)))) ``` `config.json`: ```json { "order": ["Y", "X"] } ``` `weights.json`: ```json { "X": { "low": 0.3, "high": 0.7 }, "Y": { "low": 0.4, "high": 0.6 } } ``` Run: ``` $ cargo run --bin weighted_model_count --features="cli" -- -f formula.sexp -c config.json -w weights.json 0.45999999999999996 ``` (floating-point rounding error!) Run with `-v` to get more statistics. ## partial models optionally, you can WMC over various partial models on one formula. `formula.sexp`: ``` (And (Or (Var X) (Var Z)) (Or (Not (Var X)) (Not (Var Y)))) ``` `config.json`: ```json { "partials": [ { "X": true }, { "X": false, "Y": true } ] } ``` `weights.json`: ```json { "Y": { "low": 0.4, "high": 0.6 }, "Z": { "low": 0.2, "high": 0.8 } } ``` running ``` cargo run --bin weighted_model_count --features="cli" -- -f formula.sexp -c config.json -w weights.json -o output.json ``` gives: ```json { "bdd_size": 3, "results": [ { "partial_model": { "X": true }, "wmc": 0.4 }, { "partial_model": { "X": false, "Y": true }, "wmc": 0.8 } ] } ``` Observe that adding an empty partial model (with `{}`) recovers a WMC over the entire input formula.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add a
/bin/directory that organizes the following main binaries for interacting with the library.bottomup_cnf_to_bdd: takes as input a CNF and outputs a BDD.order, specifies a variable order:auto_minfill: use a min-fill heuristic to find the variable orderingauto_force: use the FORCE heuristic to find a variable orderingmanual: provide a manual variable order as a JSON filestrategy, specifies a compilation order (i.e., a tree describing the sequence in which clauses are conjoined together)dtree, uses the dtree decomposition of the CNF according to the variable orderverbose, show verbose output (timing information, hash table information, etc.)progress, show a progress bar that gives an estimate of compilation progress (fraction of compiled clauses)bottomup_formula_to_bdd: takes as input an arbitrary logical formula and outputs a BDD.JSONformat)orderingmanual, must provide a manual variable order.interaction_minfill: user provides an interaction graph between variables and minfill is run to extract a good variable orderbottomup_cnf_to_sdd: same as for BDDbottomup_formula_to_sdd: same as for BDDcnf_to_ddnnf: compiles a d-DNNF from a CNForder, specifies a variable ordering strategystatic_minfill, follows a static variable ordering based on the minfill heuristic on the graphstatic_manual, user provides a manual static variable orderingweighted_model_count: takes as input a compiled circuit and weight file and outputs the resulting weighted model countcircuit, either a dDNNF, SDD, or BDDsemiring, choice of semiring under which to perform the computationf64orrationalfor now; more to come laterweightsA JSON file describing the weights (a dictionary mapping literals to weights)The text was updated successfully, but these errors were encountered: