diff --git a/hw4/hmyu/Manifest.toml b/hw4/hmyu/Manifest.toml
new file mode 100644
index 0000000..34d4f3b
--- /dev/null
+++ b/hw4/hmyu/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/hw4/hmyu/Project.toml b/hw4/hmyu/Project.toml
new file mode 100644
index 0000000..d8ae81a
--- /dev/null
+++ b/hw4/hmyu/Project.toml
@@ -0,0 +1,3 @@
+[deps]
+ProblemReductions = "899c297d-f7d2-4ebf-8815-a35996def416"
+Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
diff --git a/hw4/hmyu/ucsc.jl b/hw4/hmyu/ucsc.jl
new file mode 100644
index 0000000..be7b352
--- /dev/null
+++ b/hw4/hmyu/ucsc.jl
@@ -0,0 +1,180 @@
+using ProblemReductions
+using Random, Test
+"""
+uc(cnf::CNF{T}) -> Bool
+
+The Unit Clause (UC) algorithm attempts to determine the satisfiability of a given CNF formula. It uses unit clause propagation and random assignments to iteratively simplify the formula.
+
+Parameters:
+- `cnf`: A CNF formula represented as a `CNF{T}` object, where `T` is the type of variable names.
+
+Returns:
+- `true`: Indicates that the CNF formula is satisfiable.
+- `false`: Indicates "don't know," meaning the algorithm could not determine satisfiability.
+
+Notes:
+- This algorithm may return `false` for satisfiable formulas in some cases.
+
+"""
+function uc(cnf::CNF{T}) where T
+    assignments = Dict{T, Bool}()
+    cnf1 = deepcopy(cnf)
+    unsatisfied_clauses = get_unsatisfied_clauses(cnf1, assignments)
+
+    # Process unsatisfied clauses until all are satisfied or a conflict occurs
+    while !isempty(unsatisfied_clauses)
+        unit_clauses = get_unit_clauses(unsatisfied_clauses)
+        if !isempty(unit_clauses)
+            # Handle unit clauses by assigning values to their variables
+            chosen_clause = rand(unit_clauses)
+            chosen_var = chosen_clause.vars[1]
+            assignments[chosen_var.name] = !chosen_var.neg
+        else
+            # Randomly assign values to unset variables if no unit clauses exist
+            unset_vars = [var for clause in unsatisfied_clauses for var in clause.vars if !(var.name in keys(assignments))]
+            isempty(unset_vars) && return false
+            chosen_var = rand(unset_vars)
+            assignments[chosen_var.name] = rand(Bool)
+        end
+
+        # Apply the assignment and update the CNF formula
+        cnf1 = apply_assignment!(cnf1, chosen_var.name, assignments[chosen_var.name])
+
+        # Check for conflicts (empty clauses)
+        if any(is_empty_clause(clause) for clause in cnf1.clauses)
+            return false
+        end
+        unsatisfied_clauses = get_unsatisfied_clauses(cnf1, assignments)
+    end
+    return true
+end
+
+
+"""
+sc(cnf::CNF{T}) -> Bool
+
+The Short Clause (SC) algorithm attempts to determine the satisfiability of a given CNF formula. It uses unit clause propagation, two-clause handling, and random assignments to iteratively simplify the formula.
+
+Parameters:
+- `cnf`: A CNF formula represented as a `CNF{T}` object, where `T` is the type of variable names.
+
+Returns:
+- `true`: Indicates that the CNF formula is satisfiable.
+- `false`: Indicates "don't know," meaning the algorithm could not determine satisfiability.
+
+Notes:
+- This algorithm may return `false` for satisfiable formulas in some cases.
+
+"""
+function sc(cnf::CNF{T}) where T
+    assignments = Dict{T, Bool}()
+    cnf1 = deepcopy(cnf)
+    unsatisfied_clauses = get_unsatisfied_clauses(cnf1, assignments)
+
+    # Process unsatisfied clauses until all are satisfied or a conflict occurs
+    while !isempty(unsatisfied_clauses)
+        unit_clauses = get_unit_clauses(unsatisfied_clauses)
+        two_clauses = get_two_clauses(unsatisfied_clauses)
+        if !isempty(unit_clauses)
+            # Handle unit clauses by assigning values to their variables
+            chosen_clause = rand(unit_clauses)
+            chosen_var = chosen_clause.vars[1]
+            assignments[chosen_var.name] = !chosen_var.neg
+        elseif !isempty(two_clauses)
+            # Handle 2-clauses by assigning values to one of their variables
+            chosen_clause = rand(two_clauses)
+            chosen_var = rand(chosen_clause.vars)
+            assignments[chosen_var.name] = !chosen_var.neg
+        else
+            # Randomly assign values to unset variables if no unit or two-clauses exist
+            unset_vars = [var for clause in unsatisfied_clauses for var in clause.vars if !(var.name in keys(assignments))]
+            isempty(unset_vars) && return false
+            chosen_var = rand(unset_vars)
+            assignments[chosen_var.name] = rand(Bool)
+        end
+
+        # Apply the assignment and update the CNF formula
+        cnf1 = apply_assignment!(cnf1, chosen_var.name, assignments[chosen_var.name])
+
+        # Check for conflicts (empty clauses)
+        if any(is_empty_clause(clause) for clause in cnf1.clauses)
+            return false
+        end
+        unsatisfied_clauses = get_unsatisfied_clauses(cnf1, assignments)
+    end
+    return true
+end
+
+function apply_assignment!(cnf::CNF{T}, var_name::T, value::Bool) where T
+    updated_clauses = Vector{CNFClause{T}}()
+    for i in 1:length(cnf.clauses)
+        clause = popfirst!(cnf.clauses)
+        push_flag = true
+        new_vars = Vector{typeof(clause.vars[1])}()
+        for j in 1:length(clause.vars)
+            var = popfirst!(clause.vars)
+            if var.name == var_name
+                if !var.neg == value
+                    push_flag = false
+                    break
+                end
+            else
+                push!(new_vars, var)
+            end
+        end
+        if push_flag
+            push!(updated_clauses, CNFClause(new_vars))
+        end
+    end
+    return CNF(updated_clauses)
+end
+
+function is_satisfied(clause::CNFClause{T}, assignments::Dict{T, Bool}) where T
+    for var in clause.vars
+        if var.name in keys(assignments) && assignments[var.name] == !var.neg
+            return true
+        end
+    end
+    return false
+end
+
+function is_empty_clause(clause::CNFClause{T}) where T
+    isempty(clause.vars)
+end
+
+function get_unit_clauses(clauses::Vector{CNFClause{T}}) where T
+    return [clause for clause in clauses if length(clause.vars) == 1]
+end
+
+function get_two_clauses(clauses::Vector{CNFClause{T}}) where T
+    return [clause for clause in clauses if length(clause.vars) == 2]
+end
+
+function get_unsatisfied_clauses(cnf::CNF{T}, assignments::Dict{T, Bool}) where T
+    return [clause for clause in cnf.clauses if !is_satisfied(clause, assignments)]
+end
+
+
+@testset "uc and sc" begin
+    bv1, bv2, bv3, bv4 = BoolVar.(["x", "y", "z", "w"])
+    clause1 = CNFClause([bv1, bv2, bv3])  # (x ∨ y ∨ z)
+    clause2 = CNFClause([bv4, bv1, ¬bv1])  # (w ∨ x ∨ ¬x)
+    cnf1 = CNF([clause1, clause2])
+
+    @test uc(cnf1)
+    @test sc(cnf1)
+
+    clause3 = CNFClause([bv1, bv2])  # (x ∨ y)
+    clause4 = CNFClause([¬bv3, ¬bv4])  # (¬z ∨ ¬w)
+    cnf2 = CNF([clause3, clause4])
+
+    @test uc(cnf2)
+    @test sc(cnf2)
+
+    clause5 = CNFClause([BoolVar("a")])  # (a)
+    clause6 = CNFClause([BoolVar("a", true)])  # (¬a)
+    unsat_cnf = CNF([clause5, clause6])
+
+    @test !uc(unsat_cnf)
+    @test !sc(unsat_cnf)
+end