diff --git a/Manifest.toml b/Manifest.toml new file mode 100644 index 0000000..3a7d700 --- /dev/null +++ b/Manifest.toml @@ -0,0 +1,569 @@ +# This file is machine-generated - editing it directly is not advised + +julia_version = "1.11.4" +manifest_format = "2.0" +project_hash = "f9171033e24c2ca9c3bc6c4340453eee9bab475a" + +[[deps.AbstractTrees]] +git-tree-sha1 = "2d9c9a55f9c93e8887ad391fbae72f8ef55e1177" +uuid = "1520ce14-60c1-5f80-bbc7-55ef81b5835c" +version = "0.4.5" + +[[deps.AliasTables]] +deps = ["PtrArrays", "Random"] +git-tree-sha1 = "9876e1e164b144ca45e9e3198d0b689cadfed9ff" +uuid = "66dad0bd-aa9a-41b7-9441-69ab47430ed8" +version = "1.1.3" + +[[deps.ArgCheck]] +git-tree-sha1 = "f9e9a66c9b7be1ad7372bbd9b062d9230c30c5ce" +uuid = "dce04be8-c92d-5529-be00-80e4d2c0e197" +version = "2.5.0" + +[[deps.ArgTools]] +uuid = "0dad84c5-d112-42e6-8d28-ef12dabb789f" +version = "1.1.2" + +[[deps.ArnoldiMethod]] +deps = ["LinearAlgebra", "Random", "StaticArrays"] +git-tree-sha1 = "d57bd3762d308bded22c3b82d033bff85f6195c6" +uuid = "ec485272-7323-5ecc-a04f-4719b315124d" +version = "0.4.0" + +[[deps.Artifacts]] +uuid = "56f22d72-fd6d-98f1-02f0-08ddc0907c33" +version = "1.11.0" + +[[deps.Base64]] +uuid = "2a0f44e3-6c83-55bd-87e4-b1978d98bd5f" +version = "1.11.0" + +[[deps.BatchedRoutines]] +deps = ["LinearAlgebra"] +git-tree-sha1 = "441db9f0399bcfb4eeb8b891a6b03f7acc5dc731" +uuid = "a9ab73d0-e05c-5df1-8fde-d6a4645b8d8e" +version = "0.2.2" + +[[deps.BitBasis]] +deps = ["LinearAlgebra", "StaticArrays"] +git-tree-sha1 = "89dc08420d4f593ff30f02611d136b475a5eb43d" +uuid = "50ba71b6-fa0f-514d-ae9a-0916efc90dcf" +version = "0.9.10" + +[[deps.ChainRulesCore]] +deps = ["Compat", "LinearAlgebra"] +git-tree-sha1 = "1713c74e00545bfe14605d2a2be1712de8fbcb58" +uuid = "d360d2e6-b24c-11e9-a2a3-2a2ae2dbcce4" +version = "1.25.1" +weakdeps = ["SparseArrays"] + + [deps.ChainRulesCore.extensions] + ChainRulesCoreSparseArraysExt = "SparseArrays" + +[[deps.CliqueTrees]] +deps = ["AbstractTrees", "ArgCheck", "DataStructures", "Graphs", "LinearAlgebra", "SparseArrays"] +git-tree-sha1 = "a9da1d6a0921e78157927181c780ce4ea24b1502" +uuid = "60701a23-6482-424a-84db-faee86b9b1f8" +version = "1.6.0" + + [deps.CliqueTrees.extensions] + AMDExt = "AMD" + CatlabExt = "Catlab" + CryptoMiniSat_jllExt = "CryptoMiniSat_jll" + FlowCutterPACE17_jllExt = "FlowCutterPACE17_jll" + LaplaciansExt = "Laplacians" + Lingeling_jllExt = "Lingeling_jll" + MetisExt = "Metis" + PicoSAT_jllExt = "PicoSAT_jll" + TreeWidthSolverExt = "TreeWidthSolver" + libpicosat_jllExt = "libpicosat_jll" + + [deps.CliqueTrees.weakdeps] + AMD = "14f7f29c-3bd6-536c-9a0b-7339e30b5a3e" + Catlab = "134e5e36-593f-5add-ad60-77f754baafbe" + CryptoMiniSat_jll = "cf02a7a8-8cd0-5932-97be-477f95a4d9ce" + FlowCutterPACE17_jll = "008204e2-cd5c-5c6d-9360-d31f32b5f6c2" + Laplacians = "6f8e5838-0efe-5de0-80a3-5fb4f8dbb1de" + Lingeling_jll = "54ea7443-b7cf-5485-b0d0-86c7d7a308e1" + Metis = "2679e427-3c69-5b7f-982b-ece356f1e94b" + PicoSAT_jll = "e78fa76d-a187-569f-aede-ad11521a2edf" + TreeWidthSolver = "7d267fc5-9ace-409f-a54c-cd2374872a55" + libpicosat_jll = "6b231c3b-13f8-5ced-86ae-8860c7f75d86" + +[[deps.Combinatorics]] +git-tree-sha1 = "8010b6bb3388abe68d95743dcbea77650bb2eddf" +uuid = "861a8166-3701-5b0c-9a16-15d98fcdc6aa" +version = "1.0.3" + +[[deps.Compat]] +deps = ["TOML", "UUIDs"] +git-tree-sha1 = "8ae8d32e09f0dcf42a36b90d4e17f5dd2e4c4215" +uuid = "34da2185-b29b-5c13-b0c7-acf172513d20" +version = "4.16.0" +weakdeps = ["Dates", "LinearAlgebra"] + + [deps.Compat.extensions] + CompatLinearAlgebraExt = "LinearAlgebra" + +[[deps.CompilerSupportLibraries_jll]] +deps = ["Artifacts", "Libdl"] +uuid = "e66e0078-7015-5450-92f7-15fbd957f2ae" +version = "1.1.1+0" + +[[deps.Crayons]] +git-tree-sha1 = "249fe38abf76d48563e2f4556bebd215aa317e15" +uuid = "a8cc5b0e-0ffa-5ad4-8c14-923d3ee1735f" +version = "4.1.1" + +[[deps.DataAPI]] +git-tree-sha1 = "abe83f3a2f1b857aac70ef8b269080af17764bbe" +uuid = "9a962f9c-6df0-11e9-0e5d-c546b8b5ee8a" +version = "1.16.0" + +[[deps.DataStructures]] +deps = ["Compat", "InteractiveUtils", "OrderedCollections"] +git-tree-sha1 = "4e1fe97fdaed23e9dc21d4d664bea76b65fc50a0" +uuid = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" +version = "0.18.22" + +[[deps.DataValueInterfaces]] +git-tree-sha1 = "bfc1187b79289637fa0ef6d4436ebdfe6905cbd6" +uuid = "e2d170a0-9d28-54be-80f0-106bbe20a464" +version = "1.0.0" + +[[deps.Dates]] +deps = ["Printf"] +uuid = "ade2ca70-3891-5945-98fb-dc099432e06a" +version = "1.11.0" + +[[deps.Distributed]] +deps = ["Random", "Serialization", "Sockets"] +uuid = "8ba89e20-285c-5b6f-9357-94700520ee1b" +version = "1.11.0" + +[[deps.DocStringExtensions]] +git-tree-sha1 = "e7b7e6f178525d17c720ab9c081e4ef04429f860" +uuid = "ffbed154-4ef7-542d-bbb7-c09d3a79fcae" +version = "0.9.4" + +[[deps.Downloads]] +deps = ["ArgTools", "FileWatching", "LibCURL", "NetworkOptions"] +uuid = "f43a241f-c20a-4ad4-852c-f6b1247861c6" +version = "1.6.0" + +[[deps.FileWatching]] +uuid = "7b1f6079-737a-58dc-b8bc-7a2ca5c1b5ee" +version = "1.11.0" + +[[deps.Graphs]] +deps = ["ArnoldiMethod", "Compat", "DataStructures", "Distributed", "Inflate", "LinearAlgebra", "Random", "SharedArrays", "SimpleTraits", "SparseArrays", "Statistics"] +git-tree-sha1 = "3169fd3440a02f35e549728b0890904cfd4ae58a" +uuid = "86223c79-3864-5bf0-83f7-82e725a168b6" +version = "1.12.1" + +[[deps.Inflate]] +git-tree-sha1 = "d1b1b796e47d94588b3757fe84fbf65a5ec4a80d" +uuid = "d25df0c9-e2be-5dd7-82c8-3ad0b3e990b9" +version = "0.1.5" + +[[deps.InteractiveUtils]] +deps = ["Markdown"] +uuid = "b77e0a4c-d291-57a0-90e8-8db25a27a240" +version = "1.11.0" + +[[deps.IrrationalConstants]] +git-tree-sha1 = "e2222959fbc6c19554dc15174c81bf7bf3aa691c" +uuid = "92d709cd-6900-40b7-9082-c6be49f344b6" +version = "0.2.4" + +[[deps.IteratorInterfaceExtensions]] +git-tree-sha1 = "a3f24677c21f5bbe9d2a714f95dcd58337fb2856" +uuid = "82899510-4779-5014-852e-03e436cf321d" +version = "1.0.0" + +[[deps.JSON]] +deps = ["Dates", "Mmap", "Parsers", "Unicode"] +git-tree-sha1 = "31e996f0a15c7b280ba9f76636b3ff9e2ae58c9a" +uuid = "682c06a0-de6a-54ab-a142-c8b1cf79cde6" +version = "0.21.4" + +[[deps.LaTeXStrings]] +git-tree-sha1 = "dda21b8cbd6a6c40d9d02a73230f9d70fed6918c" +uuid = "b964fa9f-0449-5b57-a5c2-d3ea65f4040f" +version = "1.4.0" + +[[deps.LibCURL]] +deps = ["LibCURL_jll", "MozillaCACerts_jll"] +uuid = "b27032c2-a3e7-50c8-80cd-2d36dbcbfd21" +version = "0.6.4" + +[[deps.LibCURL_jll]] +deps = ["Artifacts", "LibSSH2_jll", "Libdl", "MbedTLS_jll", "Zlib_jll", "nghttp2_jll"] +uuid = "deac9b47-8bc7-5906-a0fe-35ac56dc84c0" +version = "8.6.0+0" + +[[deps.LibGit2]] +deps = ["Base64", "LibGit2_jll", "NetworkOptions", "Printf", "SHA"] +uuid = "76f85450-5226-5b5a-8eaa-529ad045b433" +version = "1.11.0" + +[[deps.LibGit2_jll]] +deps = ["Artifacts", "LibSSH2_jll", "Libdl", "MbedTLS_jll"] +uuid = "e37daf67-58a4-590a-8e99-b0245dd2ffc5" +version = "1.7.2+0" + +[[deps.LibSSH2_jll]] +deps = ["Artifacts", "Libdl", "MbedTLS_jll"] +uuid = "29816b5a-b9ab-546f-933c-edad1886dfa8" +version = "1.11.0+1" + +[[deps.Libdl]] +uuid = "8f399da3-3557-5675-b5ff-fb832c97cbdb" +version = "1.11.0" + +[[deps.LinearAlgebra]] +deps = ["Libdl", "OpenBLAS_jll", "libblastrampoline_jll"] +uuid = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" +version = "1.11.0" + +[[deps.LogExpFunctions]] +deps = ["DocStringExtensions", "IrrationalConstants", "LinearAlgebra"] +git-tree-sha1 = "13ca9e2586b89836fd20cccf56e57e2b9ae7f38f" +uuid = "2ab3a3ac-af41-5b50-aa03-7779005ae688" +version = "0.3.29" + + [deps.LogExpFunctions.extensions] + LogExpFunctionsChainRulesCoreExt = "ChainRulesCore" + LogExpFunctionsChangesOfVariablesExt = "ChangesOfVariables" + LogExpFunctionsInverseFunctionsExt = "InverseFunctions" + + [deps.LogExpFunctions.weakdeps] + ChainRulesCore = "d360d2e6-b24c-11e9-a2a3-2a2ae2dbcce4" + ChangesOfVariables = "9e997f8a-9a97-42d5-a9f1-ce6bfc15e2c0" + InverseFunctions = "3587e190-3f89-42d0-90ee-14403ec27112" + +[[deps.Logging]] +uuid = "56ddb016-857b-54e1-b83d-db4d58db5568" +version = "1.11.0" + +[[deps.MLStyle]] +git-tree-sha1 = "bc38dff0548128765760c79eb7388a4b37fae2c8" +uuid = "d8e11817-5142-5d16-987a-aa16d5891078" +version = "0.4.17" + +[[deps.MacroTools]] +git-tree-sha1 = "1e0228a030642014fe5cfe68c2c0a818f9e3f522" +uuid = "1914dd2f-81c6-5fcd-8719-6d5c9610ff09" +version = "0.5.16" + +[[deps.Markdown]] +deps = ["Base64"] +uuid = "d6f4376e-aef5-505a-96c1-9c027394607a" +version = "1.11.0" + +[[deps.MbedTLS_jll]] +deps = ["Artifacts", "Libdl"] +uuid = "c8ffd9c3-330d-5841-b78e-0817d7145fa1" +version = "2.28.6+0" + +[[deps.Missings]] +deps = ["DataAPI"] +git-tree-sha1 = "ec4f7fbeab05d7747bdf98eb74d130a2a2ed298d" +uuid = "e1d29d7a-bbdc-5cf2-9ac0-f12de2c33e28" +version = "1.2.0" + +[[deps.Mmap]] +uuid = "a63ad114-7e13-5084-954f-fe012c677804" +version = "1.11.0" + +[[deps.MozillaCACerts_jll]] +uuid = "14a3606d-f60d-562e-9121-12d972cd8159" +version = "2023.12.12" + +[[deps.NetworkOptions]] +uuid = "ca575930-c2e3-43a9-ace4-1e988b2c1908" +version = "1.2.0" + +[[deps.OMEinsum]] +deps = ["AbstractTrees", "BatchedRoutines", "ChainRulesCore", "Combinatorics", "LinearAlgebra", "MacroTools", "OMEinsumContractionOrders", "Test", "TupleTools"] +git-tree-sha1 = "b7e74469451c25d391381b874841480cd26edc7b" +uuid = "ebe7aa44-baf0-506c-a96f-8464559b3922" +version = "0.8.7" + + [deps.OMEinsum.extensions] + AMDGPUExt = "AMDGPU" + CUDAExt = "CUDA" + + [deps.OMEinsum.weakdeps] + AMDGPU = "21141c5a-9bdb-4563-92ae-f87d6854732e" + CUDA = "052768ef-5323-5732-b1bb-66c8b64840ba" + +[[deps.OMEinsumContractionOrders]] +deps = ["AbstractTrees", "CliqueTrees", "DataStructures", "JSON", "SparseArrays", "StatsBase", "Suppressor", "TreeWidthSolver"] +git-tree-sha1 = "57ef6d6e8fcd5d0066c0e711c242963982c9d718" +uuid = "6f22d1fd-8eed-4bb7-9776-e7d684900715" +version = "0.9.9" + + [deps.OMEinsumContractionOrders.extensions] + KaHyParExt = ["KaHyPar"] + LuxorTensorPlot = ["LuxorGraphPlot"] + + [deps.OMEinsumContractionOrders.weakdeps] + KaHyPar = "2a6221f6-aa48-11e9-3542-2d9e0ef01880" + LuxorGraphPlot = "1f49bdf2-22a7-4bc4-978b-948dc219fbbc" + +[[deps.OpenBLAS_jll]] +deps = ["Artifacts", "CompilerSupportLibraries_jll", "Libdl"] +uuid = "4536629a-c528-5b80-bd46-f80d51c5b363" +version = "0.3.27+1" + +[[deps.OrderedCollections]] +git-tree-sha1 = "05868e21324cede2207c6f0f466b4bfef6d5e7ee" +uuid = "bac558e1-5e72-5ebc-8fee-abe8a469f55d" +version = "1.8.1" + +[[deps.Parsers]] +deps = ["Dates", "PrecompileTools", "UUIDs"] +git-tree-sha1 = "7d2f8f21da5db6a806faf7b9b292296da42b2810" +uuid = "69de0a69-1ddd-5017-9359-2bf0b02dc9f0" +version = "2.8.3" + +[[deps.Pkg]] +deps = ["Artifacts", "Dates", "Downloads", "FileWatching", "LibGit2", "Libdl", "Logging", "Markdown", "Printf", "Random", "SHA", "TOML", "Tar", "UUIDs", "p7zip_jll"] +uuid = "44cfe95a-1eb2-52ea-b672-e2afdf69b78f" +version = "1.11.0" + + [deps.Pkg.extensions] + REPLExt = "REPL" + + [deps.Pkg.weakdeps] + REPL = "3fa0cd96-eef1-5676-8a61-b3b8758bbffb" + +[[deps.PrecompileTools]] +deps = ["Preferences"] +git-tree-sha1 = "5aa36f7049a63a1528fe8f7c3f2113413ffd4e1f" +uuid = "aea7be01-6a6a-4083-8856-8a6e6704d82a" +version = "1.2.1" + +[[deps.Preferences]] +deps = ["TOML"] +git-tree-sha1 = "9306f6085165d270f7e3db02af26a400d580f5c6" +uuid = "21216c6a-2e73-6563-6e65-726566657250" +version = "1.4.3" + +[[deps.PrettyTables]] +deps = ["Crayons", "LaTeXStrings", "Markdown", "PrecompileTools", "Printf", "Reexport", "StringManipulation", "Tables"] +git-tree-sha1 = "1101cd475833706e4d0e7b122218257178f48f34" +uuid = "08abe8d2-0d0c-5749-adfa-8a2ac140af0d" +version = "2.4.0" + +[[deps.Printf]] +deps = ["Unicode"] +uuid = "de0858da-6303-5e67-8744-51eddeeeb8d7" +version = "1.11.0" + +[[deps.ProblemReductions]] +deps = ["BitBasis", "DocStringExtensions", "Graphs", "InteractiveUtils", "LinearAlgebra", "MLStyle", "PrettyTables"] +git-tree-sha1 = "28aa2de76a630b3fe57bd261bb1fdaf9105b6a48" +uuid = "899c297d-f7d2-4ebf-8815-a35996def416" +version = "0.3.4" + + [deps.ProblemReductions.extensions] + IPSolverExt = "JuMP" + + [deps.ProblemReductions.weakdeps] + JuMP = "4076af6c-e467-56ae-b986-b466b2749572" + +[[deps.PtrArrays]] +git-tree-sha1 = "1d36ef11a9aaf1e8b74dacc6a731dd1de8fd493d" +uuid = "43287f4e-b6f4-7ad1-bb20-aadabca52c3d" +version = "1.3.0" + +[[deps.Random]] +deps = ["SHA"] +uuid = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" +version = "1.11.0" + +[[deps.Reexport]] +git-tree-sha1 = "45e428421666073eab6f2da5c9d310d99bb12f9b" +uuid = "189a3867-3050-52da-a836-e630ba90ab69" +version = "1.2.2" + +[[deps.SHA]] +uuid = "ea8e919c-243c-51af-8825-aaa63cd721ce" +version = "0.7.0" + +[[deps.Serialization]] +uuid = "9e88b42a-f829-5b0c-bbe9-9e923198166b" +version = "1.11.0" + +[[deps.SharedArrays]] +deps = ["Distributed", "Mmap", "Random", "Serialization"] +uuid = "1a1011a3-84de-559e-8e89-a11a2f7dc383" +version = "1.11.0" + +[[deps.SimpleTraits]] +deps = ["InteractiveUtils", "MacroTools"] +git-tree-sha1 = "5d7e3f4e11935503d3ecaf7186eac40602e7d231" +uuid = "699a6c99-e7fa-54fc-8d76-47d257e15c1d" +version = "0.9.4" + +[[deps.SimpleWeightedGraphs]] +deps = ["Graphs", "LinearAlgebra", "Markdown", "SparseArrays"] +git-tree-sha1 = "3e5f165e58b18204aed03158664c4982d691f454" +uuid = "47aef6b3-ad0c-573a-a1e2-d07658019622" +version = "1.5.0" + +[[deps.Sockets]] +uuid = "6462fe0b-24de-5631-8697-dd941f90decc" +version = "1.11.0" + +[[deps.SortingAlgorithms]] +deps = ["DataStructures"] +git-tree-sha1 = "66e0a8e672a0bdfca2c3f5937efb8538b9ddc085" +uuid = "a2af1166-a08f-5f64-846c-94a0d3cef48c" +version = "1.2.1" + +[[deps.SparseArrays]] +deps = ["Libdl", "LinearAlgebra", "Random", "Serialization", "SuiteSparse_jll"] +uuid = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" +version = "1.11.0" + +[[deps.StaticArrays]] +deps = ["LinearAlgebra", "PrecompileTools", "Random", "StaticArraysCore"] +git-tree-sha1 = "0feb6b9031bd5c51f9072393eb5ab3efd31bf9e4" +uuid = "90137ffa-7385-5640-81b9-e52037218182" +version = "1.9.13" +weakdeps = ["ChainRulesCore", "Statistics"] + + [deps.StaticArrays.extensions] + StaticArraysChainRulesCoreExt = "ChainRulesCore" + StaticArraysStatisticsExt = "Statistics" + +[[deps.StaticArraysCore]] +git-tree-sha1 = "192954ef1208c7019899fbf8049e717f92959682" +uuid = "1e83bf80-4336-4d27-bf5d-d5a4f845583c" +version = "1.4.3" + +[[deps.Statistics]] +deps = ["LinearAlgebra"] +git-tree-sha1 = "ae3bb1eb3bba077cd276bc5cfc337cc65c3075c0" +uuid = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" +version = "1.11.1" +weakdeps = ["SparseArrays"] + + [deps.Statistics.extensions] + SparseArraysExt = ["SparseArrays"] + +[[deps.StatsAPI]] +deps = ["LinearAlgebra"] +git-tree-sha1 = "9d72a13a3f4dd3795a195ac5a44d7d6ff5f552ff" +uuid = "82ae8749-77ed-4fe6-ae5f-f523153014b0" +version = "1.7.1" + +[[deps.StatsBase]] +deps = ["AliasTables", "DataAPI", "DataStructures", "LinearAlgebra", "LogExpFunctions", "Missings", "Printf", "Random", "SortingAlgorithms", "SparseArrays", "Statistics", "StatsAPI"] +git-tree-sha1 = "b81c5035922cc89c2d9523afc6c54be512411466" +uuid = "2913bbd2-ae8a-5f71-8c99-4fb6c76f3a91" +version = "0.34.5" + +[[deps.StringManipulation]] +deps = ["PrecompileTools"] +git-tree-sha1 = "725421ae8e530ec29bcbdddbe91ff8053421d023" +uuid = "892a3eda-7b42-436c-8928-eab12a02cf0e" +version = "0.4.1" + +[[deps.SuiteSparse_jll]] +deps = ["Artifacts", "Libdl", "libblastrampoline_jll"] +uuid = "bea87d4a-7f5b-5778-9afe-8cc45184846c" +version = "7.7.0+0" + +[[deps.Suppressor]] +deps = ["Logging"] +git-tree-sha1 = "6dbb5b635c5437c68c28c2ac9e39b87138f37c0a" +uuid = "fd094767-a336-5f1f-9728-57cf17d0bbfb" +version = "0.2.8" + +[[deps.TOML]] +deps = ["Dates"] +uuid = "fa267f1f-6049-4f14-aa54-33bafae1ed76" +version = "1.0.3" + +[[deps.TableTraits]] +deps = ["IteratorInterfaceExtensions"] +git-tree-sha1 = "c06b2f539df1c6efa794486abfb6ed2022561a39" +uuid = "3783bdb8-4a98-5b6b-af9a-565f29a5fe9c" +version = "1.0.1" + +[[deps.Tables]] +deps = ["DataAPI", "DataValueInterfaces", "IteratorInterfaceExtensions", "OrderedCollections", "TableTraits"] +git-tree-sha1 = "f2c1efbc8f3a609aadf318094f8fc5204bdaf344" +uuid = "bd369af6-aec1-5ad0-b16a-f7cc5008161c" +version = "1.12.1" + +[[deps.Tar]] +deps = ["ArgTools", "SHA"] +uuid = "a4e569a6-e804-4fa4-b0f3-eef7a1d5b13e" +version = "1.10.0" + +[[deps.TensorInference]] +deps = ["DocStringExtensions", "LinearAlgebra", "OMEinsum", "Pkg", "PrettyTables", "ProblemReductions", "StatsBase", "TropicalNumbers"] +path = "/Users/cycling/.julia/dev/TensorInference" +uuid = "c2297e78-99bd-40ad-871d-f50e56b81012" +version = "0.6.0" + + [deps.TensorInference.extensions] + TensorInferenceCUDAExt = "CUDA" + + [deps.TensorInference.weakdeps] + CUDA = "052768ef-5323-5732-b1bb-66c8b64840ba" + +[[deps.Test]] +deps = ["InteractiveUtils", "Logging", "Random", "Serialization"] +uuid = "8dfed614-e22c-5e08-85e1-65c5234f0b40" +version = "1.11.0" + +[[deps.TreeWidthSolver]] +deps = ["AbstractTrees", "BitBasis", "Combinatorics", "Graphs", "SparseArrays"] +git-tree-sha1 = "6738f4a82bba556df9c42aed0f8642ea7344033a" +uuid = "7d267fc5-9ace-409f-a54c-cd2374872a55" +version = "0.3.5" + +[[deps.TropicalNumbers]] +git-tree-sha1 = "eb28dda1f26cc30602b2df170119efa94c9d28c6" +uuid = "b3a74e9c-7526-4576-a4eb-79c0d4c32334" +version = "0.6.3" + +[[deps.TupleTools]] +git-tree-sha1 = "41e43b9dc950775eac654b9f845c839cd2f1821e" +uuid = "9d95972d-f1c8-5527-a6e0-b4b365fa01f6" +version = "1.6.0" + +[[deps.UUIDs]] +deps = ["Random", "SHA"] +uuid = "cf7118a7-6976-5b1a-9a39-7adc72f591a4" +version = "1.11.0" + +[[deps.Unicode]] +uuid = "4ec0a83e-493e-50e2-b9ac-8f72acf5a8f5" +version = "1.11.0" + +[[deps.Zlib_jll]] +deps = ["Libdl"] +uuid = "83775a58-1f1d-513f-b197-d71354ab007a" +version = "1.2.13+1" + +[[deps.libblastrampoline_jll]] +deps = ["Artifacts", "Libdl"] +uuid = "8e850b90-86db-534c-a0d3-1478176c7d93" +version = "5.11.0+0" + +[[deps.nghttp2_jll]] +deps = ["Artifacts", "Libdl"] +uuid = "8e850ede-7688-5339-a07c-302acd2aaf8d" +version = "1.59.0+0" + +[[deps.p7zip_jll]] +deps = ["Artifacts", "Libdl"] +uuid = "3f19e933-33d8-53b3-aaab-bd5110c3b7a0" +version = "17.4.0+2" diff --git a/Project.toml b/Project.toml new file mode 100644 index 0000000..6c8c0a2 --- /dev/null +++ b/Project.toml @@ -0,0 +1,5 @@ +[deps] +Graphs = "86223c79-3864-5bf0-83f7-82e725a168b6" +SimpleWeightedGraphs = "47aef6b3-ad0c-573a-a1e2-d07658019622" +SparseArrays = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" +TensorInference = "c2297e78-99bd-40ad-871d-f50e56b81012" diff --git a/hw1/zhaohui_zhi/solution_916.jl b/hw1/zhaohui_zhi/solution_916.jl new file mode 100644 index 0000000..e69de29 diff --git a/hw1/zhaohui_zhi/solution_96.jl b/hw1/zhaohui_zhi/solution_96.jl new file mode 100644 index 0000000..e69de29 diff --git a/hw1/zhaohui_zhi/solution_97.jl b/hw1/zhaohui_zhi/solution_97.jl new file mode 100644 index 0000000..e69de29 diff --git a/hw3/zhaohui_zhi/DPLL.jl b/hw3/zhaohui_zhi/DPLL.jl new file mode 100644 index 0000000..064a32f --- /dev/null +++ b/hw3/zhaohui_zhi/DPLL.jl @@ -0,0 +1,233 @@ +# Only used for Conjunctive Normal Form (CNF) +# Do not consider Empty clauses input, but empty clause is valid, which we will add in later version. And if we focus on K-SAT problem, which has the same length clauses. +struct SATformula + clauses::Vector{Vector{Int}} + num_vars::Int + num_clauses::Int +end + +struct SATsolution + solutions::Vector{Symbol} + num_vars::Int + clauses::Vector{Vector{Int}} # Store the clauses for reference +end + +# function SATformula(clauses::Vector{Vector{Int}})::SATformula +# num_vars = maximum(abs.(reduce(vcat, clauses))) +# num_clauses = length(clauses) +# return SATformula(clauses, num_vars, num_clauses) +# end + +Base.:(==)(s1::SATformula, s2::SATformula) = s1.clauses == s2.clauses && s1.num_vars == s2.num_vars && s1.num_clauses== s2.num_clauses +Base.:(==)(s1::SATsolution, s2::SATsolution) = s1.solutions == s2.solutions && s1.num_vars == s2.num_vars && s1.clauses == s2.clauses + +function SATformula(clauses::Vector{T})::SATformula where T + if isempty(clauses) + return SATformula(clauses, 0, 0) + end + non_empty_clauses = filter(!isempty, clauses) + if isempty(non_empty_clauses) + num_vars = 0 + else + num_vars = maximum(abs.(reduce(vcat, non_empty_clauses))) + end + num_clauses = length(clauses) + return SATformula(clauses, num_vars, num_clauses) +end + +function SATsolution(solutions::Vector{Symbol},formula::SATformula)::SATsolution + if length(solutions) != formula.num_vars + throw(ArgumentError("Solutions length must match number of variables.")) + end + clauses = formula.clauses + num_vars = formula.num_vars + return SATsolution(solutions, num_vars, clauses) +end + +function is_unit_clause(clause::Vector{Int}, assignment::Vector{Symbol}) + unassigned_count = 0 + satisfied = false + + for literal in clause + var = abs(literal) + if var > length(assignment) + throw(ArgumentError("Clause contains literal $var beyond assignment length $(length(assignment))")) + end + value = assignment[var] + + # 检查子句是否已经被满足 + if (literal > 0 && value === :t) || (literal < 0 && value === :f) + satisfied = true + break + elseif value == :u + unassigned_count += 1 + end + end + + return !satisfied && unassigned_count == 1 +end + +function is_satisfied(clause::Vector{Int64}, assignment::Vector{Symbol}) + # once one literal is true, thus clause is satisfied + @assert length(clause) <= length(assignment) "Clause length exceeds assignment length, thus undefinite." + if isempty(clause) + return true + end + for literal in clause + if literal > 0 && assignment[literal] == :t + return true + elseif literal < 0 && assignment[-literal] == :f + return true + end + end + return false +end + +function is_satisfied_all(clauses::SATformula, assignment::SATsolution) + clauses_set= clauses.clauses + solution = assignment.solutions + for clause in clauses_set + if !is_satisfied(clause, solution) + return false + end + end + return true +end + +function conflict(clauses::SATformula, assignment::SATsolution) +# check if there is any conflict in the clauses with the current all assigned assignment + clauses_set = clauses.clauses + solution = assignment.solutions + + for clause in clauses_set + if is_clause_conflicted(clause, solution) + return true + end + end + return false +end + +function is_clause_conflicted(clause::Vector{Int}, assignment::Vector{Symbol}) + # check if a single clause is conflicted with the current assignment + # A clause is conflicted if all its literals are assigned and none of them satisfy the clause. + if isempty(clause) + return true # An empty clause is considered conflicted. + end + + all_assigned = true + clause_satisfied = false + + for literal in clause + var = abs(literal) + value = assignment[var] + + if value == :u + all_assigned = false # unassigned literal found + elseif (literal > 0 && value == :t) || (literal < 0 && value == :f) + clause_satisfied = true # clause is satisfied by this literal + break + end + end + + # Only when all literals are assigned and none satisfy the clause, it is conflicted. + return all_assigned && !clause_satisfied +end + +function unit_propagate(clauses::SATformula, assignment::SATsolution) + # return unsolved clauses and updated assignment after unit propagation + clauses_set = clauses.clauses + solution = assignment.solutions + while true + unit_clauses = filter(x -> is_unit_clause(x, solution), clauses_set) + if isempty(unit_clauses) + break + end + for unit_clause in unit_clauses + for literal in unit_clause + if solution[abs(literal)] == :u + # If the variable is unassigned, assign it based on the unit clause. + if literal > 0 + solution[literal] = :t + else + solution[-literal] = :f + end + end + end + clauses_set = filter(c -> !is_satisfied(c, solution), clauses_set) + + end + end + return SATformula(clauses_set), SATsolution(solution, clauses) +end + +function choose_literal(clauses::SATformula, assignment::SATsolution) + # Choose the next unassigned variable. + clauses_set = clauses.clauses + solution = assignment.solutions + idx = findfirst(x -> x == :u, solution) + return idx +end + +function dpll(clauses::SATformula, assignment::SATsolution) # initial default assignment is :u + # solution = fill(:u, clauses.num_vars) + # assignment = SATsolution(solution, clauses) + unsolved_clauses, assignment = unit_propagate(clauses, assignment) + + if any(isempty, clauses.clauses) && !isempty(clauses.clauses) + return false, assignment + end + + if is_satisfied_all(clauses, assignment) + return true, assignment + elseif conflict(clauses, assignment) + return false, assignment + else + literal = choose_literal(clauses, assignment) + + assignment_true = deepcopy(assignment) + assignment_true.solutions[literal] = :t + result, solution = dpll(clauses, assignment_true) + if result + return true, solution + end + + assignment_false = deepcopy(assignment) + assignment_false.solutions[literal] = :f + + return dpll(clauses, assignment_false) + end +end + +# function solve_sat(formula::SATformula) +# assignment = fill(:u, formula.num_vars) +# result = dpll(formula.clauses, assignment) +# if result == true +# return SATsolution(formula.clauses, formula.num_vars) +# else +# return :u +# end +# end + +# function print_solution(solution::SATsolution) +# if solution == :u +# println("No solution found.") +# else +# println("Solution found:") +# for i in 1:solution.num_vars +# if solution.clauses[i] == true +# println("Variable $i: true") +# elseif solution.clauses[i] == false +# println("Variable $i: false") +# else +# println("Variable $i: undefined") +# end +# end +# end +# end +# function main() +# clauses = [[1, -2], [-1, 2], [2, 3], [-3]] +# formula = SATformula(clauses) +# solution = solve_sat(formula) +# print_solution(solution) +# end +# main() \ No newline at end of file diff --git a/hw3/zhaohui_zhi/SetPartition.jl b/hw3/zhaohui_zhi/SetPartition.jl new file mode 100644 index 0000000..fb5e971 --- /dev/null +++ b/hw3/zhaohui_zhi/SetPartition.jl @@ -0,0 +1,29 @@ +function balanced_partition_possible(S) + total = sum(S) + target = total ÷ 2 # 整除操作 + dp = falses(target + 1) # 初始化布尔数组（默认false） + dp[1] = true # dp[1]表示和为0（索引1对应和0） + + for num in S + # 反向遍历，避免重复计算 + for i in target:-1:num + if dp[i - num + 1] # 检查是否可以通过i-num的和得到当前和i + dp[i + 1] = true + end + end + end + + # 寻找最大的可达和 + for i in target:-1:0 + if dp[i + 1] + return abs(total - 2i) ≤ 1 + end + end + return false +end + +# 测试样例 +println(balanced_partition_possible([1, 2, 3])) # true（差0） +println(balanced_partition_possible([1, 3, 5])) # true（差1） +println(balanced_partition_possible([2, 4, 6])) # true（差0） +println(balanced_partition_possible([10])) # false（无法分割） \ No newline at end of file diff --git a/hw3/zhaohui_zhi/hw.jl b/hw3/zhaohui_zhi/hw.jl new file mode 100644 index 0000000..e69de29 diff --git a/hw3/zhaohui_zhi/test_DPLL.jl b/hw3/zhaohui_zhi/test_DPLL.jl new file mode 100644 index 0000000..11bf751 --- /dev/null +++ b/hw3/zhaohui_zhi/test_DPLL.jl @@ -0,0 +1,155 @@ +using Test +include("DPLL.jl") + +@testset "is_satisfied" begin + # Test case 1: Clause satisfied by positive literal + # :t is true, :f is false, :u is undetermined + clause1 = [1, -2] + assignment1 = [:t, :f] + @test is_satisfied(clause1, assignment1) == true + + # Test case 2: Clause satisfied by negative literal + clause2 = [1, -2] + assignment2 = [:t, :t] + @test is_satisfied(clause2, assignment2) == true + + # Test case 3: Clause not satisfied + clause3 = [1, -2] + assignment3 = [:f, :t] + @test is_satisfied(clause3, assignment3) == false + + # Test case 4: Empty clause (should be satisfied) + clause4 = [] + assignment4 = [:t, :f] + @test_broken is_satisfied(clause4, assignment4) == true + + # Test case 5: Clause with clause has no common length with assignment + clause5 = [-1, -2] + assignment5 = [:f, :f, :f] + @test is_satisfied(clause5, assignment5) == true + + # # Test case 6: Clause with clause has additional literal beyond assignment + # clause6 = [1, -2, 3] + # assignment6 = [:t, :f] + # @test_throws ArgumentError is_satisfied(clause6, assignment6) + + # Test case 7: Clause with clause has additional literal beyond assignment + clause7 = [1, -2, 3] + assignment7 = [:t, :f, :u] + @test is_satisfied(clause7, assignment7) == true + + # Test case 8: Clause with clause has additional literal beyond assignment + clause8 = [1, -2, 3] + assignment8 = [:f, :t, :u] + @test is_satisfied(clause8, assignment8) == false +end + +@testset "is_satisfied_all" begin + # Test case 1: All clauses satisfied + clauses1 = SATformula([[1, -2], [-1, 2]]) + assignment1 = SATsolution([:t, :f], clauses1) + @test is_satisfied_all(clauses1, assignment1) == false + + # Test case 2: Not all clauses satisfied + clauses2 = SATformula([[-1, -2, 3], [-3, 4]]) + assignment2 = SATsolution([:t, :t, :t, :t], clauses2) + @test is_satisfied_all(clauses2, assignment2) == true + + # Test case 3: Empty clauses (should be satisfied) + # clauses3 = SATformula([]) + # assignment3 = [:t, :f] + # @test is_satisfied_all(clauses3, assignment3) == true +end + +@testset "is_unit_clause" begin + clause = [1, -2, 3] + assignment = [:f, :u, :f] + # Test case 1: Unit clause + @test is_unit_clause(clause, assignment) == true + # Test case 2: Not a unit clause + @test is_unit_clause(clause, [:f, :t, :f]) == false + # Test case 3: Empty clause (should not be considered a unit clause) + @test is_unit_clause([2], assignment) == true +end + +@testset "unit_propagate" begin + # Test case 1: Simple unit propagation + clauses1 = SATformula([[1, -2, 3], [-1, 2], [2]]) + assignment1 = SATsolution([:u, :u, :u], clauses1) + new_clauses1, new_assignment1 = unit_propagate(clauses1, assignment1) + @test new_assignment1 == SATsolution([:u, :t, :u], clauses1) + @test new_clauses1 == SATformula([[1, -2, 3]]) + + # Test case 2: No unit clauses + clauses2 = SATformula([[1, -2], [-3]]) + assignment2 = SATsolution([:u, :u, :u], clauses2) + new_clauses2, new_assignment2 = unit_propagate(clauses2, assignment2) + @test new_assignment2 == SATsolution([:u, :u, :f], clauses2) + @test new_clauses2 == SATformula([[1, -2]]) + + # # Test case 3: Empty clauses + # clauses3 = SATformula([]) + # assignment3 = SATsolution([:u], clauses3) + # new_clauses3, new_assignment3 = unit_propagate(clauses3, assignment3) + # @test new_assignment3 == [:u] + # @test new_clauses3 == [] + # Test case 4: All clauses satisfied + clauses = SATformula([[-2, -3, -4, 5], [-1, -5, 6], [-5, 7], [-1, -6, -7], [-1, -2, 5], [-1, -3, 5], [-1, -4, 5], [-1, 2, 3, 4, 5, -6]]) + assignment = SATsolution([:t, :t, :u, :u, :u, :u, :u],clauses) + unsolved_clauses, assignment = unit_propagate(clauses, assignment) + @test assignment.solutions == [:t, :t, :u, :u, :t, :t, :t] + @test unsolved_clauses.clauses == [[-1, -6, -7]] +end + +@testset "conflict" begin + @test is_clause_conflicted([1, -2], [:t, :f]) == false + @test is_clause_conflicted([1, -2], [:f, :t]) == true + @test is_clause_conflicted([1, -2], [:f, :f]) == false + + clauses = SATformula([[1, -2], [-1, 2]]) + assignment = SATsolution([:t, :f], clauses) + @test conflict(clauses, assignment) == true +end + +@testset "choose_literal" begin + # Test case 1: Choose a literal from a simple clause + clauses1 = SATformula([[1, -2, 3]]) + assignment1 = SATsolution([:u, :u, :u], clauses1) + literal1 = choose_literal(clauses1, assignment1) + @test literal1 == 1 +end + + +# Test cases for DPLL algorithm +@testset "DPLL Tests" begin + # Test case 1: Simple satisfiable formula + clauses1 = SATformula([[-2, -3, -4, 5], [-1, -5, 6], [-5, 7], [-1, -6, -7], [-1, -2, 5], [-1, -3, 5], [-1, -4, 5], [-1, 2, 3, 4, 5, -6]]) + assignment1 = SATsolution(fill(:u, 7), clauses1) + result1 = dpll(clauses1, assignment1) + @test result1[2].solutions == [:t, :f, :f, :f, :f, :f, :u] + + # Test case 2: Simple unsatisfiable formula + clauses2 = SATformula([[1, -2], [-1, 2], [2, -3]]) + assignment2 = SATsolution(fill(:u, 3), clauses2) + result2 = dpll(clauses2, assignment2) + @test result2[2].solutions == [:t,:t,:u] + + # Test case 3: More complex satisfiable formula + clauses3 = SATformula([[1, 2], [-1, -3], [3]]) + assignment3 = SATsolution(fill(:u, 3), clauses3) + result3 = dpll(clauses3, assignment3) + @test result3[2].solutions == [:f,:t,:t] + + # Test case 4: Empty clause (unsatisfiable) + formula4 = SATformula([[1, -2], [-1, 2], []]) + assignment4 = SATsolution(fill(:u, 2), formula4) + result4 = dpll(formula4, assignment4) + @test result4[1] == false + + # Test case 5: All variables are true + formula5 = SATformula([[1], [2], [3]]) + assignment5 = SATsolution(fill(:u, 3), formula5) + result5 = dpll(formula5, assignment5) + @test result5[2].solutions == [:t,:t,:t] + +end \ No newline at end of file diff --git a/hw5/zhaohui_zhi/BP.jl b/hw5/zhaohui_zhi/BP.jl new file mode 100644 index 0000000..8224184 --- /dev/null +++ b/hw5/zhaohui_zhi/BP.jl @@ -0,0 +1,397 @@ +using Random +using Statistics +using Graphs +using LinearAlgebra + +struct SATformula + clauses::Vector{Vector{Int}} + num_vars::Int + num_clauses::Int +end + +struct SATsolution + solutions::Vector{Symbol} + num_vars::Int + clauses::Vector{Vector{Int}} # Store the clauses for reference +end + +# function SATformula(clauses::Vector{Vector{Int}})::SATformula +# num_vars = maximum(abs.(reduce(vcat, clauses))) +# num_clauses = length(clauses) +# return SATformula(clauses, num_vars, num_clauses) +# end + +Base.:(==)(s1::SATformula, s2::SATformula) = s1.clauses == s2.clauses && s1.num_vars == s2.num_vars && s1.num_clauses== s2.num_clauses +Base.:(==)(s1::SATsolution, s2::SATsolution) = s1.solutions == s2.solutions && s1.num_vars == s2.num_vars && s1.clauses == s2.clauses + +function SATformula(clauses::Vector{T})::SATformula where T + if isempty(clauses) + return SATformula(clauses, 0, 0) + end + non_empty_clauses = filter(!isempty, clauses) + if isempty(non_empty_clauses) + num_vars = 0 + else + num_vars = maximum(abs.(reduce(vcat, non_empty_clauses))) + end + num_clauses = length(clauses) + return SATformula(clauses, num_vars, num_clauses) +end + +function SATsolution(solutions::Vector{Symbol},formula::SATformula)::SATsolution + if length(solutions) != formula.num_vars + throw(ArgumentError("Solutions length must match number of variables.")) + end + clauses = formula.clauses + num_vars = formula.num_vars + return SATsolution(solutions, num_vars, clauses) +end + +# factor graph, the first num_vars are the variables (the indices), the rest are the factors (the tensors) +struct FactorGraph{T} + g::SimpleGraph{T} + num_vars::Int + edge_types::Dict{Tuple{Int, Int}, Int} # Edge types: -1 for original variable edges, 1 for negated variable edges + function FactorGraph(g::SimpleGraph{T}, num_vars::Int, edge_types::Dict{Tuple{Int, Int},Int}) where T + for e in edges(g) + s, d = src(e), dst(e) + # neighbor of a variable is a factor, and vice versa + @assert ((s ≤ num_vars) && (d > num_vars)) || ((s > num_vars) && (d ≤ num_vars)) + end + new{T}(g, num_vars, edge_types) + end +end + +Base.show(io::IO, fg::FactorGraph) = print(io, "FactorGraph{variables: $(fg.num_vars), factors: $(nv(fg.g) - fg.num_vars)}") +Base.copy(fg::FactorGraph) = FactorGraph(copy(fg.g), fg.num_vars, fg.edge_types) + +Graphs.edges(fg::FactorGraph) = edges(fg.g) +Graphs.vertices(fg::FactorGraph) = vertices(fg.g) +Graphs.nv(fg::FactorGraph) = nv(fg.g) +Graphs.ne(fg::FactorGraph) = ne(fg.g) +Graphs.has_edge(fg::FactorGraph, s, d) = has_edge(fg.g, s, d) +Graphs.has_vertex(fg::FactorGraph, v) = has_vertex(fg.g, v) +Graphs.rem_edge!(fg::FactorGraph, s, d) = rem_edge!(fg.g, s, d) +Graphs.rem_vertex!(fg::FactorGraph, v) = rem_vertex!(fg.g, v) +Graphs.rem_vertices!(fg::FactorGraph, vs) = rem_vertices!(fg.g, vs) +Graphs.add_edge!(fg::FactorGraph, s, d) = add_edge!(fg.g, s, d) +Graphs.add_vertex!(fg::FactorGraph) = add_vertex!(fg.g) +Graphs.add_vertices!(fg::FactorGraph, n) = add_vertices!(fg.g, n) +Graphs.neighbors(fg::FactorGraph, v) = neighbors(fg.g, v) +is_factor(fg::FactorGraph, v) = v > fg.num_vars +is_variable(fg::FactorGraph, v) = v ≤ fg.num_vars + +function FactorGraph(code::SATformula)::FactorGraph + num_vars = code.num_vars + num_clauses = code.num_clauses + g = SimpleGraph(num_vars + num_clauses) + edge_types = Dict{Tuple{Int, Int}, Int}() + # Add edges between variables and clauses + for (i, clause) in enumerate(code.clauses) + clause_idx = num_vars + i # Clause index in the graph + for var in clause + # Add edge from variable to clause + add_edge!(g, abs(var), clause_idx) + get!(edge_types, (abs(var), clause_idx), -sign(var)) + end + end + + return FactorGraph(g, num_vars, edge_types) +end + +function is_variable(v::Int, num_vars::Int)::Bool + """ + Check if the vertex v is a variable (i.e., its index is less than or equal to num_vars). + + """ + return v<= num_vars +end + +function Set_messages(FG::FactorGraph) + # Set messages in the factor graph + messages = Dict{Tuple{Int, Int}, Float64}() + g = FG.g + for e in edges(g) + messages[(src(e), dst(e))] = 0.5 # Initialize messages to uniform distribution + messages[(dst(e), src(e))] = 0.5 # Initialize messages in the opposite direction + end + + return messages +end + +function seperate_messages(messages::Dict{Tuple{Int, Int}, TA}, num_vars::Int64) where TA + """ + Seperate messages into two dictionaries: one for variable to factor messages and one for factor to variable messages. + """ + messages_v2f = Dict{Tuple{Int, Int}, TA}() + messages_f2v = Dict{Tuple{Int, Int}, TA}() + + for (key, value) in messages + if is_variable(key[1], num_vars) # Variable to factor message + messages_v2f[key] = value + else # Factor to variable message + messages_f2v[key] = value + end + end + + return messages_v2f, messages_f2v +end + +function BP_update!(input_messages::Dict{Tuple{Int, Int}, TA}, neighbors_ja::Vector{Int}, neighbors_bj::Vector{Tuple{Int64, Int64}}, num_vars::Int64, a::Int, edge_types::Dict{Tuple{Int, Int}, Int}, damping_factor::Float64=1.0, tolerance::Float64=1e-6) where {TA} + # Input: Set of all input_messages arriving onto each variable node j ∈ V(a)\i, a is the function node, i is the variable node to which we are sending the message to. + + V_plus = Vector{Tuple{Int64, Int64}}() # 变量j的原变量边 (a,j) where J=-1 + V_minus = Vector{Tuple{Int64, Int64}}() # 变量j的否定边 (a,j) where J=1 + + for (b, j) in neighbors_bj + J = edge_types[(j, b)] + if J == -1 + push!(V_plus, (b, j)) + elseif J == 1 + push!(V_minus, (b, j)) + end + end + γ_product = 1.0 # 初始化γ乘积 + # 对每个邻居j ∈ V(a)\i 计算γ_j→a + for j in neighbors_ja + # 获取边(a,j)的类型 + J_aj = edge_types[(j, a)] + @assert J_aj in [1, -1] "Edge type for ($a, $j) must be 1 or -1" + # 确定Vu(j→a)和Vs(j→a)的边集合 + if J_aj == -1 + # J_aj=-1: 原变量边，按公式Vu(j)=V_plus[j]\a，Vs=V_minus[j]\a + Vu = V_minus + Vs = V_plus + else + # J_aj=1: 否定边，按公式Vu(j)=V_minus[j]\a，Vs=V_plus[j]\a + Vu = V_plus + Vs = V_minus + end + # 计算Pu_j→a: ∏_{b ∈ Vu} (1 - δ_b→j) + Pu = 1.0 + for (b, j) in Vu + δ = input_messages[(b, j)] + Pu *= (1 - δ) + end + Pu = isempty(Vu) ? 1.0 : Pu # 处理空集 + # 计算Ps_j→a: ∏_{b ∈ Vs} (1 - δ_b→j) + Ps = 1.0 + for (b, j) in Vs + δ = input_messages[(b, j)] + Ps *= (1 - δ) + end + Ps = isempty(Vs) ? 1.0 : Ps + # 计算γ_j→a = Ps / (Pu + Ps) + γ = Ps / (Pu + Ps + eps()) # 加eps()防止除零 + γ_product *= γ + end + + + # # 应用阻尼（可选） + # if damping_factor < 1.0 + # old_δ = messages[(a, i)] + # new_δ = damping_factor * new_δ + (1 - damping_factor) * old_δ + # end + # new_messages[(a, i)] = new_δ + + + return γ_product +end + +function BP_iterate(order, messages::Dict{Tuple{Int, Int}, Float64}, messages_init::Dict{Tuple{Int, Int}, Float64}, FG::FactorGraph, edge_types::Dict{Tuple{Int, Int}, Int}) + new_messages = Dict{Tuple{Int, Int}, Float64}() + for (a, i) in order + # 获取 V(a)\i：所有与a相连的变量节点，排除i + neighbors_ja = [j for (a_prime, j) in keys(messages) if a_prime == a && j != i] + if isempty(neighbors_ja) # 跳过无邻居的情况 + new_messages[(a, i)] = 1.0 # 跳过无邻居的情况 + else + neighbors_bj = [(b,k) + for k in neighbors_ja + for b in FG.num_vars:ne(g) + if k != b && b!=a && haskey(messages, (b, k)) ] + + if isempty(neighbors_bj) + new_messages[(a, i)] = 0.5 # 跳过无邻居的情况 + else + input_message = Dict( + (b, k) => messages_init[(b, k)] + for (b, k) in neighbors_bj + ) # b is the function node, k is the variable node + output_message_ai = BP_update!(input_message, neighbors_ja, neighbors_bj, FG.num_vars, a, edge_types) + new_messages[(a, i)] = output_message_ai + end + end + end + + return new_messages +end + + +function BP(FG::FactorGraph, max_iter::Int=1000, randomvalue::Bool=true, tol::Float64=1e-6) + """ + Belief Propagation algorithm for solving SAT problems represented as a FactorGraph. + Parameters: + g : FactorGraph representing the SAT problem + max_iter : maximum number of iterations + tol : tolerance for convergence + Returns: + "UN-CONVERGED" or all messages. + """ + # Initialize messages + messages = Set_messages(FG) + edge_types = FG.edge_types # Edge types: -1 for original variable edges, 1 for negated variable edges + + + final_iter = 0 + messages_v2f, messages_f2v = seperate_messages(messages, FG.num_vars) + t = collect(keys(messages_f2v)) + order = randomvalue ? t[sortperm(rand(length(t)))] : t + + prev_messages = deepcopy(messages_f2v) # Store previous messages for convergence check + new_messages = Dict{Tuple{Int, Int}, Float64}() + for iter in 1:max_iter + # Update messages from variables to clauses + new_messages = BP_iterate(order, messages, prev_messages, FG, edge_types) + + max_delta = 0.0 + for key in keys(new_messages) + delta = abs(new_messages[key] - get(prev_messages, key, 0.0)) + max_delta = max(max_delta, delta) + end + + prev_messages = deepcopy(new_messages) + + # 判断是否收敛 + if max_delta < tol && iter > 1 # 确保至少有一次迭代 + final_iter = iter + break + end + final_iter = iter # 更新最终迭代次数 + end + + + if final_iter == max_iter + return "UN-CONVERGED" + else + return new_messages + end +end + +function marginal(messages_f2v::Dict{Tuple{Int, Int}, TT}) where TT + + marginals = Dict{Int, TT}() + + for (f, v) in keys(messages_f2v) + haskey(marginals, v) ? marginals[v] *= messages_f2v[(f, v)] : marginals[v] = messages_f2v[(f, v)] + end + + sum_p = sum(values(marginals)) + for v in keys(marginals) + marginals[v] /= sum_p # Normalize marginals + end + return marginals +end + +# function compute_entropy(alpha; k=3, N=100_000, num_iter=100, num_samples=10_000) +# """ +# BP algorithm for calculating entropy density in random 3-SAT +# Parameters: +# alpha : clause density +# k : SAT problem order (default 3-SAT) +# N : population size +# num_iter : iterations for population dynamics +# num_samples : Monte Carlo samples for entropy calculation +# """ +# # Initialize populations with uniform distributions +# rng = MersenneTwister() # Separate RNG for thread safety +# eta = rand(rng, N) +# eta_s = rand(rng, N) + +# # Population dynamics iterations +# for _ in 1:num_iter +# # Update ηs population (clause to variable messages) +# for i in 1:N +# selected = rand(rng, 1:N, k-1) +# new_eta_s = 1.0 - prod(1.0 .- eta[selected]) +# replace_idx = rand(rng, 1:N) +# eta_s[replace_idx] = new_eta_s +# end + +# # Update η population (variable to clause messages) +# for i in 1:N +# p = rand(rng, Poisson(k * alpha / 2)) +# q = rand(rng, Poisson(k * alpha / 2)) +# total = p + q + +# if total == 0 +# new_eta = 0.5 +# else +# selected = rand(rng, 1:N, total) +# pos_neg = eta_s[selected] +# pos = @view pos_neg[1:p] +# neg = @view pos_neg[p+1:end] + +# # Stabilize computation using logarithms +# log_prod1 = sum(log, pos) + sum(x -> log(1 - x), neg) +# log_prod2 = sum(x -> log(1 - x), pos) + sum(log, neg) +# max_log = max(log_prod1, log_prod2) +# log_total = max_log + log(exp(log_prod1 - max_log) + exp(log_prod2 - max_log)) +# new_eta = exp(log_prod1 - log_total) +# end + +# replace_idx = rand(rng, 1:N) +# eta[replace_idx] = new_eta +# end +# end + +# # Calculate entropy components +# term1 = zeros(num_samples) +# term2 = zeros(num_samples) +# term3 = zeros(num_samples) + +# # Parallel computation using threads +# Threads.@threads for i in 1:num_samples +# rng = Random.MersenneTwister() # Thread-local RNG + +# # Term 1 calculation +# indices = rand(rng, 1:N, k) +# product = prod(eta[indices]) +# term1[i] = log(1 - product + 1e-10) + +# # Term 2 calculation +# p = rand(rng, Poisson(k * alpha / 2)) +# q = rand(rng, Poisson(k * alpha / 2)) +# total = p + q + +# if total == 0 +# term2[i] = log(2.0) +# else +# selected = rand(rng, 1:N, total) +# pos_neg = eta_s[selected] +# pos = @view pos_neg[1:p] +# neg = @view pos_neg[p+1:end] + +# log_prod1 = sum(log, pos) + sum(x -> log(1 - x), neg) +# log_prod2 = sum(x -> log(1 - x), pos) + sum(log, neg) +# max_log = max(log_prod1, log_prod2) +# term2[i] = max_log + log(exp(log_prod1 - max_log) + exp(log_prod2 - max_log)) +# end + +# # Term 3 calculation +# idx_eta = rand(rng, 1:N) +# idx_eta_s = rand(rng, 1:N) +# term3[i] = log(eta_s[idx_eta_s] * eta[idx_eta] + +# (1 - eta_s[idx_eta_s]) * (1 - eta[idx_eta]) + 1e-10) +# end + +# # Final entropy calculation +# s = alpha * mean(term1) + mean(term2) - (k * alpha / 2) * mean(term3) +# return s +# end + +# # Example usage +# let alpha = 4.0 # Clause density +# entropy = compute_entropy(alpha) +# println("Entropy density: ", entropy) +# end \ No newline at end of file diff --git a/hw5/zhaohui_zhi/test_BP.jl b/hw5/zhaohui_zhi/test_BP.jl new file mode 100644 index 0000000..829eedc --- /dev/null +++ b/hw5/zhaohui_zhi/test_BP.jl @@ -0,0 +1,107 @@ +include("BP.jl") +using Test +using TensorInference + +function is_tree(g::AbstractGraph) + n = nv(g) # 顶点数 + e = ne(g) # 边数 + + # 边数不等于 n-1 直接返回 false + e != n - 1 && return false + + # 检查连通性（空图或单顶点图直接视为连通） + n ≤ 1 && return true + + # 使用 BFS/DFS 判断连通性（避免依赖特定包的实现） + visited = falses(n) + queue = [1] # 从第一个顶点开始遍历 + visited[1] = true + count = 1 + + while !isempty(queue) + v = popfirst!(queue) + for u in neighbors(g, v) + if !visited[u] + visited[u] = true + push!(queue, u) + count += 1 + end + end + end + + # 所有顶点都被访问过则为连通 + return count == n +end + +clauses1 = SATformula([[-2, -3, -4, 5], [-1, -5, 6], [-5, 7], [-1, -6, -7], [-1, -2, 5], [-1, -3, 5], [-1, -4, 5], [-1, 2, 3, 4, 5, -6]]) +FG = FactorGraph(clauses1) + + + + +@testset "FactorGraph" begin + clauses2 = SATformula([[1, -2], [-1, 2, 3], [3, 4, -5], [1]]) + FG=FactorGraph(clauses2) + # 1 -> 5 var index, 6->9 clause idx, or a, b, c, d + g = FG.g + @test g == SimpleGraph{Int64}(9, [[6, 7, 9], [6, 7], [7, 8], [8], [8], [1, 2], [1, 2, 3], [3, 4, 5], [1]]) + @test FG.num_vars == 5 +end + +@testset "BP_update" begin + clauses2 = SATformula([[1, -2], [-1, 2, -3], [3, 4, -5], [1]]) + FG=FactorGraph(clauses2) + # 1 -> 5 var index, 6->9 clause idx, or a, b, c, d + g = FG.g + edge_types = FG.edge_types + @test g == SimpleGraph{Int64}(9, [[6, 7, 9], [6, 7], [7, 8], [8], [8], [1, 2], [1, 2, 3], [3, 4, 5], [1]]) + @test edge_types == Dict((4, 8) => -1, (3, 7) => 1, (1, 7) => 1, (1, 6) => -1, (1, 9) => -1, (2, 7) => -1, (3, 8) => -1, (2, 6) => 1, (5, 8) => 1) + @test FG.num_vars == 5 + messages = Set_messages(FG) + @test messages == Dict((3, 7) => 0.5, (8, 3) => 0.5, (6, 2) => 0.5, (8, 4) => 0.5, (7, 1) => 0.5, (3, 8) => 0.5, (2, 6) => 0.5, (7, 2) => 0.5, (1, 9) => 0.5, (2, 7) => 0.5, (7, 3) => 0.5, (8, 5) => 0.5, (4, 8) => 0.5, (1, 6) => 0.5, (5, 8) => 0.5, (1, 7) => 0.5, (6, 1) => 0.5, (9, 1) => 0.5) + + messages_v2f, messages_f2v = seperate_messages(messages, FG.num_vars) + @test messages_v2f== Dict((4, 8) => 0.5, (3, 7) => 0.5, (1, 7) => 0.5, (1, 6) => 0.5, (1, 9) => 0.5, (2, 7) => 0.5, (3, 8) => 0.5, (2, 6) => 0.5, (5, 8) => 0.5) + @test messages_f2v == Dict((8, 3) => 0.5, (6, 2) => 0.5, (7, 2) => 0.5, (8, 4) => 0.5, (7, 1) => 0.5, (6, 1) => 0.5, (8, 5) => 0.5, (7, 3) => 0.5, (9, 1) => 0.5) + a = 7 + i = 1 + neighbors_ja = [j for (a_prime, j) in keys(messages) if a_prime == a && j != i] + + + + + @test neighbors_ja == [2, 3] + + neighbors_bj = [(k,b) + for k in neighbors_ja + for b in FG.num_vars:ne(g) + if k != b && b!=a && haskey(messages, (k, b)) ] + + @test neighbors_bj == [(2, 6), (3, 8)] + input_message = Dict( + (k, b) => messages[(k, b)] + for (k,b) in neighbors_bj + ) + + @test input_message == Dict((2, 6) => 0.5, (3, 8) => 0.5) + new_messages = BP_update!(input_message, neighbors_ja, neighbors_bj, FG.num_vars, a, edge_types) + + @test new_messages ≈ 0.25 # 根据具体的计算结果进行调整 + + a=8;i=3 + neighbors_ja = [j for (a_prime, j) in keys(messages) if a_prime == a && j != i] + @test neighbors_ja == [4, 5] + neighbors_bj = [(k,b) + for k in neighbors_ja + for b in FG.num_vars:ne(g) + if k != b && b!=a && haskey(messages, (k, b)) ] +end + +@testset "BP" begin + clauses2 = SATformula([[1, -2], [-1, 2, -3], [3, 4, -5], [1]]) + FG=FactorGraph(clauses2) + # 1 -> 5 var index, 6->9 clause idx, or a, b, c, d + g = FG.g + edge_types = FG.edge_types + @test BP(FG) == Dict((8, 3) => 0.5, (6, 2) => 0.0, (7, 2) => 0.9999999999999996, (8, 4) => 0.25, (7, 1) => 0.22222222222222213, (6, 1) => 0.9999999999999993, (8, 5) => 0.25, (7, 3) => 0.0, (9, 1) => 1.0) +end \ No newline at end of file