SCryptoDiagnoser is a Model-Based Diagnosis solver based on SAT described in the paper "Compiling Model-Based Diagnosis to Boolean Satisfaction".
SCryptoDiagnoser approach is constraint-based and it generating a constraint model for the instance, compiling the constraints to CNF using BEE and solving the CNF using SCryptoMinisat.


SCryptoDiagnoser is a tool which process the System and find Top-Level Minimal Cardinality Diagnoses.
This tool is using BEE and SCryptoMinisat and written in Prolog.

SCryptoDiagnoser Usage

SCryptoDiagnoser Output

SCryptoDiagnoser TLD2ALL

SCryptoDiagnoser TLD2ALL is a tool which expands Top-Level Diagnoses found by ScryptoDiagnoser to all Diagnoses.
This tool implements Procedure 2 from the paper and written in Java.

SCryptoDiagnoser TLD2ALL Usage

SCryptoDiagnoser TLD2ALL Output

File Formats

SCryptoDiagnoser is written in Prolog and therefore the file formats written in Prolog style.

System Description (.sys)

Preprocessed System Description (.syspp)

Observations set (.obs)

Top-Level Diagnoses (.tld)

All Diagnoses (.all)


Solver Downloads

SCryptoDiagnoser compiled with SWI Prolog 6.0.2.

Instances Downloads

Experiments Information Downloads