UNIVERSITY OF BELGRADE
DEPARTMENT FOR COMPUTER SCIENCE

ARGO

Automated reasoning group

Downloads

Formalisations

KRK chess endgame
Complex geometry
Classic DPLL procedure
Modern SAT solver verification
Frankl's Conjecture: FC Families
Simplex procedure
Tarski's book
Automated verification of informal proofs

Software

ArgoSat
Source code (v1.0)

ArgoSmArT (solver portfolio)
Source and binaries

ArgoSmArT k-NN
Source and binaries

ArgoLib
Description for SMTCOMP'07
Source code (v3.5)
Binary for linux (v3.5)

ArgoClp
Executable (v2.0)
Executable (v3.0) (with automated support for dealing with symmetric predicates and reformulations of lemmas)
Executable (v4.0) (with support for tptp input and XML output)

GCLC - geometry software
Distribution

LAV
LAV page

Non-CNF instance features computation
Source code and executables

OpenGeoProver - Wu's method for geometry theorem proving
Source code

A strategy for KRK Chess endgame
URSA specifications (of the game, strategy, and correctness lemmas) and C program for analysis of KRK

meSAT
meSAT page (instance based selection of encodings included)

ATCo shift scheduling
ATCo shift scheduling page

Sudoku solver and generator
Sudoku page

Coherent logic Vernacular
CLVernacular

ArgoTriCS - Triangle Construction Solver
ArgoTriCS

Marc Bezem's CL (Coherent Logic) page on Hessenberg's Theorem