We aim at comparing Constraint Programming (CP) and
SatisfiabilityModulo Theories (SMT) techniques in order to solve
problems of Very Large ScaleIntegration (VLSI).
We have built two models: one using MiniZinc with the standard CP
theory while the other one employes a similar problem model expressed
in First Order Logic with new specific contraints.
A particular implementation in SAT is also available.
Check the FULL REPORT for all the details.
Very Large Scale Integration (VLSI) is a well known problem since the modern digital electronic was born. The core problem consists in finding the best disposition of chips on a circuit plate in order to minimize the overall size of the device. In our specific case, we have a fixed plate width for every problem instance and all the chips that must be included respecting the plates' size constraints. Then the height of the plate must be minimize.
The following python packages have to be installed on the machine in order to run our implementation of the models:
- matplotlib
- seaborn
- pandas
- numpy
- minizinc
Follow also the minizinc guide to install the minizinc system in order to use the python minizinc package.
All usage information is contained separately for each formulation in the respective directories, which provide README files: CP and SMT
CP model performance on 40 VLSI instances:
SMT model performance on 40 VLSI instances:
The SAT model implementation has also an explicative plot that shows the disposition of the chips (for more details on SAT check the FULL REPORT):
