{'fraction_non_alphanumeric': 0.018793273986152326, 'fraction_numerical': 0.0, 'mean_word_length': 4.8497109826589595, '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}}
Proposal of a compact and efficient SAT encoding using a numeral system of any base

This paper describes a new SAT encoding method, named compact order encoding, applicable to finite domain CSP. It is a generalization of log encoding (compact encoding) and order encoding which is adopted by an award-winning SAT-based CSP solver. The basic idea of the compact order encoding is the use of a numeral system of some base. Each integer variable is divided into some digits and each digit is encoded by using the order encoding. It generates much smaller SAT instances than the order encoding and more efficient SAT instances than the log encoding in general because it requires fewer carry propagations when using larger base than two. We confirmed these observations through the experimental results on some benchmarks, such as Open-Shop Scheduling problems. Especially for very large instances, our solver with MiniSat engine outperformed other encodings and the state-of-the-art CSP solvers choco and Mistral.