Scholarlink

<p>Lazy clause generation (LCG) is an approach to building constraint programming (CP) solvers that uses ideas from Boolean Satisfiability (SAT) solvers. Propagation in the CP solver is extended to <i>explain</i> itself, lazily creating explanation clauses. This allows SAT style conflict analysis to be used to create clausal nogoods that record the reason for failure, and avoid the same failure in the future. LCG has proven to be a highly effective architecture, used in all most performant CP solvers. In this review we consider how LCG has been refined and expanded over the years since its invention.</p>

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

Lazy clause generation in retrospect

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年7月9日

查看全文
  • Olga Ohrimenko,
  • Peter J. Stuckey,
  • Michael Codish

摘要

Lazy clause generation (LCG) is an approach to building constraint programming (CP) solvers that uses ideas from Boolean Satisfiability (SAT) solvers. Propagation in the CP solver is extended to explain itself, lazily creating explanation clauses. This allows SAT style conflict analysis to be used to create clausal nogoods that record the reason for failure, and avoid the same failure in the future. LCG has proven to be a highly effective architecture, used in all most performant CP solvers. In this review we consider how LCG has been refined and expanded over the years since its invention.