Rectify

crillab · Feb 19, 2024 · 75c9529 · 75c9529
1 parent 2d6ff68
commit 75c9529
Show file tree

Hide file tree

Showing 31 changed files with 192 additions and 24 deletions.
diff --git a/pyxai/examples/DT/builder-rectify2.py b/pyxai/examples/DT/builder-rectify2.py
@@ -46,9 +46,6 @@
 
 print("Minimal sufficient reason:", minimal)
 
-print("")
-print("[rectify]")
-
 explainer.rectify(decision_rule=minimal, label=1) 
 print("binary representation: ", explainer.binary_representation)
 print("target_prediction:", explainer.target_prediction)

diff --git a/pyxai/sources/core/explainer/explainerDT.py b/pyxai/sources/core/explainer/explainerDT.py
@@ -296,7 +296,6 @@ def is_reason(self, reason, *, n_samples=-1):
 
     def simplify_theory(self, tree_rectified):
         if self._theory is True:
-            print("Rectify simplify_theory ...")
             solver = GlucoseSolver()
             #max_id_binary_cnf = CNFencoding.compute_max_id_variable(tree_rectified)
             #theory_cnf, _ = self._tree.get_theory(
@@ -305,7 +304,6 @@ def simplify_theory(self, tree_rectified):
             #        id_new_var=max_id_binary_cnf)
             theory_cnf = self._tree.get_theory(None)
             tree_rectified = solver.symplify_theory(tree_rectified, theory_cnf)
-            print("Rectify simplify_theory: ", tree_rectified.raw_data_for_CPP())
             return tree_rectified
         return tree_rectified
 
