This repository contains materials for the Logic in Computer Science course (Logika v računalništvu) at Faculty of Mathematics and Physics, University of Ljubljana.
The satsolver folder contains a simple implementation of Boolean expressions in Python, which can be used as a reference for the project of implementing a SAT solver. Its dimacs subfolder contains some formulas in the DIMACS format along with their solutions (i.e., valuations satisfying the formula).
The alloy folder contains exercises in Alloy. The unsolved exercises are in the alloy-original branch.
The nusmv folder contains models for NuSMV.
Materials from the 2017 tutorials.
Links to students' SAT solver repositories from the 2016 and 2017 courses, respectively. The dimacs subfolder contains links to the formulas in DIMACS format provided by students as a part of their assignments. The run subfolder contains scripts used to run the submissions and test their solutions.
Common files used to test the submissions.