The pattern-backtracking FPT algorithm and experimental data set for the WSP with class-independent constraints

This folder contains an executable code of the pattern-backtracking FPT algorithm and an experimental data set used for the WSP with class-independent constraints in:J. Crampton, A. Gagarin, G. Gutin, M. Jones, and M. Wahlstrom, “On the workflow satisfiability problem with class-independent constraints for hierarchical organizations,” 2015. The pattern-backtracking FPT algorithm is implemented in C++. The project is compiled using Eclipse Standard/SDK, Version: Kepler Service Release 1. The executable code is created on a MacBook Pro computer having a 2.6 GHz Intel Core i5 processor, 8 GB 1600 MHz DDR3 RAM 2 and running Mac OS X Version 10.9.5. This is an advanced and more efficient implementation of the pattern-backtracking FPT algorithm which returns a solution assignment in the case of solved satisfiable instances and explicitly checks correctness of the obtained solution assignment. Some memory and time control features are added as well. The random generator used to create the experimental data set is a development of the random generator described in:D. Cohen, J. Crampton, A. Gagarin, G. Gutin, and M. Jones, “Algorithms for the workflow satisfiability problem engineered for counting constraints,” J. Combinatorial Optimization (2015), in press.In particular, the random instance generator avoids generation of trivially unsatisfiable instances with respect to class-independent constraints. The current calendar time is used as a random seed value. Each instance of the original WSP is stored in a file with extension .wsp and named WSP_input_#S_#U_#C_a_b_c_d.wsp, where #S is the number of steps in the instance, #U is the number of users, #C is the number of equivalence classes of users, a is the number of user-independent not-equals (separation-of-duty) constraints, b is the number of user-independent at-most constraints, c is the number of class-independent equivalence constraints (requiring a pair of steps to be performed by users from the same equivalence class), and d is the number of class-independent non-equivalence constraints (requiring a pair of steps to be performed by users from different equivalence classes). The corresponding formulation of the instance in terms of the pseudo-Boolean satisfiability (PB SAT) problem is stored in a file with extension .opb and named WSP_input_#S_#U_#C_a_b_c_d_PBSAT.opb. A reader can install the PB SAT solver SAT4J and run it on these PB SAT formulation input files. The outputs of our runs of SAT4J on the PB SAT formulation are stored in files named WSP_input_#S_#U_#C_a_b_c_d_PBSAT_output.txt. The PB SAT solution converted back to the original WSP solution is stored in files named WSP_input_#S_#U_#C_a_b_c_d_PBSAT_output_WSPsoln.txt (clearly, only solved satisfiable PB SAT instances provide non-empty WSP solution files). The outcome decisions of the FPT algorithm (“satisfiable” or “unsatisfiable”), together with solution assignments (if applicable) and some basic information about its runs (numbers of patterns generated and considered in the search space, the running times) are stored in files named WSP_input_#S_#U_#C_a_b_c_d_FPTgen_soln.txt. This implementation of the FPT algorithm has check points for memory usage and elapsed running time. It stops the computational process when the running time of the FPT algorithm reaches one hour limit or the virtual memory consumption exceeds 64GB. Summary Excel tables for the computational experiments are included as well. The executable code of the FPT algorithm and the experimental data set are provided for non-commercial use only. When using this executable code or the data set, please cite the full-size paper above.