{'fraction_non_alphanumeric': 0.016605166051660517, 'fraction_numerical': 0.0, 'mean_word_length': 6.0, '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}}
Integrating Simplication Techniques in SAT Algorithms

Propositional Satisfiability (SAT) is fundamental in solving many application problems in Artificial Intelligence and in other fields of Computer Science and Engineering. In the past, it has already been shown that large simplifications can be obtained using algebraic simplification techniques. On the other hand, intelligent backtrack search algorithms for SAT have empirically been shown to be highly effective in pruning the amount of search, applying strategies for non-chronological backtracking and procedures for clause recording. In this paper we propose integrating some algebraic simplification techniques — namely twovariable equivalence and clause inference — within intelligent backtrack search algorithms. When integrated in SAT algorithms, these techniques target the simplification of a problem instance, reducing the associated search cost. With the obtained experimental results we show the importance of the proposed techniques, demonstrating that they are indeed applied in hard real-world problem instances.