This archive includes the implementations and data used in the experimental part of the following paper:
Daniel Karapetyan, Gregory Gutin. Solving the Workflow Satisfiability Problem using General Purpose Solvers. 2021.

If using the content of this archive for non-commercial purposes, please reference the above paper.  To use any of its content for commercial purposes, please contact the authors (daniel.karapetyan@nottingham.ac.uk, g.gutin@rhul.ac.uk).

Files in the "data" folder:
- Phase transition.txt: gives the values of $e_{k,n}$.  For details, see Section 6.1 of the paper.
- Phase transition SoD.txt: gives the values of $e^c_{k,n}$.  For details, see Section 6.1 of the paper.
- scaling-<c>-10k.txt: the running times of OR-Tools (CS) and OR-Tools (PBPB) along the n = 10k slice.  The WSP_<c>(k, 10k) instances are used, where <c> is a constraint type.  These results were used in Figure 3a.
- scaling-<c>-kIs18.txt: the running times of OR-Tools (CS) and OR-Tools (PBPB) along the k = 18 slice.  The WSP_<c>(18, n) instances are used, where <c> is a constraint type.  These results were used in Figure 3b.

Files in the "solvers" folder include all the solvers, in Python, used in paper.  To work, they need appropriate installations of OR-Tools/Z3/SAT4J.

instances.zip contains all the instances used in the paper.  To generate all the instances, one can also use the instance generator with parameters "wsp.exe generate all".