Solving Constrained Horn Clauses (CHCs) is a fundamental challenge behind a
wide range of verification and analysis tasks. Data-driven approaches show
great promise in improving CHC solving without the painstaking manual effort of
creating and tuning various heuristics. However, a large performance gap exists
between data-driven CHC solvers and symbolic reasoning-based solvers. In this
work, we develop a simple but effective framework, "Chronosymbolic Learning",
which unifies symbolic information and numerical data points to solve a CHC
system efficiently. We also present a simple instance of Chronosymbolic
Learning with a data-driven learner and a BMC-styled reasoner. Despite its
great simplicity, experimental results show the efficacy and robustness of our
tool. It outperforms state-of-the-art CHC solvers on a dataset consisting of
288 benchmarks, including many instances with non-linear integer arithmetics.

本论文提出了 Chronosymbolic Learning 这一基于数据驱动的框架，结合符号信息和数值数据点解决 Constrained Horn Clauses（CHC）系统，此工具在包含许多非线性整数算术实例的数据集上表现出比现有 CHC 求解器更高的性能。