{'fraction_non_alphanumeric': 0.017597551644988524, 'fraction_numerical': 0.0007651109410864575, 'mean_word_length': 5.742268041237113, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Visualising SMT-Based Parallel Constraint Solving

Problem instances arising from a multitude of applications can be naturally reduced to the search for a solution satisfying a set of constraints. Characteristically such applications, that include model checking and the satisfiability of propositional formulas (SAT) and SAT modulo theories, are notorious for the computational complexity of the underlying decision problem. A central approach for tackling the hardness of these problems is through the use of parallel computing, with methods such as divide-and-conquer, algorithm portfolios, and their combinations. However, such algorithms are often complicated and it is difficult to assess whether their executions have anomalies. This paper presents a user-friendly interface to analyze the partitioning tree parallelization approach that generalizes both divide-and-conquer and algorithm portfolios. We use the interface to analyze parallel executions of both the IC3/PDR algorithm and an SMT solver, demonstrating its usefulness in visualizing the otherwise complicated executions of diverse algorithms in a parallel environment. Based on the initial results we believe that the visualization of these executions will further encourage the adoption of parallel computing techniques in these domains.