Skip to content

Commit

Permalink
bugfix
Browse files Browse the repository at this point in the history
  • Loading branch information
@mb706
mb706 committed Sep 23, 2024
1 parent e428a94 commit 7583cab
Show file tree
Hide file tree
Showing 2 changed files with 125 additions and 2 deletions.
6 changes: 4 additions & 2 deletions R/CnfFormula_simplify1.R
View file
Original file line number Diff line number Diff line change
Expand Up @@ -586,6 +586,7 @@ simplify_cnf = function(entries, universe) {
}
# prefer to eliminate the outer loopo clause first, since we have already
# done more work for the inner loop clause (which comes earlier in 'entries')
not_subset_count[meta_idx_outer, meta_idx_inner] = sum(is_not_subset_of[[meta_idx_outer]][meta_idx_inner, ])
rowsum = sum(is_not_subset_of[[meta_idx_inner]][meta_idx_outer, ])
not_subset_count[meta_idx_inner, meta_idx_outer] = rowsum
if (rowsum <= 2) {
Expand All @@ -594,8 +595,8 @@ simplify_cnf = function(entries, universe) {
if (ousr) return(return_entries(FALSE))
if (eliminated[[clause_idx_inner]] || is_unit[[clause_idx_inner]]) next # yes this can happen.
}
rowsum = sum(is_not_subset_of[[meta_idx_outer]][meta_idx_inner, ])
not_subset_count[meta_idx_outer, meta_idx_inner] = rowsum
# need to get rowsum back again, since the call above could have changed something!
rowsum = not_subset_count[meta_idx_outer, meta_idx_inner]
if (rowsum <= 2) {
ousr = on_updated_subset_relations(meta_idx_outer, meta_idx_inner)
if (identical(ousr, TRUE)) return(return_entries(FALSE))
Expand All @@ -604,6 +605,7 @@ simplify_cnf = function(entries, universe) {
}
}
}

# Now for the big one: Asymmetric Hidden Literal Addition (Marijn et al.)

# First, we do non-units, then we do units separately.
Expand Down
121 changes: 121 additions & 0 deletions attic/experiments.R
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1133,3 +1133,124 @@ V2 %among% c("v2_5", "v2_2", "v2_3") & V2 %among% c("v2_5", "v2_4", "v2_3", "v2_
V2 %among% c("v2_2", "v2_1"))) & (V1 %among% c("v1_5", "v1_3") & V4 %among% c("v4_3", "v4_5", "v4_4") & (V1 %among% c("v1_4", "v1_5", "v1_2", "v1_3") &
V4 %among% c("v4_3", "v4_2", "v4_1")) |
V3 %among% c("v3_2", "v3_3", "v3_1") & V3 %among% c("v3_1", "v3_5", "v3_2") & (V4 %among% "v4_4" & V2 %among% c("v2_1", "v2_5", "v2_3", "v2_2")))))


quote((V3 %among% c("v3_3", "v3_1") & V2 %among% c("v2_1", "v2_5", "v2_4") & (V1 %among% c("v1_1", "v1_4", "v1_2", "v1_5") & V3 %among% "v3_3") |
(V3 %among% c("v3_2", "v3_1", "v3_3") & V2 %among% c("v2_5", "v2_4") | V1 %among% c("v1_2", "v1_1", "v1_5", "v1_3") & V4 %among% c("v4_4", "v4_2", "v4_1"))) &
(V4 %among% c("v4_2", "v4_3", "v4_1", "v4_5") & V4 %among% c("v4_1", "v4_4", "v4_5") | (V2 %among% c("v2_3", "v2_2", "v2_5", "v2_4") | V3 %among% "v3_1") |
V4 %among% c("v4_3", "v4_4", "v4_5") & V4 %among% c("v4_1", "v4_5", "v4_4") & (V1 %among% c("v1_3", "v1_1", "v1_5") | V3 %among% "v3_2")) &
((V3 %among% c("v3_2", "v3_3") & V2 %among% "v2_5" | (V1 %among% "v1_3" | V4 %among% c("v4_3", "v4_2", "v4_4", "v4_1")) | V2 %among% c("v2_5", "v2_4") &
V4 %among% c("v4_5", "v4_2") & (V2 %among% c("v2_5", "v2_4", "v2_3") | V4 %among% c("v4_1", "v4_5", "v4_4"))) & (V1 %among% "v1_2" & V2 %among% "v2_2" |
(V2 %among% c("v2_3", "v2_4") | V2 %among% c("v2_3", "v2_4", "v2_1", "v2_2")) |
(V3 %among% c("v3_1", "v3_5", "v3_2", "v3_4") & V4 %among% c("v4_1", "v4_4") | V3 %among% "v3_4" & V4 %among% c("v4_5", "v4_4"))))
) |> eval() |> formula_to_expression() |> evaluate_expression(assignments) -> a1

