In many QBF encodings, sequences of Boolean variables stand for binary representations of integer variables. Examples are state labels in bounded model checking or actions in planning problems. Often not the full possible range is used, e.g., for representing six different states, three Boolean variables are required, rendering two of the eight possible assignments irrelevant for the solution of the problem. As QBF solvers do not have any domain-specific knowledge on the formula they process, they are not able to detect this pruning opportunity. In this paper, we introduce the idea of int-splits, which provide domain-specific information on integer variables to QBF solvers. This is particularly appealing for parallel Divide-and-Conquer solving which partitions the search space into independently solvable sub-problems. Using this technique, we reduce the number of generated sub-problems from a full expansion to only the required subset. We then evaluate how many resources int-splits save in problems already well suited for D&C. In that context, we provide a reference implementation that splits QBF formulas into many sub-problems with or without int-splits and merges results. We finally propose a comment-based optional syntax extension to (Q)DIMACS that includes int-splits and is suited for supplying proposed guiding paths natively to D&C solvers.

翻译：在许多QBF编码中，布尔变量序列用于表示整型变量的二进制编码，例如有界模型检验中的状态标签或规划问题中的动作。实际应用中往往不会使用完整的数值范围，如表示六个不同状态需要三个布尔变量，导致八个可能赋值中有两个与问题求解无关。由于QBF求解器缺乏处理公式的领域知识，无法自动识别这一剪枝机会。本文提出整数拆分（int-splits）的概念，为QBF求解器提供整型变量的领域特定信息。这一方法对并行分治求解尤为适用，该策略将搜索空间划分为可独立求解的子问题。通过该技术，我们将生成的子问题数量从完全展开缩减为仅包含必要子集。我们评估了整数拆分在已适合分治策略的问题中所节省的资源，并提供了将QBF公式拆分为多个子问题的参考实现（支持/不支持整数拆分及结果合并）。最后，我们提出一种基于注释的(Q)DIMACS可选语法扩展，该扩展支持整数拆分且适于为分治求解器原生提供引导路径。