Strong Bridges for the Circuit Constraint
Implementing and Evaluating Strong Bridge Detection in a Lazy Clause Generation Solver
M.J.C. van Leest (TU Delft - Electrical Engineering, Mathematics and Computer Science)
E. Demirović – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
I.C.W.M. Marijnissen – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
M.A. Costea – Graduation committee member (TU Delft - Electrical Engineering, Mathematics and Computer Science)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Constraint Programming with Lazy Clause Generation (LCG) relies on effective propagation to reduce the search space. We study the integration of strong bridge detection into a circuit propagator, where strong bridges identify edges that must be present to maintain strong connectivity in the graph induced by current domains. Compared to a baseline that only prevents subcycles, this approach substantially reduces search effort, with reductions of up to three orders of magnitude in the satisfaction setting and one order of magnitude in the optimization setting. These gains often translate into runtime improvements, particularly for satisfaction. The extension also produces shorter nogoods, while its effect on LBD is mixed, reflecting more global explanations. Overall, the results demonstrate that identifying necessary edges is an effective way to strengthen propagation and significantly reduce the explored search space.