quote((V3 %among% c("v3_3", "v3_1") & V2 %among% c("v2_1", "v2_5", "v2_4") & (V1 %among% c("v1_1", "v1_4", "v1_2", "v1_5") & V3 %among% "v3_3") |
(V3 %among% c("v3_2", "v3_1", "v3_3") & V2 %among% c("v2_5", "v2_4") | V1 %among% c("v1_2", "v1_1", "v1_5", "v1_3") & V4 %among% c("v4_4", "v4_2", "v4_1"))) &
(V4 %among% c("v4_2", "v4_3", "v4_1", "v4_5") & V4 %among% c("v4_1", "v4_4", "v4_5") | (V2 %among% c("v2_3", "v2_2", "v2_5", "v2_4") | V3 %among% "v3_1") |
V4 %among% c("v4_3", "v4_4", "v4_5") & V4 %among% c("v4_1", "v4_5", "v4_4") & (V1 %among% c("v1_3", "v1_1", "v1_5") | V3 %among% "v3_2")) &
((V3 %among% c("v3_2", "v3_3") & V2 %among% "v2_5" | (V1 %among% "v1_3" | V4 %among% c("v4_3", "v4_2", "v4_4", "v4_1")) | V2 %among% c("v2_5", "v2_4") &
V4 %among% c("v4_5", "v4_2") & (V2 %among% c("v2_5", "v2_4", "v2_3") | V4 %among% c("v4_1", "v4_5", "v4_4"))) & (V1 %among% "v1_2" & V2 %among% "v2_2" |
(V2 %among% c("v2_3", "v2_4") | V2 %among% c("v2_3", "v2_4", "v2_1", "v2_2")) |
(V3 %among% c("v3_1", "v3_5", "v3_2", "v3_4") & V4 %among% c("v4_1", "v4_4") | V3 %among% "v3_4" & V4 %among% c("v4_5", "v4_4"))))
) |> evaluate_expression(assignments) -> a2

which(a1 != a2)



