2026· International Conference on Principles and Practice of Constraint Programming· pp. 42:1-42:21· 0 citations· 43 references
Computer Science
TL;DR
This work presents the first systematic analysis of how leading LCG solvers maintain their SAT encodings, based on source-code inspection and developer correspondence, and proposes a native CDCL framework for CP, replacing SAT literals with atomic constraints, enabling conflict analysis, nogood learning, and nogood propagation directly at the CP level.
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.
O. Ohrimenko, Peter James Stuckey, M. Codish· Constraints· 0 citations
This paper revisits previous work on ER, which factors out repeated parts of learned clauses during conflict analysis, and explores how their original strategy benefits from 15 years of improvements in the state-of-the-art solver CaDiCaL, and proposes a new, less intrusive inprocessing approach based on factoring XOR and ITE gates from learned clauses globally.
Florian Pollitt, Zachary Battleman, Mathias Fleury et al.· International Conference on...· 1 citation
On a new benchmark of 77 problems with an exact oracle, translation to Answer Set Programming is faithful on six of seven domains and fails only on aggregate coverage scheduling, which concentrates the translation tax in one diagnosable pattern.
FLEX is presented, a foundational Constrained Horn Clause (CHC) solver implemented in LEAN, that reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code, via three contributions.
J. Khan, Petros Markopoulos, Nicolás Lehmann et al.· 0 citations
Large language models can derive a plausible mathematical object yet still violate explicit requirements--for example, by omitting a modular reduction, returning a non-integer, or using the wrong encoded answer form. We introduce Constraint-First Reasoning (CFR), a training-free two-stage prompting protocol: Stage 1 extracts and summarizes constraints entailed by the problem, and Stage 2 solves while checking intermediate and final results against that summary. Routed-CFR activates the two-stage protocol only when a text-only regex router detects restrictive cues; otherwise it uses direct chain-of-thought (CoT). Across AIME, CMIMC, BRUMO, and AIMO_AMC, the method improves direct CoT on multiple backbones. We further report convention-controlled routing experiments, matched prompting baselines, problem-level paired tests, decoding robustness, constraint-quality audits, total-token accounting, and an OlympiadBench evaluation. These analyses position CFR as a targeted test-time intervention whose benefit depends on recoverable constraints and reliable Stage 1 extraction, rather than as a general-purpose replacement for mathematical reasoning.
Hongbo Ma, Bang Yang, Y. Cheng et al.· 0 citations
This work presents a pipeline that combines LLM-based constraint generation with empirical evaluation and formal verification, and handles MiniZinc’s partial semantics by requiring the base model to be safe and separately proving that the proposed constraint is well-defined for all instances and solutions of the base model.
Philipp Danzinger, Nysret Musliu· International Conference on...· 0 citations