Unexpected behaviour for disjunction

[rimvydasrub]

Simple disjunction of literals seems to be evaluated incorrectly. For the following input:

using LogicCircuits

println("Disjunction of two literals")
p, q = pos_literals(LogicCircuit, 2)
circuit1 = p | q

println("true | true = $(circuit1(true,true))")
println("true | false = $(circuit1(true,false))")
println("false | true = $(circuit1(false,true))")
println("false | false = $(circuit1(false,false))")

println("is satisfiable?: $(issatisfiable(circuit1))")
println("is tautology?: $(istautology(circuit1))")
println("model count: $(model_count(circuit1))")
println()

println("Disjunction of three literals")
a, b, c = pos_literals(LogicCircuit, 3)
circuit2 = a | b | c

println("true | true | true = $(circuit2(true,true,true))")
println("false | true | true = $(circuit2(false,true,true))")
println("true | false | true = $(circuit2(true,false,true))")
println("true | true | false = $(circuit2(true,true,false))")
println("false | false | true = $(circuit2(false,false,true))")
println("true | false | false = $(circuit2(true,false,false))")
println("false | true | false = $(circuit2(false,true,false))")
println("false | false | false = $(circuit2(false,false,false))")

println("is satisfiable?: $(issatisfiable(circuit2))")
println("is tautology?: $(istautology(circuit2))")
println("model count: $(model_count(circuit2))")

I observe the following output:

Disjunction of two literals
true | true = true
true | false = true
false | true = true
false | false = false
is satisfiable?: true
is tautology?: true
model count: 4

Disjunction of three literals
true | true | true = true
false | true | true = true
true | false | true = true
true | true | false = true
false | false | true = true
true | false | false = true
false | true | false = true
false | false | false = false
is satisfiable?: true
is tautology?: false
model count: 12

• The disjunction of two literals is evaluated as tautology and having model count 4, yet the truth table clearly indicates that false | false is evaluated as false
• For disjunction of 3 literals, model count is 12, yet there could at most be 8 models for circuit with 3 literals.

[khosravipasha]

Hi, thanks for the detailed issue.

model_count does not enumerate models to count how many are true (cause there are exponential). Here we have a tractable version of model_count which comes with few restrictions.

model_count can only be used when the circuit is deterministic, in this case p | q and a | b | c are not deterministic so we get wrong answers for model_count. Additionally, istautology uses model_count so that also gets wrong answer.

We are planning to add some prerequsites so it makes it easier to know when you can use different functions.

[guyvdbroeck]

For now you could go through SDD compilation to obtain a circuit that is deterministic and allows for efficient and correct model counting

[rimvydasrub]

Thank you for the API clarification. Performing SDD compilation resolves the problem.

[guyvdbroeck]

Great. I will close this as we have https://github.com/Juice-jl/ProbabilisticCircuits.jl/issues/61 to already keep track of this API flaw.