quote(

(((V2 %among% "v2_2" | V1 %among% "v1_2") & (V1 %among% c("v1_1", "v1_3") & V4 %among% c("v4_3", "v4_1")) | (V3 %among% c("v3_2", "v3_3") &
V3 %among% c("v3_3", "v3_1") | V1 %among% "v1_1" & V3 %among% "v3_2") | (V3 %among% "v3_3" | V3 %among% c("v3_3", "v3_2") |
V1 %among% c("v1_1", "v1_3") & V1 %among% "v1_2" | (V1 %among% c("v1_1", "v1_3") | V1 %among% "v1_1" | (V2 %among% c("v2_2", "v2_1") |
V4 %among% "v4_2")))) & (((V2 %among% c("v2_2", "v2_1") | V4 %among% c("v4_3", "v4_1")) & (V2 %among% c("v2_2", "v2_3") & V4 %among% c("v4_1", "v4_2")) |
(V1 %among% c("v1_3", "v1_1") | V4 %among% c("v4_1", "v4_2")) & (V1 %among% "v1_3" & V2 %among% "v2_3")) & (V2 %among% "v2_3" & V4 %among% "v4_2" | (V3 %among% "v3_3" |
V3 %among% c("v3_2", "v3_3")) | (V2 %among% "v2_2" | V1 %among% "v1_2" | V2 %among% "v2_2" & V4 %among% c("v4_3", "v4_2")))) | ((V3 %among% "v3_2" | V3 %among% c("v3_2", "v3_1")) &
(V2 %among% "v2_1" | V2 %among% c("v2_2", "v2_3")) | V1 %among% "v1_1" & V1 %among% "v1_1" & (V2 %among% "v2_2" | V3 %among% "v3_3")) &
((V4 %among% c("v4_2", "v4_3") & V3 %among% "v3_1" | (V2 %among% c("v2_3", "v2_2") | V2 %among% c("v2_3", "v2_2"))) & (V1 %among% "v1_2" &
V2 %among% "v2_2" & (V2 %among% "v2_3" & V1 %among% "v1_3"))) & ((V2 %among% "v2_1" | V2 %among% c("v2_1", "v2_2") | V2 %among% "v2_2" &
V2 %among% c("v2_2", "v2_3") | (V1 %among% c("v1_1", "v1_2") | V2 %among% c("v2_3", "v2_2")) & (V3 %among% c("v3_1", "v3_3") & V4 %among% c("v4_1", "v4_3"))) &
(V3 %among% "v3_3" & V3 %among% c("v3_2", "v3_1") | V4 %among% "v4_2" & V2 %among% "v2_2" | V3 %among% c("v3_1", "v3_3") & V4 %among% c("v4_2", "v4_1") &
(V3 %among% "v3_2" & V4 %among% "v4_1")))) &

((V2 %among% c("v2_1", "v2_2") & V2 %among% "v2_2" & (V2 %among% c("v2_3", "v2_1") | V3 %among% c("v3_2", "v3_3")) |
(V1 %among% "v1_1" | V1 %among% c("v1_2", "v1_1") | (V2 %among% "v2_2" | V2 %among% c("v2_2", "v2_3"))) | (V2 %among% "v2_3" & V2 %among% c("v2_1", "v2_3") &
(V4 %among% "v4_2" | V3 %among% c("v3_2", "v3_1")) | V2 %among% "v2_1" & V4 %among% "v4_3" & (V3 %among% "v3_2" | V2 %among% c("v2_2", "v2_3")))) &
(((V1 %among% c("v1_1", "v1_3") | V1 %among% "v1_3") & (V4 %among% c("v4_3", "v4_2") | V1 %among% c("v1_1", "v1_2")) | V3 %among% "v3_1" & V2 %among% c("v2_1", "v2_3") &
(V4 %among% c("v4_3", "v4_2") & V3 %among% c("v3_2", "v3_1"))) & ((V1 %among% c("v1_3", "v1_1") | V1 %among% c("v1_3", "v1_2")) & (V2 %among% c("v2_3", "v2_2") & V1 %among% "v1_2") |
V4 %among% c("v4_3", "v4_1") & V3 %among% "v3_2" & (V3 %among% c("v3_2", "v3_1") | V2 %among% "v2_3"))) & (((V1 %among% "v1_2" | V4 %among% "v4_3") & (V1 %among% c("v1_1", "v1_2") |
V2 %among% "v2_3") | V3 %among% "v3_2" & V1 %among% c("v1_2", "v1_3") & (V3 %among% c("v3_3", "v3_1") | V2 %among% c("v2_3", "v2_2"))) & (V1 %among% c("v1_1", "v1_2") &
V2 %among% c("v2_2", "v2_1") | (V3 %among% "v3_2" | V2 %among% "v2_3") | V2 %among% c("v2_2", "v2_3") & V1 %among% c("v1_3", "v1_1") & (V2 %among% "v2_2" | V2 %among% c("v2_1", "v2_2"))) |
(V2 %among% "v2_1" & V2 %among% "v2_3" | V4 %among% "v4_1" & V2 %among% "v2_1" | V1 %among% c("v1_1", "v1_3") & V1 %among% c("v1_1", "v1_2") & (V4 %among% c("v4_1", "v4_2") & V2 %among% "v2_2")) &
(V1 %among% "v1_1" & V1 %among% c("v1_3", "v1_2") | V3 %among% c("v3_2", "v3_1") & V3 %among% "v3_2" | (V2 %among% c("v2_1", "v2_2") | V4 %among% "v4_1" | V2 %among% "v2_3" & V3 %among% "v3_2"))))
) -> bigex

