Add weighted_model_count binary

[mattxwang]

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:

{
  "order": ["Y", "X"]
}

weights.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:

{
  "partials": [
    { "X": true },
    { "X": false, "Y": true }
  ]
}

weights.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:

{
  "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.

[mattxwang]

Here's another example that demonstrates the new primitives:

(Xor (Iff (Var X) (Var Y)) (Ite (Var Z) (Not (Var X)) (Not (Var Y))))

[mattxwang]

Adding the new workflow for partial model assignment!

formula.sexp:

(And (Or (Var X) (Var Y)) (Or (Not (Var X)) (Not (Var Y))))

config.json:

{
  "partials": [
    { "X": true },
    { "X": false }
  ]
}

weights.json:

{
    "X": {
      "low": 0.3,
      "high": 0.7
    },
    "Y": {
      "low": 0.4,
      "high": 0.6
    }
}

running

cargo run --bin weighted_model_count --features="cli" -- -f formula.sexp -c config.json -w weights.json -o out.json

generates:

{
  "bdd_size": 2,
  "results": [
    {
      "partial_model": {
        "X": true
      },
      "wmc": 0.4
    },
    {
      "partial_model": {
        "X": false
      },
      "wmc": 0.6
    }
  ]
}