@classmethod
def exactly_half_floor(cls, variables):
    """Clauses encoding a "exactly half" constraint (rounded down)
     
        Parameters
        ----------
        variables : list of variables
           variables in the constraint
     
        Returns
        -------
            a list of clauses
        """
    threshold = int(len(variables) / 2)
    return cls.equal_to_constraint(variables, threshold)
