1. Configuration rules

A backup application offers local storage, remote storage, encryption, and notifications. It needs at least one storage destination; remote backups require encryption. The rule is

(L ∨ R) ∧ (¬R ∨ E).

Notifications are optional. We will count the valid configurations, inspect forced choices, and follow a user changing their selections.

from tididi import Literal, Vtree, cube, literal

vtree = Vtree.balanced(4)
local_choice = Literal(1)
remote_choice = Literal(2)
encrypted_choice = Literal(3)
notifications_choice = Literal(4)
names = {1: "local backups", 2: "remote backups", 3: "encryption", 4: "notifications"}

local = literal(vtree, local_choice)
remote = literal(vtree, remote_choice)
encrypted = literal(vtree, encrypted_choice)
notifications = literal(vtree, notifications_choice)

1.1. Build and count

remote.copy() creates an operand for this operation so the original remains available. The resulting circuit owns its storage.

destination = local | remote.copy()
encryption_rule = ~remote.copy() | encrypted.copy()
configurations = destination & encryption_rule
print("Valid configurations:", configurations.model_count())
with_notifications = configurations.copy() & notifications
print("With notifications:", with_notifications.model_count())

Valid configurations: 8
With notifications: 4

1.2. Inspect a user’s choices

Requiring remote backups leaves only configurations with encryption.

with_remote = configurations.copy() & remote
print("With remote backups:", with_remote.model_count())
for choice in with_remote.implied_literals():
    print(f"Required choice: {names[choice.variable]} = {choice.sign}")
remote_without_encryption = with_remote & ~encrypted
print("Satisfiable:", remote_without_encryption.is_sat())

With remote backups: 4
Required choice: remote backups = True
Required choice: encryption = True
Satisfiable: False

A witness chooses one value for every variable. It is a list of immutable Literal values that can be reused to construct a cube.

witness = configurations.satisfying_assignment()
for choice in witness:
    print(f"{names[choice.variable]}: {choice.sign}")
selected = configurations.copy() & cube(vtree, witness)
print("Selected valid configurations:", selected.model_count())

local backups: True
remote backups: True
encryption: True
notifications: False
Selected valid configurations: 1

1.3. Count under changing observations

A counter owns the circuit while it retains cached counts. Creating it consumes configurations. Observations use the named literal values, which are reusable and do not own circuits.

counter = configurations.counter()
counter.observe([remote_choice])
print("Matching configurations:", counter.model_count())
counter.observe([~notifications_choice])
print("Matching configurations:", counter.model_count())
counter.observe([~remote_choice, ~encrypted_choice])
print("Matching configurations:", counter.model_count())
counter.clear_observations()
print("Matching configurations:", counter.model_count())

Matching configurations: 4
Matching configurations: 2
Matching configurations: 1
Matching configurations: 8

Finish the counter to recover its original diagram. Its observations never changed that diagram. Minimization returns a canonical circuit for this vtree.

configurations = counter.finish().minimize()
print("Valid configurations:", configurations.model_count())
print("Minimized pairs:", configurations.pair_count())

Valid configurations: 8
Minimized pairs: 8