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

<p>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:<br>J. Crampton, A. Gagarin, G. Gutin, and M. Jones, “On the workflow satisfiability problem with class-independent constraints,” Proc. 10th International Symposium on Parameterized and Exact Computation (IPEC 2015), 16-18 September, Patras, Greece, LIPIcs series, Schloss Dagstuhl - Leibniz Center for Informatics, 2015.</p> <p>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 a preliminary implementation of the pattern-backtracking FPT algorithm which is still under development. This version only decides whether an instance is satisfiable or not, without returning an actual assignment solution for satisfiable instances.</p> <p>The random generator used to create the experimental data set is a development of the random generator described in:<br>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.<br>In particular, the random instance generator avoids generation of trivially unsatisfiable instances with respect to class-independent constraints, and the current calendar time is used as a random seed value.</p> <p>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: the 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 some basic information about its runs (numbers of patterns generated and considered in the search space, the run times) are stored in files named WSP_input_#S_#U_#C_a_b_c_d_FPTgen_soln.txt. A new version of the FPT algorithm (under development) is going to return actual assignment solutions in case of satisfiable instances and stop the computational process when the FPT algorithm is not likely to be able to solve an instance. Summary Excel tables for the computational experiments are included as well.</p> <p>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 conference paper above.</p> <p> </p> <p>