Algorithms for Computational Logic

This repository belongs to group 10 and holds both projects of alc25 — the Nurse Scheduling Problem (NSP). The two projects solve the same problem on the same public instances; they only differ in implementation strategy:

• sat/ — project 1, MaxSAT formulation using PySAT (RC2 solver with kmtotalizer cardinality encoding).
• smt/ — project 2, integer-variable formulation using Z3's Optimize (per-nurse-per-day start/end/amount ints, with continuity enforced arithmetically).

Each project's statement and report live next to its code as statement.pdf and report.pdf. The shared public test instances live at the repository root in public-tests/, and the nsp-checker binary is shared too.

Repository layout

alc/
├── README.md
├── run.sh                # drives both projects against public-tests/
├── nsp-checker.zip       # Linux checker
├── nsp-checker-mac.zip   # macOS checker
├── public-tests/         # shared instances + expected outputs
├── sat/
│   ├── main.py
│   ├── statement.pdf
│   └── report.pdf
└── smt/
    └── (same)

Running a project locally

cd into the project's folder and pipe a shared instance through Python:

cd sat            # or smt
python3 main.py < ../public-tests/t01.nsp > t01.myout

sat/main.py requires the python-sat package; smt/main.py requires z3-solver.

Checking a single output

Unzip the nsp-checker binary that matches your OS at the repo root (nsp-checker.zip for Linux, nsp-checker-mac.zip for macOS), then:

unzip nsp-checker.zip && chmod +x nsp-checker
./nsp-checker public-tests/t01.nsp sat/t01.myout

Running every public test

From the repo root:

./run.sh              # runs both sat and smt
./run.sh sat          # runs only sat
./run.sh smt          # runs only smt

Each per-instance run is capped at 1800 seconds. Outputs (tNN.myout) and checker results (tNN.check) land inside the respective project folder.