Bryan Bu Wen Bin

Z3-Solver Github Z3-Solver

This is the programming project for my third-semester AI Programming portfolio exam. In this project, I was asked to construct tables according to the given specifications.

Description

The aim of this project is to solve a simplified version of very common problem, instances of which appear in scheduling, production planning, resource allocation, etc. The problem is to find integer values with which to fill an m x n table, ensuring that given constraints on the values are met, and in such a way that the sum of the values in the table is minimal.

Example

Fill in a 2 x 3 table A such that
👉 A[i][j] ≤ 10
👉 A[i][j] > -5
👉 A[1][j] + A[2][j] > 1
👉 A[i][j] < A[i + 1][j]

Variables that appear as indices are assumed to be universally bound, i.e., the condition must hold for all indices in the range of the table. The first index is the row index, ranging from 1 to m, the second is the column index, ranging from 1 to n. Thus, the last condition is an abbreviation for the list
👉 A[1][1] < A[2][1]
👉 A[1][2] < A[2][2]
👉 A[1][3] < A[2][3]

A table satisfying these constraints

-3	2	-1
10	4	3

This is, however, not a minimal-sum solution. An actual minimal sum solution to this problem is, for example:

-4	-2	0
6	4	2

(the third constraint tells us that the sum of all values will be ≥ 6). The minimal solution is, in general, not unique.

Approach

So, I was asked to implement a solve function to take in the list of constraints and then pass it to the Z3 Solver to solve for the value of each cell. To achieve this, I first need to implement a parser system to properly format the constraints in the list, ensuring they are translated into a format that the Z3 Solver can understand. For more detailed information, you can refer to my GitHub repository.

RETURN