evaluate_expression(bigex, ass)
evaluate_expression(formula_to_expression(eval(bigex)), ass)


# |> eval() |> formula_to_expression() |> evaluate_expression(assignments) -> a1

which(a1 != a2)

ass <- assignments[which(a1 != a2), ]



eval(bigex) |> as.list() |> lapply(as.CnfFormula) |> lapply(formula_to_expression) |> sapply(evaluate_expression, assignment = ass) -> clauses


which(!clauses)


e1 <- (((V2 %among% "v2_2" | V1 %among% "v1_2") & (V1 %among% c("v1_1", "v1_3") & V4 %among% c("v4_3", "v4_1")) | (V3 %among% c("v3_2", "v3_3") &
V3 %among% c("v3_3", "v3_1") | V1 %among% "v1_1" & V3 %among% "v3_2") | (V3 %among% "v3_3" | V3 %among% c("v3_3", "v3_2") |
V1 %among% c("v1_1", "v1_3") & V1 %among% "v1_2" | (V1 %among% c("v1_1", "v1_3") | V1 %among% "v1_1" | (V2 %among% c("v2_2", "v2_1") |
V4 %among% "v4_2")))) & (((V2 %among% c("v2_2", "v2_1") | V4 %among% c("v4_3", "v4_1")) & (V2 %among% c("v2_2", "v2_3") & V4 %among% c("v4_1", "v4_2")) |
(V1 %among% c("v1_3", "v1_1") | V4 %among% c("v4_1", "v4_2")) & (V1 %among% "v1_3" & V2 %among% "v2_3")) & (V2 %among% "v2_3" & V4 %among% "v4_2" | (V3 %among% "v3_3" |
V3 %among% c("v3_2", "v3_3")) | (V2 %among% "v2_2" | V1 %among% "v1_2" | V2 %among% "v2_2" & V4 %among% c("v4_3", "v4_2")))) | ((V3 %among% "v3_2" | V3 %among% c("v3_2", "v3_1")) &
(V2 %among% "v2_1" | V2 %among% c("v2_2", "v2_3")) | V1 %among% "v1_1" & V1 %among% "v1_1" & (V2 %among% "v2_2" | V3 %among% "v3_3")) &
((V4 %among% c("v4_2", "v4_3") & V3 %among% "v3_1" | (V2 %among% c("v2_3", "v2_2") | V2 %among% c("v2_3", "v2_2"))) & (V1 %among% "v1_2" &
V2 %among% "v2_2" & (V2 %among% "v2_3" & V1 %among% "v1_3"))) & ((V2 %among% "v2_1" | V2 %among% c("v2_1", "v2_2") | V2 %among% "v2_2" &
V2 %among% c("v2_2", "v2_3") | (V1 %among% c("v1_1", "v1_2") | V2 %among% c("v2_3", "v2_2")) & (V3 %among% c("v3_1", "v3_3") & V4 %among% c("v4_1", "v4_3"))) &
(V3 %among% "v3_3" & V3 %among% c("v3_2", "v3_1") | V4 %among% "v4_2" & V2 %among% "v2_2" | V3 %among% c("v3_1", "v3_3") & V4 %among% c("v4_2", "v4_1") &
(V3 %among% "v3_2" & V4 %among% "v4_1"))))

