http://hdl.handle.net/10256.1/7702 Tue, 10 Feb 2026 06:26:39 GMT 2026-02-10T06:26:39Z http://diobma.udg.edu:443/bitstream/id/65129/ http://hdl.handle.net/10256.1/7702 http://hdl.handle.net/10256.1/7782 Closing Bofill, Miquel; Villaret i Ausellé, Mateu Miquel Bofill and Mateu Villaret close the Congress Tue, 03 Sep 2024 00:00:00 GMT http://hdl.handle.net/10256.1/7782 2024-09-03T00:00:00Z http://hdl.handle.net/10256.1/7781 Encoding the Hamiltonian Cycle Problem into SAT Based on Vertex Elimination Zhou, Neng-Fa Neng-Fa Zhou, from the City University of New York, presents a SAT encoding, called vertex elimination encoding (VEE), for the Hamiltonian Cycle Problem (HCP). The encoding maps a Hamiltonian cycle in the reduced graph after vertex elimination to a Hamiltonian cycle in the original graph. While VEE is not competitive for large dense graphs due to its large encoding sizes, it can be utilized to reduce graphs when they are sparse. This paper compares VEE with the distance encoding, and shows that the hybridization of these two encodings is effective for the benchmarks. For the knight's tour problem, in particular, the hybrid encoding solves some middle-sized instances that were beyond the reach for previous eager SAT encodings Tue, 03 Sep 2024 00:00:00 GMT http://hdl.handle.net/10256.1/7781 2024-09-03T00:00:00Z http://hdl.handle.net/10256.1/7780 Computing small Rainbow Cycle Numbers with SAT modulo Symmetries Kirchweger, Markus; Szeider, Stefan Markus Kirchweger from the Vienna University of Technology, tells that envy-freeness up to any good (EFX) is a key concept in Computational Social Choice for the fair division of indivisible goods, where no agent envies another's allocation after removing any single item. A deeper understanding of EFX allocations is facilitated by exploring the rainbow cycle number ($R_f(d)$), the largest number of independent sets in a certain class of directed graphs. Upper bounds on $R_f(d)$ provide guarantees the feasibility of EFX allocations (Chaudhury et al., EC 2021). In this work, we precisely compute the numbers $R_f(d)$ for small values of d, employing the SAT modulo Symmetries framework. SAT modulo Symmetries is specifically tailored for the constraint-based isomorph-free generation of combinatorial structures. We provide an efficient encoding for the rainbow cycle number, comparing eager and lazy approaches. To cope with the huge search space, we extend the encoding with invariant pruning, a new method that significantly speeds up computation Tue, 03 Sep 2024 00:00:00 GMT http://hdl.handle.net/10256.1/7780 2024-09-03T00:00:00Z http://hdl.handle.net/10256.1/7779 Exponential steepest ascent from valued constraint graphs of pathwidth four Kaznatcheev, Artem; Van Marle, Melle Melle van Marle from the University of Utrecht, Holland, tells us about the complexity of maximising fitness via local search on valued constraint satisfaction problems (VCSPs). We consider two kinds of local ascents: (1) steepest ascents, where each step changes the domain that produces a maximal increase in fitness; and(2) $\prec$-ordered ascents, where -- of the domains with available fitness increasing changes -- each step changes the $\prec$-minimal domain. We provide a general padding argument to simulate any ordered ascent by a steepest ascent. We construct a VCSP that is a path of binary constraints between alternating 2-state and 3-state domains with exponentially long ordered ascents. We apply our padding argument to this VCSP to obtain a Boolean VCSP that has a constraint (hyper)graph of arity 5 and pathwidth 4 with exponential steepest ascents. This is an improvement on the previous best known construction for long steepest ascents, which had arity 8 and pathwidth 7 Tue, 03 Sep 2024 00:00:00 GMT http://hdl.handle.net/10256.1/7779 2024-09-03T00:00:00Z