From 1d964fd7230a4b2724dda49f3204f185cd340899 Mon Sep 17 00:00:00 2001 From: ArrogantGao Date: Mon, 26 May 2025 12:23:26 +0800 Subject: [PATCH 1/2] update dpll --- hw3/xzgao/Manifest.toml | 293 ++++++++++++++++++++++++++++++++++++++++ hw3/xzgao/Project.toml | 3 + hw3/xzgao/dpll.jl | 91 +++++++++++++ 3 files changed, 387 insertions(+) create mode 100644 hw3/xzgao/Manifest.toml create mode 100644 hw3/xzgao/Project.toml create mode 100644 hw3/xzgao/dpll.jl diff --git a/hw3/xzgao/Manifest.toml b/hw3/xzgao/Manifest.toml new file mode 100644 index 0000000..34d4f3b --- /dev/null +++ b/hw3/xzgao/Manifest.toml @@ -0,0 +1,293 @@ +# This file is machine-generated - editing it directly is not advised + +julia_version = "1.11.5" +manifest_format = "2.0" +project_hash = "b1ab78982ba1a93dc4c21c11e745e01316748745" + +[[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.BitBasis]] +deps = ["LinearAlgebra", "StaticArrays"] +git-tree-sha1 = "89dc08420d4f593ff30f02611d136b475a5eb43d" +uuid = "50ba71b6-fa0f-514d-ae9a-0916efc90dcf" +version = "0.9.10" + +[[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.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.IteratorInterfaceExtensions]] +git-tree-sha1 = "a3f24677c21f5bbe9d2a714f95dcd58337fb2856" +uuid = "82899510-4779-5014-852e-03e436cf321d" +version = "1.0.0" + +[[deps.LaTeXStrings]] +git-tree-sha1 = "dda21b8cbd6a6c40d9d02a73230f9d70fed6918c" +uuid = "b964fa9f-0449-5b57-a5c2-d3ea65f4040f" +version = "1.4.0" + +[[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.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.Mmap]] +uuid = "a63ad114-7e13-5084-954f-fe012c677804" +version = "1.11.0" + +[[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.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 = "457d73aaff2ee43eb82e5da118e44de32367b203" +uuid = "899c297d-f7d2-4ebf-8815-a35996def416" +version = "0.3.3" + + [deps.ProblemReductions.extensions] + IPSolverExt = "JuMP" + + [deps.ProblemReductions.weakdeps] + JuMP = "4076af6c-e467-56ae-b986-b466b2749572" + +[[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.Sockets]] +uuid = "6462fe0b-24de-5631-8697-dd941f90decc" +version = "1.11.0" + +[[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" + + [deps.StaticArrays.extensions] + StaticArraysChainRulesCoreExt = "ChainRulesCore" + StaticArraysStatisticsExt = "Statistics" + + [deps.StaticArrays.weakdeps] + ChainRulesCore = "d360d2e6-b24c-11e9-a2a3-2a2ae2dbcce4" + Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" + +[[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.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.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 = "598cd7c1f68d1e205689b1c2fe65a9f85846f297" +uuid = "bd369af6-aec1-5ad0-b16a-f7cc5008161c" +version = "1.12.0" + +[[deps.Test]] +deps = ["InteractiveUtils", "Logging", "Random", "Serialization"] +uuid = "8dfed614-e22c-5e08-85e1-65c5234f0b40" +version = "1.11.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.libblastrampoline_jll]] +deps = ["Artifacts", "Libdl"] +uuid = "8e850b90-86db-534c-a0d3-1478176c7d93" +version = "5.11.0+0" diff --git a/hw3/xzgao/Project.toml b/hw3/xzgao/Project.toml new file mode 100644 index 0000000..d8ae81a --- /dev/null +++ b/hw3/xzgao/Project.toml @@ -0,0 +1,3 @@ +[deps] +ProblemReductions = "899c297d-f7d2-4ebf-8815-a35996def416" +Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40" diff --git a/hw3/xzgao/dpll.jl b/hw3/xzgao/dpll.jl new file mode 100644 index 0000000..c3536b3 --- /dev/null +++ b/hw3/xzgao/dpll.jl @@ -0,0 +1,91 @@ +using ProblemReductions +using Test + +function dpll(cnf::CNF{T}) where T + res, config = _dpll(deepcopy(cnf), Dict{T, Bool}()) + if !res + return false, nothing + else + for clause in cnf.clauses + for var in clause.vars + if !(var.name in keys(config)) + config[var.name] = true + end + end + end + return true, config + end +end + +function _dpll(cnf::CNF{T}, config::Dict{T, Bool}) where T + isempty(cnf.clauses) && return true, config + for clause in cnf.clauses + if isempty(clause.vars) + return false, nothing + end + end + + for clause in cnf.clauses + if length(clause.vars) == 1 + var_fix = clause.vars[1] + cnf = apply_config!(cnf, var_fix.name, !var_fix.neg) + config[var_fix.name] = !var_fix.neg + return _dpll(cnf, config) + end + end + + for clause in cnf.clauses + for var in clause.vars + if !(var.name in keys(config)) + config1 = deepcopy(config) + config1[var.name] = !var.neg + res1, config1 = _dpll(apply_config!(deepcopy(cnf), var.name, !var.neg), config1) + + config2 = deepcopy(config) + config2[var.name] = var.neg + res2, config2 = _dpll(apply_config!(deepcopy(cnf), var.name, var.neg), config2) + + if res1 + return true, config1 + elseif res2 + return true, config2 + else + return false, nothing + end + end + end + end +end + +function apply_config!(cnf::CNF{T}, var_name::T, val::Bool) where T + for i in 1:length(cnf.clauses) + clause = popfirst!(cnf.clauses) + push_flag = true + for j in 1:length(clause.vars) + var = popfirst!(clause.vars) + if var.name == var_name + if !var.neg == val # the config is true + push_flag = false + break + end + else + push!(clause.vars, var) + end + end + if push_flag + push!(cnf.clauses, clause) + end + end + return cnf +end + +@testset "dpll" begin + bv1, bv2, bv3 = BoolVar.(["x", "y", "z"]) + clause1 = CNFClause([bv1, bv2, bv3]) + clause2 = CNFClause([BoolVar("w"), bv1, BoolVar("x", true)]) + cnf = CNF([clause1, clause2]) + + res, config = dpll(cnf) + @test res + @test satisfiable(cnf, config) +end \ No newline at end of file From eb55ac3980ba15339d4443cb62523bab73bf7775 Mon Sep 17 00:00:00 2001 From: ArrogantGao Date: Mon, 26 May 2025 20:14:16 +0800 Subject: [PATCH 2/2] update dpll --- hw3/xzgao/dpll.jl | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/hw3/xzgao/dpll.jl b/hw3/xzgao/dpll.jl index c3536b3..f55097f 100644 --- a/hw3/xzgao/dpll.jl +++ b/hw3/xzgao/dpll.jl @@ -40,18 +40,14 @@ function _dpll(cnf::CNF{T}, config::Dict{T, Bool}) where T config1 = deepcopy(config) config1[var.name] = !var.neg res1, config1 = _dpll(apply_config!(deepcopy(cnf), var.name, !var.neg), config1) + res1 && return true, config1 config2 = deepcopy(config) config2[var.name] = var.neg res2, config2 = _dpll(apply_config!(deepcopy(cnf), var.name, var.neg), config2) + res2 && return true, config2 - if res1 - return true, config1 - elseif res2 - return true, config2 - else - return false, nothing - end + return false, nothing end end end