For constraint programming solvers, you need to define a model (i.e. what are the variables that the solver can change). Typically, a good model naturally enforces hard constraints. For instance, consider the employee scheduling problem, where you have a list of shifts that need to be assigned a single employee. Two possible models for it are:

- Use a boolean variable that is true if and only if a particular employee is assigned to a particular shift. For 2 shifts (A, B) and 2 employees (Amy, Beth), the variables would be Amy_A, Amy_B, Beth_A, Beth_B

- Use an int variable, where each employee is mapped to a number. For 2 shifts (A, B) and 3 employees (Amy, Beth, Carl), the variables would be A, B (which will have value 0 for Amy, 1 for Beth, 2 for Carl).

Using an int variable is usually better, since it automatically encodes the "each shift must have exactly one employee constraint" which would otherwise need to be added. That being said, sometimes the boolean model is used so a SAT solver can be used instead of a Integer Linear Programming Solver.

Typically, for theorem based solvers (such as Z3 or OR Tools), you add a group of similar constraints in a loop where you iterate through relevant variables. For instance, to add constraints for overlapping shifts, you would have a directory mapping each shift to the shifts its overlaps, and add a not equals constraint for each pair (since if they are equal, they have the same employee, and employees usually are unable to be at two places at the same time).

  for shift in shift_vars:
      for overlapping_shift in overlapping_shifts[shift]:
          solver.add(shift != overlapping_shift)

There are also local search solvers, such as Timefold, which allows you use your domain objects and functions directly in your constraints. For instance, the above constraint would look like this:

  @planning_entity
  @dataclass
  class Shift:
      employee: Annotated[Employee, PlanningVariable]
      start: datetime
      end: datetime
      
      def overlaps(self, other: 'Shift') -> bool:
          return self.start < other.end and other.start < self.end
  
  def no_overlapping_shifts(constraint_factory: ConstraintFactory):
      return (constraint_factory.for_each(Shift)
                                .join(Shift,
                                      Joiners.equal(lambda shift: shift.employee))
                                .filter(lambda a, b: a.overlaps(b))
                                .penalize(HardSoftScore.ONE_HARD)
                                .as_constraint('Overlapping Shift'))

Disclosure: I work for Timefold