e2 <- ((V2 %among% c("v2_1", "v2_2") & V2 %among% "v2_2" & (V2 %among% c("v2_3", "v2_1") | V3 %among% c("v3_2", "v3_3")) |
(V1 %among% "v1_1" | V1 %among% c("v1_2", "v1_1") | (V2 %among% "v2_2" | V2 %among% c("v2_2", "v2_3"))) | (V2 %among% "v2_3" & V2 %among% c("v2_1", "v2_3") &
(V4 %among% "v4_2" | V3 %among% c("v3_2", "v3_1")) | V2 %among% "v2_1" & V4 %among% "v4_3" & (V3 %among% "v3_2" | V2 %among% c("v2_2", "v2_3")))) &
(((V1 %among% c("v1_1", "v1_3") | V1 %among% "v1_3") & (V4 %among% c("v4_3", "v4_2") | V1 %among% c("v1_1", "v1_2")) | V3 %among% "v3_1" & V2 %among% c("v2_1", "v2_3") &
(V4 %among% c("v4_3", "v4_2") & V3 %among% c("v3_2", "v3_1"))) & ((V1 %among% c("v1_3", "v1_1") | V1 %among% c("v1_3", "v1_2")) & (V2 %among% c("v2_3", "v2_2") & V1 %among% "v1_2") |
V4 %among% c("v4_3", "v4_1") & V3 %among% "v3_2" & (V3 %among% c("v3_2", "v3_1") | V2 %among% "v2_3"))) & (((V1 %among% "v1_2" | V4 %among% "v4_3") & (V1 %among% c("v1_1", "v1_2") |
V2 %among% "v2_3") | V3 %among% "v3_2" & V1 %among% c("v1_2", "v1_3") & (V3 %among% c("v3_3", "v3_1") | V2 %among% c("v2_3", "v2_2"))) & (V1 %among% c("v1_1", "v1_2") &
V2 %among% c("v2_2", "v2_1") | (V3 %among% "v3_2" | V2 %among% "v2_3") | V2 %among% c("v2_2", "v2_3") & V1 %among% c("v1_3", "v1_1") & (V2 %among% "v2_2" | V2 %among% c("v2_1", "v2_2"))) |
(V2 %among% "v2_1" & V2 %among% "v2_3" | V4 %among% "v4_1" & V2 %among% "v2_1" | V1 %among% c("v1_1", "v1_3") & V1 %among% c("v1_1", "v1_2") & (V4 %among% c("v4_1", "v4_2") & V2 %among% "v2_2")) &
(V1 %among% "v1_1" & V1 %among% c("v1_3", "v1_2") | V3 %among% c("v3_2", "v3_1") & V3 %among% "v3_2" | (V2 %among% c("v2_1", "v2_2") | V4 %among% "v4_1" | V2 %among% "v2_3" & V3 %among% "v3_2"))))

evaluate_expression(formula_to_expression(e1), ass)
evaluate_expression(formula_to_expression(e2), ass)
evaluate_expression(formula_to_expression(e1 & e2), ass)

e1
e2
eval(e1 & e2) |> as.list() |> lapply(as.CnfFormula) |> lapply(formula_to_expression) |> sapply(evaluate_expression, assignment = ass) -> clauses

e1&e2

entries[!eliminated] |> lapply(function(x) structure(list(x), universe = universe, class = "CnfFormula")) |> lapply(formula_to_expression) |> sapply(evaluate_expression, assignment = ass) -> cl
entries[!eliminated][!cl] |> lapply(structure, class = "CnfClause")

meta_idx_inner
c
lapply(seq_along(eliminated), function(x) if (eliminated[[x]]) FALSE else structure(entries[[x]], class = "CnfClause"))

entries[!eliminated] |> lapply(structure, class = "CnfClause")
which(eliminated)

which(!clauses)

e1&e2
e1
e2

0 comments on commit 7583cab

Please sign in to comment.