@@ -320,24 +318,32 @@ def rectify(self, *, decision_rule, label):
         Returns:
             DecisionTree: The rectified tree.  
         """
-
+        print("")
+        print("-------------- Rectify information:")
         tree_decision_rule = self._tree.decision_rule_to_tree(decision_rule)
-        print("tree_decision_rule:", tree_decision_rule.raw_data_for_CPP())
-
+        print("Desision Rule Number of nodes:", tree_decision_rule.n_nodes())
+        print("Model Number of nodes:", self._tree.n_nodes())
         if label == 1:
             #  
             tree_decision_rule = tree_decision_rule.negating_tree()
             tree_rectified = self._tree.disjoint_tree(tree_decision_rule)
+            print("Model Number of nodes (after rectify):", tree_rectified.n_nodes())
             tree_rectified = self.simplify_theory(tree_rectified)
+            print("Model Number of nodes (symplify theory):", tree_rectified.n_nodes())
             tree_rectified.simplify()
+            print("Model Number of nodes (symplify redundancy):", tree_rectified.n_nodes())
         else:
             # 
             tree_rectified = self._tree.concatenate_tree(tree_decision_rule)
+            print("Model Number of nodes (after rectify):", tree_rectified.n_nodes())
             self.simplify_theory(tree_rectified)
+            print("Model Number of nodes (symplify theory):", tree_rectified.n_nodes())
             tree_rectified.simplify()
+            print("Model Number of nodes (symplify redundancy):", tree_rectified.n_nodes())
         self._tree = tree_rectified
         if self._instance is not None:
             self.set_instance(self._instance)
+        print("--------------")
         return self._tree
 
 

diff --git a/pyxai/sources/core/structure/decisionTree.py b/pyxai/sources/core/structure/decisionTree.py
@@ -311,7 +311,12 @@ def compute_nodes_with_leaves(self, node):
             output += self.compute_nodes_with_leaves(node.right)
         return output
 
+    def n_nodes(self):
+        return self._n_nodes(self.root)
 
+    def _n_nodes(self, node):
+        return 1 if node.is_leaf() else 1 + self._n_nodes(node.left) + self._n_nodes(node.right)
+
     def display(self, node):
         if node.is_leaf():
             print(node)

diff --git a/pyxai/sources/solvers/SAT/glucoseSolver.py b/pyxai/sources/solvers/SAT/glucoseSolver.py
@@ -34,63 +34,61 @@ def propagate(self, reason):
         return self.glucose.propagate(reason)
 
     def symplify_theory(self, decision_tree, theory_cnf):
-        print("theory_cnf:", theory_cnf)
         self.add_clauses(theory_cnf)
 
-
         def is_node_consistent(node, stack):
             if node.is_leaf():
-                return True, True
+                return False, False
 
-            id_feature = node.id_feature    
+            id_literal = decision_tree.map_features_to_id_binaries[(node.id_feature, node.operator, node.threshold)][0]
             # Check consistency on the left
-            stack.append(-id_feature)
+            stack.append(-id_literal)
             left_consistent = self.glucose.propagate(stack)[0]
+
             stack.pop()
 
             # Check consistency on the right
-            stack.append(id_feature)
+            stack.append(id_literal)
             right_consistent = self.glucose.propagate(stack)[0]
             stack.pop()
-
             return left_consistent, right_consistent
 
         def _symplify_theory(node, *, stack, parent, come_from, root):
             if node.is_leaf():
                 return root
-            id_feature = node.id_feature 
+            id_literal = decision_tree.map_features_to_id_binaries[(node.id_feature, node.operator, node.threshold)][0]
             left_consistent, right_consistent = is_node_consistent(node, stack)
             if left_consistent:
                 # The left part is consistent, simplify recursively
-                root = _symplify_theory(node.left, stack=stack + [-id_feature], parent=node, come_from=0, root=root)
+                root = _symplify_theory(node.left, stack=stack + [-id_literal], parent=node, come_from=0, root=root)
             else:
                 # The left part is inconsistent, replace this node with the right
                 if come_from == None:
                     #The root change
-                    root = _symplify_theory(node.right, stack=stack + [id_feature], parent=None, come_from=None, root=node.right)
+                    root = _symplify_theory(node.right, stack=stack + [id_literal], parent=None, come_from=None, root=node.right)
                 elif come_from == 0:
                     #Replace the node
                     parent.left = node.right
-                    root = _symplify_theory(node.right, stack=stack + [id_feature], parent=parent, come_from=0, root=root)
+                    root = _symplify_theory(node.right, stack=stack + [id_literal], parent=parent, come_from=0, root=root)
                 elif come_from == 1:
                     parent.right = node.right
-                    root = _symplify_theory(node.right, stack=stack + [id_feature], parent=parent, come_from=1, root=root)
+                    root = _symplify_theory(node.right, stack=stack + [id_literal], parent=parent, come_from=1, root=root)
 
             if right_consistent:
                 # The right part is consistent, simplify recursively
-                root = _symplify_theory(node.right, stack=stack + [id_feature], parent=node, come_from=1, root=root)
+                root = _symplify_theory(node.right, stack=stack + [id_literal], parent=node, come_from=1, root=root)
             else:
                 # The right part is inconsistent, replace with the left
                 if come_from == None:
                     #The root change
-                    root = _symplify_theory(node.left, stack=stack + [-id_feature], parent=None, come_from=None, root=node.left)
+                    root = _symplify_theory(node.left, stack=stack + [-id_literal], parent=None, come_from=None, root=node.left)
                 elif come_from == 0:
                     #Replace the node
                     parent.left = node.left
-                    root = _symplify_theory(node.left, stack=stack + [-id_feature], parent=parent, come_from=0, root=root)
+                    root = _symplify_theory(node.left, stack=stack + [-id_literal], parent=parent, come_from=0, root=root)
                 elif come_from == 1:
                     parent.right = node.left
-                    root = _symplify_theory(node.left, stack=stack + [-id_feature], parent=parent, come_from=1, root=root)
+                    root = _symplify_theory(node.left, stack=stack + [-id_literal], parent=parent, come_from=1, root=root)
 
             return root
 

diff --git a/tmp/wbo-10800331.wcnf b/tmp/wbo-10800331.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-13351277.wcnf b/tmp/wbo-13351277.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-14031925.wcnf b/tmp/wbo-14031925.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-15767817.wcnf b/tmp/wbo-15767817.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-15835756.wcnf b/tmp/wbo-15835756.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-16730192.wcnf b/tmp/wbo-16730192.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-17923783.wcnf b/tmp/wbo-17923783.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-18707833.wcnf b/tmp/wbo-18707833.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-19743337.wcnf b/tmp/wbo-19743337.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-19867073.wcnf b/tmp/wbo-19867073.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-20729516.wcnf b/tmp/wbo-20729516.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-21395586.wcnf b/tmp/wbo-21395586.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-23269759.wcnf b/tmp/wbo-23269759.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-23933993.wcnf b/tmp/wbo-23933993.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-24262394.wcnf b/tmp/wbo-24262394.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-24336094.wcnf b/tmp/wbo-24336094.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-24932345.wcnf b/tmp/wbo-24932345.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-25434562.wcnf b/tmp/wbo-25434562.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-26224984.wcnf b/tmp/wbo-26224984.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-26857975.wcnf b/tmp/wbo-26857975.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-28079137.wcnf b/tmp/wbo-28079137.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-52461942.wcnf b/tmp/wbo-52461942.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-54381170.wcnf b/tmp/wbo-54381170.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-74319869.wcnf b/tmp/wbo-74319869.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-80783887.wcnf b/tmp/wbo-80783887.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-82078600.wcnf b/tmp/wbo-82078600.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0
diff --git a/tmp/wbo-99781932.wcnf b/tmp/wbo-99781932.wcnf
@@ -0,0 +1,6 @@
+p wcnf 2 5 3
+1 -1 0
+1 -2 0
+3 1 2 0
+3 -1 -2 0
+3 -1 -2 0