add domain_on_triple

sagebei · Nov 14, 2023 · cfb74ba · cfb74ba
1 parent 876e401
commit cfb74ba
Show file tree

Hide file tree

Showing 5 changed files with 76 additions and 16 deletions.
diff --git a/algorithms/benckmarking/sat_solver.py b/algorithms/benckmarking/sat_solver.py
@@ -0,0 +1,18 @@
+from z3 import *
+from cdl import *
+
+cd = CondorcetDomain(5)
+trs = cd.init_trs()
+
+solver = Solver()
+
+rules = []
+for i in range(cd.num_triples):
+    rules.append(Int(f"t{i}"))
+
+solver.add([And(rule >= 1, rule <= 4) for rule in rules])
+
+solver.add(cd.size(cd.trs_to_state(rules)) == 18)
+
+while solver.check() == sat:
+    model = solver.model()
diff --git a/bind/bind.cpp b/bind/bind.cpp
@@ -107,6 +107,7 @@ PYBIND11_MODULE(cdl, m) {
             .def("subset_weights", &CondorcetDomain::subset_weights)
             .def("subset_trs_list", &CondorcetDomain::subset_trs_list, py::arg("trs"))
             .def("subset_domain_list", &CondorcetDomain::subset_domain_list, py::arg("domain"))
+            .def("domain_on_triple", &CondorcetDomain::domain_on_triple, py::arg("cd"), py::arg("triple"))
             .def("subset_states", &CondorcetDomain::subset_states, py::arg("trs"))
             .def("subset_states_any_ordering", &CondorcetDomain::subset_states_any_ordering, py::arg("trs"))
             .def("subset_cd_sizes", &CondorcetDomain::subset_cd_sizes, py::arg("trs"))

diff --git a/core/include/condorcet_domain.h b/core/include/condorcet_domain.h
@@ -69,6 +69,7 @@ class CondorcetDomain
     std::vector<int> subset_weights();
     std::vector<TRS> subset_trs_list(const TRS& trs);
     CDS subset_domain_list(const CD& cd);
+    CD domain_on_triple(const CD& cd, const Triple& triple);
     std::vector<std::vector<Int8>> subset_states(const TRS& trs);
     std::vector<std::vector<Int8>> subset_states_any_ordering(const TRS& trs);
     std::tuple<std::vector<TRS>, std::vector<std::size_t>> subset_cd_sizes(const TRS& trs);

diff --git a/core/src/condorcet_domain.cpp b/core/src/condorcet_domain.cpp
@@ -581,6 +581,35 @@ CDS CondorcetDomain::subset_domain_list(const CD& cd)
     return subset_cds;
 }
 
+CD CondorcetDomain::domain_on_triple(const CD& cd, const Triple& triple)
+{
+    std::set<IntList> subset_domain{};
+
+    for (const IntList& permutation : cd)
+    {
+        std::map<Int8, Int8> idx_alt{};
+        for (const Int8& t : triple)
+        {
+            int idx = get_index(permutation, t);
+            if (idx == -1)
+                break;
+            else
+                idx_alt[idx] = t;
+        }
+
+        if (idx_alt.size() == 3)
+        {
+            IntList sub_perm{};
+            for (const auto &pair: idx_alt)
+                sub_perm.push_back(pair.second);
+            subset_domain.insert(sub_perm);
+        }
+    }
+
+    CD subset_cd(subset_domain.begin(), subset_domain.end());
+    return subset_cd;
+}
+
 std::vector<std::vector<Int8>> CondorcetDomain::subset_states(const TRS& trs)
 {
     std::vector<std::vector<Int8>> sub_states{};

diff --git a/core/src/main.cpp b/core/src/main.cpp
@@ -68,24 +68,35 @@
 //    return 0;
 //}
 
+//int main()
+//{
+//    CondorcetDomain cd(5);
+//    auto trs = cd.init_trs();
+//    trs = cd.assign_rule_by_index(trs, 0, "1N3");
+//    trs = cd.assign_rule_by_index(trs, 1, "2N3");
+//    trs = cd.assign_rule_by_index(trs, 2, "2N3");
+//    trs = cd.assign_rule_by_index(trs, 3, "2N3");
+//    trs = cd.assign_rule_by_index(trs, 4, "2N3");
+//    trs = cd.assign_rule_by_index(trs, 5, "2N3");
+//    trs = cd.assign_rule_by_index(trs, 6, "2N3");
+//    trs = cd.assign_rule_by_index(trs, 7, "1N3");
+//    trs = cd.assign_rule_by_index(trs, 8, "1N3");
+//    trs = cd.assign_rule_by_index(trs, 9, "1N3");
+//
+//
+//    print_trs(trs);
+//    bool result = cd.is_trs_isomorphic(trs, {1, 3, 5}, {"1N3", "2N3"});
+//    std::cout<< result << std::endl;
+//    return 0;
+//}
+
 int main()
 {
     CondorcetDomain cd(5);
-    auto trs = cd.init_trs();
-    trs = cd.assign_rule_by_index(trs, 0, "1N3");
-    trs = cd.assign_rule_by_index(trs, 1, "2N3");
-    trs = cd.assign_rule_by_index(trs, 2, "2N3");
-    trs = cd.assign_rule_by_index(trs, 3, "2N3");
-    trs = cd.assign_rule_by_index(trs, 4, "2N3");
-    trs = cd.assign_rule_by_index(trs, 5, "2N3");
-    trs = cd.assign_rule_by_index(trs, 6, "2N3");
-    trs = cd.assign_rule_by_index(trs, 7, "1N3");
-    trs = cd.assign_rule_by_index(trs, 8, "1N3");
-    trs = cd.assign_rule_by_index(trs, 9, "1N3");
-
-
-//    print_trs(trs);
-    bool result = cd.is_trs_isomorphic(trs, {1, 3, 5}, {"1N3", "2N3"});
-    std::cout<< result << std::endl;
+    TRS trs = cd.init_trs();
+//    TRS trs = cd.init_trs_by_scheme(Fishburn_scheme);
+    CD domain = cd.domain(trs);
+    CD sub_domain = cd.domain_on_triple(domain, {1, 2, 3});
+    std::cout << sub_domain.size() << std::endl;
     return 0;
 }