FindC2 not working properly

pycona/benchmarks/__init__.py

@@ -4,4 +4,6 @@
 from .exam_timetabling import construct_examtt_simple
 from .job_shop_scheduling import construct_job_shop_scheduling_problem
 from .nurse_rostering import construct_nurse_rostering
-
+from .zebra import construct_zebra_problem
+from .nqueens import construct_nqueens_problem
+from .golomb import construct_golomb

pycona/benchmarks/golomb.py

@@ -0,0 +1,138 @@
+import cpmpy as cp
+from cpmpy.transformations.normalize import toplevel_list
+from ..answering_queries.constraint_oracle import ConstraintOracle
+from ..problem_instance import ProblemInstance, absvar
+from itertools import combinations
+from ..utils import get_scope, replace_variables, combine_sets_distinct
+
+class GolombInstance(ProblemInstance):
+
+    def construct_bias(self, X=None):
+        """
+        Construct the bias (candidate constraints) for the golomb instance. 
+        We need a different bias construction for the golomb instance because 
+        it needs to include all permutations of scopes for the quaternary relations.
+        """
+        if X is None:
+            X = self.X
+
+        all_cons = []
+
+        for relation in self.language:
+
+            abs_vars = get_scope(relation)
+
+            combs = list(combinations(X, 2))
+
+            if len(abs_vars) == 2:
+                for comb in combs:
+                    replace_dict = dict()
+                    for i, v in enumerate(comb):
+                        replace_dict[abs_vars[i]] = v
+                    constraint = replace_variables(relation, replace_dict)
+                    all_cons.append(constraint)
+            elif len(abs_vars) == 4:
+                result_combinations = combine_sets_distinct(combs, combs)
+                for ((v1, v2), (v3, v4)) in result_combinations:
+                    replace_dict = dict()
+                    replace_dict[abs_vars[0]] = v1
+                    replace_dict[abs_vars[1]] = v2
+                    replace_dict[abs_vars[2]] = v3
+                    replace_dict[abs_vars[3]] = v4
+                    constraint = replace_variables(relation, replace_dict)
+                    all_cons.append(constraint)
+
+        self.bias = list(set(all_cons) - set(self.cl) - set(self.excluded_cons))
+
+    def construct_bias_for_vars(self, v1, X=None):
+        """
+        Construct the bias (candidate constraints) for specific variables in the golomb instance.
+        Overrides the parent class method to handle the special case of quaternary relations in Golomb.
+
+        Args:
+            v1: The variable(s) for which to construct the bias. Can be a single variable or list of variables.
+            X: The set of variables to consider, default is None (uses self.X).
+        """
+        if not isinstance(v1, list):
+            v1 = [v1]
+
+        if X is None:
+            X = self.X
+
+        # Sort X based on variable names for consistency
+        X = sorted(X, key=lambda var: var.name)
+
+        all_cons = []
+
+        for relation in self.language:
+            abs_vars = get_scope(relation)
+
+            combs = list(combinations(X, 2))
+
+            if len(abs_vars) == 2:
+                for comb in combs:
+                    replace_dict = dict()
+                    for i, v in enumerate(comb):
+                        replace_dict[abs_vars[i]] = v
+                    constraint = replace_variables(relation, replace_dict)
+                    all_cons.append(constraint)
+            elif len(abs_vars) == 4:
+                result_combinations = combine_sets_distinct(combs, combs)
+                for ((v1_, v2), (v3, v4)) in result_combinations:
+                    replace_dict = dict()
+                    replace_dict[abs_vars[0]] = v1_
+                    replace_dict[abs_vars[1]] = v2
+                    replace_dict[abs_vars[2]] = v3
+                    replace_dict[abs_vars[3]] = v4
+                    constraint = replace_variables(relation, replace_dict)
+                    all_cons.append(constraint)
+
+        # Filter constraints to only include those containing at least one of the specified variables
+        filtered_cons = [c for c in all_cons if any(v in set(get_scope(c)) for v in v1)]
+        self.bias = list(set(filtered_cons) - set(self.cl) - set(self.excluded_cons))
+
+
+def construct_golomb(n_marks=8):
+    """
+    :Description: The Golomb ruler problem is to place n marks on a ruler such that the distances between any two marks are all different.
+    A Golomb ruler with 8 marks is sought in this instance.
+    :return: a ProblemInstance object, along with a constraint-based oracle
+    """
+    # Parameters
+    parameters = {"n_marks": n_marks}
+
+    # Variables
+    grid = cp.intvar(1, n_marks*8, shape=(1, n_marks), name="grid") 
+    # adaptive domain: the larger the domain the slower query generation is
+    # current domain makes it satisfiable up to 12 marks, more marks make it too slow either way
+
+    C_T = []
+
+    all_mark_pairs = []
+    for a in range(n_marks):
+        for b in range(a + 1, n_marks):
+            all_mark_pairs.append((a, b))
+
+    for outer_idx in range(len(all_mark_pairs)):
+        i, j = all_mark_pairs[outer_idx]  # Get the first pair of marks (i, j)
+
+        for inner_idx in range(outer_idx + 1, len(all_mark_pairs)):
+            x, y = all_mark_pairs[inner_idx]  # Get the second pair of marks (x, y)
+
+            C_T += [cp.abs(grid[0, j] - grid[0, i]) != cp.abs(grid[0, y] - grid[0, x])]
+
+    for i in range(n_marks):
+        for j in range(i + 1, n_marks):
+            C_T += [grid[0, i] < grid[0, j]]
+
+    # Create the language:
+    AV = absvar(4)  # create abstract vars - as many as maximum arity
+
+    # create abstract relations using the abstract vars
+    lang = [AV[0] == AV[1], AV[0] != AV[1], AV[0] < AV[1], AV[0] > AV[1], AV[0] >= AV[1], AV[0] <= AV[1], cp.abs(AV[0] - AV[1]) != cp.abs(AV[2] - AV[3])]
+
+    instance = GolombInstance(variables=grid, params=parameters, language=lang, name="golomb")
+
+    oracle = ConstraintOracle(list(set(toplevel_list(C_T))))
+
+    return instance, oracle

