Solving problems using Z3Py.
Z3Py code to solve the scheduling problem is given as follows. There are seven jobs #1, #2, #3, #4, #5, #6 and #7. All jobs are executed by three people A, B, and C. Solutions of the scheduling problem must satisfy all of the following constraints.
- Each job should be executed by one of three persons A, B, and C without interruption.
- Each person can handle at most one job each time.
- Each job #𝑖 has running time 3 + 𝑖 if person C executes it, and 4 + 𝑖 otherwise.
- Only person B is allowed to execute jobs #1 and #7.
- Job #2 should run after jobs #5 and #6 have finished.
- Each job should be done in time 0 to 20.
Declare only three functions whose domains and ranges are both the set of integers.
- Function S maps each job to its start time.
- Function E maps each job to its end time.
- Function P maps each job to the person who executes it.
Z3Py code to establish the possibility that the following program causes a crash.
Here, ‘←’ is an assignment operator, and ‘?1’ and ‘?2’ are unknown tests that may yield false or true in any situation.
Solve the magic squares problem using Z3Py, the task is to construct a magic square, given an incomplete N x N number grid square.