Modern combinatorial solvers can be understood as searching for proofs of unsatisfiability or optimality. The proof system implemented by a solver, therefore, fundamentally shapes solver performance. While propositional resolution is simple and complete for propositional formulas, no existing practical resolution-based system offers unrestricted complete reasoning over integer linear inequalities. We introduce hypercube linear resolution, a new proof system that is both sound and complete for integer linear reasoning. Hypercube linear resolution integrates propositional resolution with Fourier resolution through a new constraint type, the hypercube linear constraint, which captures linear relations within a discrete hypercube. Our main contribution is the theory of the proof system, establishing its soundness and completeness. Our proof system generalises propositional and Fourier resolution, and can be seen as an extended cutting planes proof system. We also provide a conflict-driven search algorithm that exploits the system in practice. Our preliminary experiments demonstrate that the new system reduces conflicts compared to propositional resolution. This shows that the structure captured by hypercube linear constraints can be exploited to improve constraint solving.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Resolution Meets Cutting Planes: Introducing Hypercube Linear Resolution

  • Maarten Flippo,
  • Peter J. Stuckey,
  • Emir Demirović

摘要

Modern combinatorial solvers can be understood as searching for proofs of unsatisfiability or optimality. The proof system implemented by a solver, therefore, fundamentally shapes solver performance. While propositional resolution is simple and complete for propositional formulas, no existing practical resolution-based system offers unrestricted complete reasoning over integer linear inequalities. We introduce hypercube linear resolution, a new proof system that is both sound and complete for integer linear reasoning. Hypercube linear resolution integrates propositional resolution with Fourier resolution through a new constraint type, the hypercube linear constraint, which captures linear relations within a discrete hypercube. Our main contribution is the theory of the proof system, establishing its soundness and completeness. Our proof system generalises propositional and Fourier resolution, and can be seen as an extended cutting planes proof system. We also provide a conflict-driven search algorithm that exploits the system in practice. Our preliminary experiments demonstrate that the new system reduces conflicts compared to propositional resolution. This shows that the structure captured by hypercube linear constraints can be exploited to improve constraint solving.