From 3b0e018917b6b20d624f2ae725aea8e440343351 Mon Sep 17 00:00:00 2001 From: Renato Lui Geh Date: Tue, 16 Feb 2021 17:13:49 -0300 Subject: [PATCH 1/4] Add SDD to PSDD compilation --- src/structured_prob_nodes.jl | 70 +++++++++++++++++++++++++++++ test/structured_prob_nodes_tests.jl | 24 +++++++++- 2 files changed, 93 insertions(+), 1 deletion(-) diff --git a/src/structured_prob_nodes.jl b/src/structured_prob_nodes.jl index 0cf8cc32..8539fee6 100644 --- a/src/structured_prob_nodes.jl +++ b/src/structured_prob_nodes.jl @@ -135,6 +135,76 @@ function compile(::Type{<:StructProbCircuit}, vtree::Vtree, circuit::LogicCircui foldup_aggregate(circuit, f_con, f_lit, f_a, f_o, StructProbCircuit) end +function Base.convert(::Type{<:StructProbCircuit}, sdd::Sdd)::StructProbCircuit + L = Dict{Int32, StructProbLiteralNode}() + visited = Dict{Sdd, StructProbCircuit}() + Sc_sdd = variables_by_node(sdd) + ⊤_node = SddTrueNode(false, nothing) + function get_lit(l::Int32, V::Vtree, L::Dict{Int32, StructProbLiteralNode})::StructProbLiteralNode + if !haskey(L, l) + node = StructProbLiteralNode(l, V) + L[l] = node + return node + end + return L[l] + end + function passdown(S::Sdd, V::Vtree, ignore::Bool = false)::StructProbCircuit + if !ignore && haskey(visited, S) return visited[S] end + if S isa SddTrueNode + Sc = variables(V) + if length(Sc) == 1 + l = convert(Int32, first(Sc)) + return StructSumNode([get_lit(l, V, L), get_lit(-l, V, L)], V) + end + # Fully factorize. + left, right = passdown(S, V.left, true), passdown(S, V.right, true) + return StructSumNode([StructMulNode(left, right, V)], V) + elseif S isa SddLiteralNode + l = S.literal + Sc = variables(V) + if length(Sc) == 1 return get_lit(l, V, L) end + v = abs(l) + left = passdown(v ∈ variables(V.left) ? S : ⊤_node, V.left, true) + right = passdown(v ∈ variables(V.right) ? S : ⊤_node, V.right, true) + return StructSumNode([StructMulNode(left, right, V)], V) + end + # Else, disjunction node. + ch = Vector{StructProbCircuit}() + for c ∈ S.children + if c.sub isa SddFalseNode continue end + if haskey(visited, c) + push!(ch, visited[c]) + continue + end + p = passdown(c.prime, V.left) + # Corner case for when SDD is not smooth on the left. Add missing variables. + if !(V.left isa PlainVtreeLeafNode) + if V.left.left isa PlainVtreeLeafNode && V.left.left.var ∉ variables(vtree(p)) + p = StructSumNode([StructMulNode(passdown(⊤_node, V.left.left, true), p, V.left)], V.left) + end; if V.left.right isa PlainVtreeLeafNode && V.left.right.var ∉ variables(vtree(p)) + p = StructSumNode([StructMulNode(p, passdown(⊤_node, V.left.right, true), V.left)], V.left) + end + end + s = passdown(c.sub, V.right) + # Corner case for when SDD is not smooth on the right. Add missing variables. + if !(V.right isa PlainVtreeLeafNode) + if V.right.left isa PlainVtreeLeafNode && V.right.left.var ∉ variables(vtree(s)) + s = StructSumNode([StructMulNode(passdown(⊤_node, V.right.left, true), s, V.right)], V.right) + end; if V.right.right isa PlainVtreeLeafNode && V.right.right.var ∉ variables(vtree(s)) + s = StructSumNode([StructMulNode(s, passdown(⊤_node, V.right.right, true), V.right)], V.right) + end + end + e = StructMulNode(p, s, V) + visited[c] = e + push!(ch, e) + end + sum = StructSumNode(ch, V) + visited[S] = sum + return sum + end + return passdown(sdd, Vtree(sdd.vtree)) +end + function fully_factorized_circuit(::Type{<:ProbCircuit}, vtree::Vtree) ff_logic_circuit = fully_factorized_circuit(PlainStructLogicCircuit, vtree) compile(StructProbCircuit, vtree, ff_logic_circuit) diff --git a/test/structured_prob_nodes_tests.jl b/test/structured_prob_nodes_tests.jl index 3f49afe7..7c186367 100644 --- a/test/structured_prob_nodes_tests.jl +++ b/test/structured_prob_nodes_tests.jl @@ -120,5 +120,27 @@ using DataFrames: DataFrame @test num_parameters_node(r1) == num_parameters_node(r) @test isempty(intersect(linearize(r1),linearize(r))) + # Convert tests + function apply_test_cnf(n_vars::Int, cnf_path::String) + vtree = Vtree(n_vars, :random) + println("Compiling...") + sdd = compile(SddMgr(vtree), zoo_cnf(cnf_path)) + @test num_variables(sdd) == n_vars + println("Converting...") + psdd = convert(StructProbCircuit, sdd) + @test num_variables(psdd) == n_vars + @test issmooth(psdd) + @test isdecomposable(psdd) + @test isdeterministic(psdd) + @test respects_vtree(psdd, vtree) + data = DataFrame(convert(BitMatrix, rand(Bool, 100, n_vars))) + println("Testing data...") + @test all(sdd(data) .== (EVI(psdd, data) .!= -Inf)) + nothing + end + apply_test_cnf(17, "easy/C17_mince.cnf") + apply_test_cnf(15, "easy/majority_mince.cnf") + apply_test_cnf(21, "easy/b1_mince.cnf") + apply_test_cnf(20, "easy/cm152a_mince.cnf") +end -end \ No newline at end of file From c56dcae303d2c45e080cb9fc7e4dc2e452ea5f7f Mon Sep 17 00:00:00 2001 From: Tal Friedman Date: Wed, 3 Mar 2021 14:07:41 -0800 Subject: [PATCH 2/4] rewrite convert using smooth --- src/structured_prob_nodes.jl | 72 ++--------------------------- test/structured_prob_nodes_tests.jl | 2 +- 2 files changed, 6 insertions(+), 68 deletions(-) diff --git a/src/structured_prob_nodes.jl b/src/structured_prob_nodes.jl index 8539fee6..209632a2 100644 --- a/src/structured_prob_nodes.jl +++ b/src/structured_prob_nodes.jl @@ -136,73 +136,11 @@ function compile(::Type{<:StructProbCircuit}, vtree::Vtree, circuit::LogicCircui end function Base.convert(::Type{<:StructProbCircuit}, sdd::Sdd)::StructProbCircuit - L = Dict{Int32, StructProbLiteralNode}() - visited = Dict{Sdd, StructProbCircuit}() - Sc_sdd = variables_by_node(sdd) - ⊤_node = SddTrueNode(false, nothing) - function get_lit(l::Int32, V::Vtree, L::Dict{Int32, StructProbLiteralNode})::StructProbLiteralNode - if !haskey(L, l) - node = StructProbLiteralNode(l, V) - L[l] = node - return node - end - return L[l] - end - function passdown(S::Sdd, V::Vtree, ignore::Bool = false)::StructProbCircuit - if !ignore && haskey(visited, S) return visited[S] end - if S isa SddTrueNode - Sc = variables(V) - if length(Sc) == 1 - l = convert(Int32, first(Sc)) - return StructSumNode([get_lit(l, V, L), get_lit(-l, V, L)], V) - end - # Fully factorize. - left, right = passdown(S, V.left, true), passdown(S, V.right, true) - return StructSumNode([StructMulNode(left, right, V)], V) - elseif S isa SddLiteralNode - l = S.literal - Sc = variables(V) - if length(Sc) == 1 return get_lit(l, V, L) end - v = abs(l) - left = passdown(v ∈ variables(V.left) ? S : ⊤_node, V.left, true) - right = passdown(v ∈ variables(V.right) ? S : ⊤_node, V.right, true) - return StructSumNode([StructMulNode(left, right, V)], V) - end - # Else, disjunction node. - ch = Vector{StructProbCircuit}() - for c ∈ S.children - if c.sub isa SddFalseNode continue end - if haskey(visited, c) - push!(ch, visited[c]) - continue - end - p = passdown(c.prime, V.left) - # Corner case for when SDD is not smooth on the left. Add missing variables. - if !(V.left isa PlainVtreeLeafNode) - if V.left.left isa PlainVtreeLeafNode && V.left.left.var ∉ variables(vtree(p)) - p = StructSumNode([StructMulNode(passdown(⊤_node, V.left.left, true), p, V.left)], V.left) - end; if V.left.right isa PlainVtreeLeafNode && V.left.right.var ∉ variables(vtree(p)) - p = StructSumNode([StructMulNode(p, passdown(⊤_node, V.left.right, true), V.left)], V.left) - end - end - s = passdown(c.sub, V.right) - # Corner case for when SDD is not smooth on the right. Add missing variables. - if !(V.right isa PlainVtreeLeafNode) - if V.right.left isa PlainVtreeLeafNode && V.right.left.var ∉ variables(vtree(s)) - s = StructSumNode([StructMulNode(passdown(⊤_node, V.right.left, true), s, V.right)], V.right) - end; if V.right.right isa PlainVtreeLeafNode && V.right.right.var ∉ variables(vtree(s)) - s = StructSumNode([StructMulNode(s, passdown(⊤_node, V.right.right, true), V.right)], V.right) - end - end - e = StructMulNode(p, s, V) - visited[c] = e - push!(ch, e) - end - sum = StructSumNode(ch, V) - visited[S] = sum - return sum - end - return passdown(sdd, Vtree(sdd.vtree)) + lc = LogicCircuit(sdd) + plc = propagate_constants(lc, remove_unary=true) + structplc = compile(StructLogicCircuit, vtree(sdd), plc) + sstructplc = smooth(structplc) + compile(StructProbCircuit, sstructplc) end function fully_factorized_circuit(::Type{<:ProbCircuit}, vtree::Vtree) diff --git a/test/structured_prob_nodes_tests.jl b/test/structured_prob_nodes_tests.jl index 7c186367..e16c1567 100644 --- a/test/structured_prob_nodes_tests.jl +++ b/test/structured_prob_nodes_tests.jl @@ -139,7 +139,7 @@ using DataFrames: DataFrame nothing end apply_test_cnf(17, "easy/C17_mince.cnf") - apply_test_cnf(15, "easy/majority_mince.cnf") + apply_test_cnf(14, "easy/majority_mince.cnf") apply_test_cnf(21, "easy/b1_mince.cnf") apply_test_cnf(20, "easy/cm152a_mince.cnf") end From d53f614b26a7e40109eeb43c063ba896b165a6b8 Mon Sep 17 00:00:00 2001 From: Renato Lui Geh Date: Thu, 4 Mar 2021 14:55:34 -0300 Subject: [PATCH 3/4] Remove prints and sample more vtrees during testing --- test/structured_prob_nodes_tests.jl | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/test/structured_prob_nodes_tests.jl b/test/structured_prob_nodes_tests.jl index e16c1567..daecebff 100644 --- a/test/structured_prob_nodes_tests.jl +++ b/test/structured_prob_nodes_tests.jl @@ -122,20 +122,19 @@ using DataFrames: DataFrame # Convert tests function apply_test_cnf(n_vars::Int, cnf_path::String) - vtree = Vtree(n_vars, :random) - println("Compiling...") - sdd = compile(SddMgr(vtree), zoo_cnf(cnf_path)) - @test num_variables(sdd) == n_vars - println("Converting...") - psdd = convert(StructProbCircuit, sdd) - @test num_variables(psdd) == n_vars - @test issmooth(psdd) - @test isdecomposable(psdd) - @test isdeterministic(psdd) - @test respects_vtree(psdd, vtree) - data = DataFrame(convert(BitMatrix, rand(Bool, 100, n_vars))) - println("Testing data...") - @test all(sdd(data) .== (EVI(psdd, data) .!= -Inf)) + for i in 1:10 + vtree = Vtree(n_vars, :random) + sdd = compile(SddMgr(vtree), zoo_cnf(cnf_path)) + @test num_variables(sdd) == n_vars + psdd = convert(StructProbCircuit, sdd) + @test num_variables(psdd) == n_vars + @test issmooth(psdd) + @test isdecomposable(psdd) + @test isdeterministic(psdd) + @test respects_vtree(psdd, vtree) + data = DataFrame(convert(BitMatrix, rand(Bool, 100, n_vars))) + @test all(sdd(data) .== (EVI(psdd, data) .!= -Inf)) + end nothing end apply_test_cnf(17, "easy/C17_mince.cnf") From 7f2668fd3ffab17a86f3b36bd011cf53f2d1c1f6 Mon Sep 17 00:00:00 2001 From: Renato Lui Geh Date: Fri, 12 Mar 2021 17:09:24 -0300 Subject: [PATCH 4/4] Rename convert to compile --- src/structured_prob_nodes.jl | 2 +- test/structured_prob_nodes_tests.jl | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/structured_prob_nodes.jl b/src/structured_prob_nodes.jl index 209632a2..f20eb74d 100644 --- a/src/structured_prob_nodes.jl +++ b/src/structured_prob_nodes.jl @@ -135,7 +135,7 @@ function compile(::Type{<:StructProbCircuit}, vtree::Vtree, circuit::LogicCircui foldup_aggregate(circuit, f_con, f_lit, f_a, f_o, StructProbCircuit) end -function Base.convert(::Type{<:StructProbCircuit}, sdd::Sdd)::StructProbCircuit +function compile(::Type{<:StructProbCircuit}, sdd::Sdd)::StructProbCircuit lc = LogicCircuit(sdd) plc = propagate_constants(lc, remove_unary=true) structplc = compile(StructLogicCircuit, vtree(sdd), plc) diff --git a/test/structured_prob_nodes_tests.jl b/test/structured_prob_nodes_tests.jl index daecebff..762a7a90 100644 --- a/test/structured_prob_nodes_tests.jl +++ b/test/structured_prob_nodes_tests.jl @@ -126,7 +126,7 @@ using DataFrames: DataFrame vtree = Vtree(n_vars, :random) sdd = compile(SddMgr(vtree), zoo_cnf(cnf_path)) @test num_variables(sdd) == n_vars - psdd = convert(StructProbCircuit, sdd) + psdd = compile(StructProbCircuit, sdd) @test num_variables(psdd) == n_vars @test issmooth(psdd) @test isdecomposable(psdd)