eyeprolog

A feature model in Boolean constraints

Which product configurations are valid, and how many are there?

A product line offers four features with rules about which go together. EyeProlog states those rules as Boolean constraints, lists every valid configuration, and counts them without enumerating them first.

Run it in the playground · Source

The question

A deployment runs either in the cloud or at the edge, never both. Auditing needs encryption. An edge deployment needs auditing. Which combinations of cloud, edge, audit, and encryption satisfy all three rules?

This is a feature model: the kind of rulebook a product line uses to keep customers from ordering a configuration that cannot work.

The rules as constraints

feature_constraints(Cloud, Edge, Audit, Encryption) :-
  sat((Cloud # Edge) *
      (Audit =< Encryption) *
      (Edge =< Audit)).

Each feature is a 0/1 variable from library(clpb). # is exclusive or, * is “and”, and A =< B on Booleans reads “if A then B”. The three factors are the three rules, written once.

Listing and counting

feature_plan(features(
    cloud(Cloud), edge(Edge), audit(Audit), encryption(Encryption))) :-
  feature_constraints(Cloud, Edge, Audit, Encryption),
  labeling([Cloud, Edge, Audit, Encryption]).

feature_plan_count(Count) :-
  sat_count((_Cloud # Edge) *
            (Audit =< _Encryption) *
            (Edge =< Audit), Count).

labeling/1 turns the constraints into concrete 0/1 assignments. sat_count/2 counts the solutions of the formula directly from its binary decision diagram, without producing them one by one.

The answer

eyeprolog examples/clpb-feature-model.pl

feature_plan(features(cloud(0), edge(1), audit(1), encryption(1))).
feature_plan(features(cloud(1), edge(0), audit(0), encryption(0))).
feature_plan(features(cloud(1), edge(0), audit(0), encryption(1))).
feature_plan(features(cloud(1), edge(0), audit(1), encryption(1))).
feature_plan_count(4).

One edge configuration, which must audit and encrypt, and three cloud configurations. The count agrees with the list.

The reason

step(feature_plan(features(cloud(0), edge(1), audit(1), encryption(1))),
     rule(2),
     ['Cloud' = 0, 'Edge' = 1, 'Audit' = 1, 'Encryption' = 1],
     [feature_constraints(0, 1, 1, 1), labeling([0, 1, 1, 1])]).
step(sat((0 # 1) * (1 =< 1) * (1 =< 1)), builtin, [], []).

The edge plan comes from the feature_plan/1 rule with all four variables bound. Its support is the constraint formula with those values substituted: 0 # 1, 1 =< 1, 1 =< 1, which is plainly true.

The check

condition('C5', re_decision, ok, 4).
obligation(builtin, stateful, sat((0 # 1) * (1 =< 1) * (1 =< 1))).
obligation(builtin, stateful, sat_count((A # B) * (C =< D) * (B =< C), 4)).
trusted(5).
verdict(checked_with_obligations).

The checker verifies the rules and recomputes four built-in steps. The sat/1 and sat_count/2 calls depend on the constraint store the run built up, so the checker cannot recompute them in isolation. It records them as obligations: the proof holds provided those five constraint results are right. The verdict says exactly that.

Try it

Drop the rule Edge =< Audit from feature_plan_count/1. The count rises from 4 to 6; which two configurations are new?
Add a fifth feature, backup, required by audit, and predict the new count before running it.
Ask only for edge plans: --goal 'feature_plan(features(cloud(0), E, A, X))'.

Learn more in The Art of EyeProlog, Chapter 10.

This site is open source. Improve this page.