Propagating Regular Counting with Lazy Clause Generation
DFA vs counter-DFA for finite domain satisfaction problems
D.G.S. Ravensbergen (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
cDFAs offer a more natural encoding of counting regular patterns—a prevalent problem in timetabling and sequencing—than widely-used DFAs. A cDFA-based propagator for finite domain constraint solving has been shown to solve satisfaction problems faster and make more propagations than the decomposition of a DFA-based regular constraint. This paper extends that algorithm with explanations for lazy clause generation and shows that it often solves satisfaction problems faster than a DFA-based regular constraint both decomposed and propagated, even though the explanations are simple and nogood quality is worse. Additionally, this paper showcases a generator for cDFAs and DFAs that are equivalent to each other to aid comparison of the constraints