pycona/benchmarks/nqueens.py

@@ -0,0 +1,48 @@
+import cpmpy as cp
+from cpmpy.transformations.normalize import toplevel_list
+from ..answering_queries.constraint_oracle import ConstraintOracle
+from ..problem_instance import ProblemInstance, absvar
+
+def construct_nqueens_problem(n):
+
+    parameters = {"n": n}
+
+    queens = cp.intvar(1, n, shape=n, name="queens")
+
+    # Model
+    model = cp.Model()
+
+    # Constraints list
+    CT = []
+    diag = []
+
+    CT += list(cp.AllDifferent(queens).decompose())
+
+    for i in range(n):
+        for j in range(i + 1, n): # Compare each queen with every other queen once
+            diag += [(queens[i] - i != queens[j] - j)]  # Different major diagonals
+            diag += [(queens[i] + i != queens[j] + j)]  # Different minor diagonals
+
+    # Add all collected constraints to the model
+    model += CT + diag
+
+    C_T = toplevel_list(CT + diag) 
+
+    AV = absvar(2)
+    lang = [AV[0] == AV[1], AV[0] != AV[1], AV[0] < AV[1], AV[0] > AV[1], AV[0] >= AV[1], AV[0] <= AV[1]]
+    #lang = [AV[0] - AV[1] == constant for constant in range(-n, 2*n)] + [AV[0] - AV[1] != constant for constant in range(-n, 2*n)]
+
+    instance = ProblemInstance(variables=queens, params=parameters, language=lang, name="nqueens")
+
+    instance.construct_bias()
+    instance.bias = instance.bias + diag
+
+    oracle = ConstraintOracle(list(set(toplevel_list(C_T))))
+
+    print("oracle constraints: ", len(oracle.constraints))
+    for c in oracle.constraints:
+        print(c)
+
+    input("Press Enter to continue...")
+
+    return instance, oracle

