Bug in model_count after conjoin of non-smooth and using Lit(2)

[khosravipasha]

This should hold for model_count but it does not:

mc(delta | x_1) + mc(delta | not x_1) = mc(delta)

The issue imight be because of conjoin on non-smooth circuits.

[khosravipasha]

Smooth a circuit and compile to sdd then conjoin and compare model count

using LogicCircuits
random_lc = zoo_sdd("random.sdd");
vtree = zoo_vtree("random.vtree");

plc = propagate_constants(random_lc , remove_unary=true);
structplc = compile(StructLogicCircuit, vtree, plc);
sstructplc = smooth(structplc);
lits = pos_literals(LogicCircuit, num_variables(random_lc))


manager = SddMgr(sstructplc.vtree)
sdd = compile(manager, sstructplc)
sdd_lits = pos_literals(Sdd, manager, num_variables(random_lc))

model_count(random_lc), model_count(sstructplc)

model_count(sdd & sdd_lits[2]), model_count(sdd & -sdd_lits[2])

model_count(conjoin(random_lc, Lit(2))), model_count(conjoin(random_lc, Lit(-2)))

model_count(conjoin(random_lc, lits[2])), model_count(conjoin(random_lc, -lits[2]))

model_count(conjoin(LogicCircuit(sstructplc), Lit(2))), model_count(conjoin(LogicCircuit(sstructplc), Lit(-2)))

model_count(conjoin(LogicCircuit(sstructplc), lits[2])), model_count(conjoin(LogicCircuit(sstructplc), -lits[2]))

Output: First one is withouth conjoining. The others should all be equal but second one is wrong (i.e. conjoin on a non-smooth circuit and then using Lit(2)). All other cases seem correct.

julia> model_count(random_lc), model_count(sstructplc)
(65536, 65536)

julia> model_count(conjoin(random_lc, Lit(2))), model_count(conjoin(random_lc, Lit(-2)))
(55552, 55552)

julia> model_count(sdd & sdd_lits[2]), model_count(sdd & -sdd_lits[2])
(32768, 32768)

julia> model_count(conjoin(random_lc, lits[2])), model_count(conjoin(random_lc, -lits[2]))
(32768, 32768)

julia> model_count(conjoin(LogicCircuit(sstructplc), Lit(2))), model_count(conjoin(LogicCircuit(sstructplc), Lit(-2)))
(32768, 32768)

julia> model_count(conjoin(LogicCircuit(sstructplc), lits[2])), model_count(conjoin(LogicCircuit(sstructplc), -lits[2]))
(32768, 32768)

Doing & with Sdds

Update: now works correctly as expected.

sun, rain, rainbow = pos_literals(LogicCircuit, 3)
circuit = (rainbow & sun & rain) | (-rainbow); # rainbow implies sun and rain
manager = SddMgr(7, :balanced)
circuit = compile(manager, circuit);
sun, rain, rainbow, cloud, snow, belgium, los_angeles = pos_literals(Sdd, manager, 7)
circuit &= (-los_angeles | -belgium) # cannot be in LA and Belgium at the same time
circuit &= (los_angeles ⇒ sun) ∧ (belgium ⇒ cloud) # unicode logical syntax
circuit &= (¬(rain ∨ snow) ⇐ ¬cloud); # no rain or snow without clouds


circuit_sun = circuit & sun # condition(circuit, sun) throws error cannot condition sdd
circuit_nosun = circuit & -sun # condition(circuit, -sun) throws error cannot condition sdd

model_count(circuit) # 29
model_count(circuit_sun)  # 20 
model_count(circuit_nosun) # 9