add implied literals

Artifacts.toml

@@ -7,10 +7,10 @@ lazy = true
     sha256 = "5d66a95037e44010502ad28ec8d6dc26f46947dc88e962633b7de54e614b1a47"
 
 [circuit_model_zoo]
-git-tree-sha1 = "49e3a134c68acbcd87075dee811aff997c29cad2"
+git-tree-sha1 = "af581f4a7ca5e29685f8d67843e0120302ead3ab"
 lazy = true
 
  [[circuit_model_zoo.download]]
-    url = "https://github.com/UCLA-StarAI/Circuit-Model-Zoo/archive/v0.1.3.tar.gz"
-    sha256 = "537d4d414b8955e8f9b64e4e3aaf5382889a6901c5e24aa9bc8bc2fbea51dc4f"
+    url = "https://github.com/UCLA-StarAI/Circuit-Model-Zoo/archive/v0.1.4.tar.gz"
+    sha256 = "ec6ea6649364ec0e1305fea3afc3a2dcb3dd40d4d54626e85499a47a07a436b4"
 

src/LoadSave/circuit_loaders.jl

@@ -17,7 +17,7 @@ export zoo_cnf,
 # loaders from model zoo
 #####################
 
-const zoo_version = "/Circuit-Model-Zoo-0.1.3"
+const zoo_version = "/Circuit-Model-Zoo-0.1.4"
 
 zoo_cnf(name) = 
     load_cnf(zoo_cnf_file(name))

src/queries.jl

@@ -6,6 +6,7 @@ export variables_by_node,
     isstruct_decomposable,
     isdeterministic, 
     iscanonical,
+    implied_literals,
     sat_prob, 
     model_count, 
     prob_equiv_signature,
@@ -223,6 +224,48 @@ function isdeterministic(root::LogicCircuit)::Bool
     result
 end
 
+
+"""
+    implied_literals(root::LogicCircuit)::Dict{LogicCircuit, Union{BitSet, Nothing}}
+
+Compute at each node literals that are implied by the formula. 
+nothing at a node means all literals are implied (i.e. the node's formula is false)
+
+This algorithm is sound but not complete - all literals returned are correct, but some true implied literals may be missing. 
+"""
+implied_literals(root::LogicCircuit)::Dict{LogicCircuit, Union{BitSet, Nothing}} =
+    implied_literals_rec(root, Dict{LogicCircuit, Union{BitSet, Nothing}}())
+
+
+function implied_literals_rec(root::LogicCircuit, lcache::Dict{LogicCircuit, Union{BitSet, Nothing}})
+    if isconstantgate(root)
+        if constant(root)
+            # True implies no literals
+            lcache[root] = BitSet()
+        else
+            # False implies any literal, so "full" bitset represented by Nothing
+            lcache[root] = nothing
+        end
+    elseif isliteralgate(root)
+        lcache[root] = BitSet([literal(root)])
+    elseif isinnergate(root)
+        for c in root.children
+            implied_literals_rec(c, lcache)
+        end
+        if is⋀gate(root)
+            # If there's a false in here then this is false too
+            if any(x -> lcache[x] === nothing, root.children)
+                lcache[root] = nothing
+            else
+                lcache[root] = mapreduce(c -> lcache[c], union, root.children)
+            end
+        else
+            # Just filter out any falses, they don't do anything here
+            lcache[root] = mapreduce(c -> lcache[c], intersect, filter(x -> lcache[x] !== nothing, root.children))
+        end
+    end
+    lcache
+end
 #####################
 # structural properties
 #####################

test/queries_test.jl

@@ -4,6 +4,7 @@ using LogicCircuits
 
 include("helper/plain_logic_circuits.jl")
 
+
 @testset "Queries test" begin
 
     r1 = fully_factorized_circuit(PlainLogicCircuit,10)
@@ -117,4 +118,29 @@ end
     @test respects_vtree(random, random_vtree)
     # @test respects_vtree(random, random_inferred) # "issues/#47"
 
-end 
+end
+
+
+@testset "Implied Literals Test" begin
+
+    # Load and compile as a bdd
+    c17 = zoo_cnf("easy/C17_mince.cnf")
+    vtr = PlainVtree(num_variables(c17), :rightlinear)
+    mgr = SddMgr(vtr)
+    circuit = compile(mgr, c17)
+    plc = PlainLogicCircuit(circuit)
+
+    il = implied_literals(plc)
+
+    for ornode in or_nodes(plc)
+        @test num_children(ornode) == 2
+        # If there's a nothing just continue, it'll always work
+        if il[ornode.children[1]] === nothing || il[ornode.children[2]] === nothing
+            continue
+        end
+        implied1 = il[ornode.children[1]]
+        implied2 = il[ornode.children[2]]
+        neg_implied2 = BitSet(map(x -> -x, collect(implied2)))
+        @test !isempty(intersect(implied1, neg_implied2))
+    end
+end