pycona/benchmarks/zebra.py

@@ -0,0 +1,63 @@
+import cpmpy as cp
+from cpmpy.transformations.normalize import toplevel_list
+from ..answering_queries.constraint_oracle import ConstraintOracle
+from ..problem_instance import ProblemInstance, absvar
+
+
+def construct_zebra_problem():
+    """
+    :Description: The zebra puzzle is a well-known logic puzzle. Five houses, each of a different color, are occupied by men of 
+    different nationalities, with different pets, drinks and cigarettes. The puzzle is to find out who owns the zebra.
+    The puzzle has 15 clues that help determine the solution.
+    :return: a ProblemInstance object, along with a constraint-based oracle
+    """
+    # Create a dictionary with the parameters
+    parameters = {"grid_size": 5, "num_categories": 5}
+
+    # Variables
+    # Flattened array with 25 elements, representing 5 elements for each of the 5 categories
+    grid = cp.intvar(1, 5, shape=(5, 5), name="grid")
+
+    C_T = list()
+
+    # Extract variables for readability
+    ukr, norge, eng, spain, jap = grid[0, :]  # Nationalities
+    red, blue, yellow, green, ivory = grid[1,:]  # Colors
+    oldGold, parly, kools, lucky, chest = grid[2,:]  # Cigarettes
+    zebra, dog, horse, fox, snails = grid[3,:]  # Pets
+    coffee, tea, h2o, milk, oj = grid[4,:]  # Drinks
+
+    # Add all constraints
+    C_T += [(eng == red)]  # Englishman lives in the red house
+    C_T += [(spain == dog)]  # Spaniard owns the dog
+    C_T += [(coffee == green)]  # Coffee is drunk in the green house
+    C_T += [(ukr == tea)]  # Ukrainian drinks tea
+    C_T += [(green == ivory + 1)]  # Green house is immediately right of the ivory house
+    C_T += [(oldGold == snails)]  # OldGold smoker owns snails
+    C_T += [(kools == yellow)]  # Kools are smoked in the yellow house
+    C_T += [(milk == 3)]  # Milk is drunk in the middle house
+    C_T += [(norge == 1)]  # Norwegian lives in the first house
+    C_T += [(abs(chest - fox) == 1)]  # Chesterfield smoker lives next to the man with the fox
+    C_T += [(abs(kools - horse) == 1)]  # Kools are smoked in the house next to the house with the horse
+    C_T += [(lucky == oj)]  # Lucky smoker drinks orange juice
+    C_T += [(jap == parly)]  # Japanese smokes Parliaments
+    C_T += [(abs(norge - blue) == 1)]  # Norwegian lives next to the blue house
+
+    # Each row must have different values
+    for row in grid:
+        C_T += list(cp.AllDifferent(row).decompose())
+
+    # Create the language:
+    AV = absvar(2)  # create abstract vars - as many as maximum arity
+
+    # create abstract relations using the abstract vars
+    lang = [AV[0] == AV[1], AV[0] != AV[1], AV[0] < AV[1], AV[0] > AV[1], AV[0] >= AV[1], AV[0] <= AV[1],
+            abs(AV[0] - AV[1]) == 1, abs(AV[0] - AV[1]) != 1, AV[0] - AV[1] == 1, AV[1] - AV[0] == 1] + [AV[0] == constant for constant in range(1, 6)] + [AV[0] != constant for constant in range(1, 6)]
+
+    instance = ProblemInstance(variables=grid, params=parameters, language=lang, name="zebra")
+
+    oracle = ConstraintOracle(list(set(toplevel_list(C_T))))
+
+
+
+    return instance, oracle

pycona/ca_environment/ca_env_core.py

@@ -92,6 +92,7 @@ def add_to_cl(self, C):
         self.instance.cl.extend(C)
         self.instance.bias = list(set(self.instance.bias) - set(C))
 
-        self.metrics.cl += 1
+        self.metrics.cl += len(C)
         if self.verbose == 1:
-            print("L", end="")
+            for c in C:
+                print("L", end="")