khosravipasha
commented
4 years ago 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
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.