Module reliability

Module reliability 

Source
Expand description

§Network reliability

Two sites, s and t, are joined by a small network of five links. Each link works on a given day with probability 0.9, independently of the others. How likely is it that s can still reach t, and which link matters most?

Run the complete program with cargo run --example reliability.

§Describe connection as clauses

Links 1 (s–a), 2 (s–b), 3 (a–b), 4 (a–t) and 5 (b–t) form the classic bridge network. A variable is true when its link works. The sites are disconnected exactly when every link of some cut fails, so they are connected when every cut keeps a working link: {1, 2} around s, {4, 5} around t, and the two cuts through the bridge, {1, 3, 5} and {2, 3, 4}. Each cut becomes one clause.

ⓘ
let network = "\
c t wmc
p cnf 5 4
1 2 0
4 5 0
1 3 5 0
2 3 4 0
";

The c t wmc line declares the task: a weighted model count.

A weighted model count gives each literal a weight. An assignment weighs the product of its literals’ weights, and the count is the sum over the assignments that satisfy the formula. With a link’s probability of working on its positive literal and the probability of failing on its negative one, an assignment weighs its probability, and the count is the probability that the sites are connected. c p weight lines carry the weights, one for each literal of each link.

ⓘ
/// The weight lines for links that each work with the given percentage.
fn weights(percent_working: [u32; 5]) -> String {
    let mut lines = String::new();
    for (link, percent) in (1..).zip(percent_working) {
        lines += &format!("c p weight {link} {percent}/100 0\n");
        lines += &format!("c p weight -{link} {}/100 0\n", 100 - percent);
    }
    lines
}

§Count

The header declares the task, so count needs no Mode. The weighted count is computed in floating point, and Count::to_f64 reads it as a number.

ⓘ
let reliable = [90; 5];
let instance = format!("{network}{}", weights(reliable));
let answer = tididi_cnf::count(parse_dimacs(instance.as_bytes())?, None, &Limits::default())?;
println!("Connected: {:.5}", answer.count().to_f64());

Output:

Connected: 0.97848

A link that is down works with probability 0. Taking each link down in turn shows how much the network depends on it:

ⓘ
for link in 1..=5 {
    let mut broken = reliable;
    broken[link - 1] = 0;
    let instance = format!("{network}{}", weights(broken));
    let answer = tididi_cnf::count(parse_dimacs(instance.as_bytes())?, None, &Limits::default())?;
    println!("Connected with link {link} down: {:.5}", answer.count().to_f64());
}

Output:

Connected with link 1 down: 0.88290
Connected with link 2 down: 0.88290
Connected with link 3 down: 0.96390
Connected with link 4 down: 0.88290
Connected with link 5 down: 0.88290

Without the bridge, s reaches t over a–t or b–t: 1 − (1 − 0.81)² = 0.9639. Each outer link matters more: without link 1, every route starts on link 2.

The complete program also builds the instance text for each case.