Circular chromatic index of small snarks DuΕ‘an BernΓ‘t1 , JΓ‘n MazΓ‘k1,* 1 FMFI UK, Bratislava, Slovakia Abstract This paper verifies and extends previous computational results on circular chromatic index of small snarks, gives further support for certain conjectures, and discusses various practical aspects of using SAT solvers to solve graph colouring problems (e.g. the impact of solver choice and Boolean formula construction on running time). Keywords cubic graph, snark, circular chromatic index, SAT solver 1. Introduction This paper focuses on circular chromatic index πœ’β€²π‘ , which is a refinement of chromatic index that allows real The main aim of this article is to popularize the usage of values as colours instead of just integers. For π‘Ÿ β‰₯ 1, SAT solvers for computations in combinatorics. For more a circular π‘Ÿ-edge-colouring of a graph 𝐺 is a mapping than a decade, SAT solvers have been among the most 𝑐 : 𝐸(𝐺) β†’ [0, π‘Ÿ) such that 1 ≀ |𝑐(𝑒) βˆ’ 𝑐(𝑓 )| ≀ π‘Ÿ βˆ’ 1 efficient tools for problems in discrete mathematics, and for any two incident edges 𝑒 and 𝑓 of 𝐺. If a graph 𝐺 has there are plenty of them freely available. However, many a circular π‘Ÿ-edge-colouring, we say that it is circularly researchers in the area, both young and more experi- π‘Ÿ-edge-colourable. The circular chromatic index πœ’β€²π‘ of 𝐺 enced, are still not sufficiently aware of their advantages is the infimum of all π‘Ÿ such that 𝐺 has a circular π‘Ÿ-edge- and the simplicity of their use. We will illustrate the colouring. This infimum is in fact a minimum; for a finite usage of SAT solvers through computations concerned graph it is always attained. Moreover, it is rational, and with edge-colourings of graphs. the only possible candidates for πœ’β€²π‘ (𝐺) are fractions 𝑝/π‘ž Cubic graphs that do not admit a 3-edge-colouring such that 𝑝 ≀ |𝐸(𝐺)|. Circular colourings can be used (so-called uncolourable) have been studied for more than for optimization in certain types of scheduling problems, a century, initially in connection with the Four Colour but we are not exploring this in this paper. For a detailed Problem, and more recently in the context of flows and introduction to circular colourings, we refer the reader cycle covers. In this article, a snark is a bridgeless simple to the survey [4]. cubic graph with chromatic index 4. Since the problem of Colourable cubic graphs have πœ’β€²π‘ = 3, while snarks determining the chromatic index of a cubic graph is NP- have πœ’β€²π‘ > 3, so πœ’β€²π‘ is also a β€œmeasure of uncoloura- complete, we cannot expect a simple characterization bility”, perhaps the most natural one. Snarks with πœ’β€²π‘ of snarks, and volumes have been written on various close to 3 are plentiful, whereas snarks with πœ’β€²π‘ above attempts to gain a better understanding of their structure 10/3 seem rare. This is partly known, partly hypothe- [1]. sized. An intuition behind this statement is as follows: One possible approach is to acknowledge that β€œnot In a 3-edge-colouring, when you fix the colours of two all snarks are of the same difficulty” and introduce a edges at a vertex, the colour of the third edge is uniquely measure that somehow splits snarks into classes with determinedβ€”there is no wiggle room. But in a circu- β€œincreasing levels of uncolourability” [2]. For instance, lar (3 + πœ€)-edge-colouring, there is typically a small in- if we consider the minimum number of odd cycles in a terval of length up to πœ€ for allowed values of the third 2-factor of a cubic graph (its oddness), there are cubic colour. With a bit of flexibility at each vertex, over a large graphs with oddness 2π‘˜ for every non-negative integer enough subgraph, we can gradually shift the colours into π‘˜. For π‘˜ = 0, we get colourable graphs, and presumably pretty much anything we want on the edges leaving the as oddness increases, the difficulty of proving theorems subgraph, making it easy to get a circular (3 + πœ€)-edge- for such snarks increases: e.g. the 5-flow conjecture was colouring of the whole large graph even for a small value gradually proved for snarks with oddness 0, 2, and 4 [3]. of πœ€. Of course, there are situations where this does not CADM’24: Computational Aspects of Large-Scale Problems in Discrete applyβ€”for instance, if we have a small subgraph that Mathematics, ITAT 2024 cannot be coloured with 3 + πœ€ colours for a small πœ€, it * Corresponding author. will ensure a lower bound on πœ’β€²π‘ for the whole graph. $ dusan.bernat@fmph.uniba.sk (D. BernΓ‘t); The following theorems and conjectures summarize jan.mazak@fmph.uniba.sk (J. MazΓ‘k)  0000-0002-6498-9984 (J. MazΓ‘k) the current state of knowledge about πœ’β€²π‘ of cubic graphs. Β© 2024 Author:Pleasefillinthe\copyrightclause macro CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) Theorem 1 ([5]). There is no graph with πœ’β€²π‘ ∈ (11/3, 4). CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings Theorem 2 ([6, 7]). The Petersen graph has πœ’β€²π‘ = 11/3. colour and that no two incident edges can be assigned There exists an infinite class of snarks with connectivity 3 colours with difference less than π‘ž (using clauses like and πœ’β€²π‘ = 7/2. Β¬π‘₯𝑒,0 ∨ Β¬π‘₯𝑒,1 ). Then a SAT solver is used to decide the satisfiability of the problem instance. As explained in Theorem 3 ([8]). For every πœ€ > 0, there exists an integer Section 1, there are finitely many candidates for fractions 𝑔 such that every snark with girth at least 𝑔 has πœ’β€²π‘ ≀ 3+πœ€. 𝑝/π‘ž and some bounds can be set based on the size of the input graph, so it is possible to determine πœ’β€²π‘ by sub- Theorem 4 ([6]). The circular chromatic index of every sequently solving several SAT instances. This type of snark with girth at least 6 is at most 7/2. problem is often solved by a binary search (we order the possible fractions from the lowest to the highest, look Theorem 5 ([9]). For every rational π‘Ÿ ∈ (3, 10/3) βˆͺ {3 + into the middle etc.), but it would be suboptimal in this 𝑝/(3𝑝 βˆ’ 1) | 𝑝 ∈ Z+ }, there exists a snark with πœ’β€²π‘ = π‘Ÿ. case, as we explain in the next paragraph. The time required to solve a particular instance for Conjecture 1 ([6, 7]). The circular chromatic index of a given graph highly depends on 𝑝: a large value of 𝑝 every snark 𝐺 except the Petersen graph is at most 7/2. If results in a large number of variables, which is the biggest 𝐺 is cyclically 4-connected, πœ’β€²π‘ (𝐺) < 7/2. determinant of time complexity (Section 4.2 gives more It is still open if the Petersen graph is the only graph details on this). Our experiments clearly indicate that we with πœ’β€²π‘ = 11/3. Based on our computational results, we need to reduce the number of instances with large values propose two additional conjectures and one problem. of 𝑝 as much as possible during a search for πœ’ β€² 𝑐 . There are two other factors at play, but both play a minor role. The Conjecture 2. If 𝐺 is a snark with girth at least 6, then first is that the time increases when the tested fraction πœ’β€²π‘ (𝐺) ≀ 10/3. is near πœ’β€²π‘ β€”when the value is far below πœ’β€²π‘ , the solver can quickly recognise unsatisfiability; when the fraction The evidence for Conjecture 2 is somewhat scarce: it is too far above πœ’β€² , it is easy to find a colouring. The 𝑐 holds for Isaacs snarks with girth 6 (though not for those second is specific to circular colourings: fractions of the of smaller girth), and we verified it for all 42 snarks with form 3 + 1/π‘˜ are easier to exclude than 3 + 2/π‘˜, 3 + 3/π‘˜ girth 6 on at most 38 vertices and an incomplete list of etc. because there is less flexibility in colouring edges snarks on 40 to 44 vertices (all of them being the result incident to a vertex. Based on these observations, we use of a dot product applied to smaller snarks). Weak indirect a heuristic that always starts testing for the fraction with support is also provided by Theorems 3 and 4. the smallest numerator. Conjecture 3. All cyclically 4-connected snarks 𝐺 have πœ’β€²π‘ (𝐺) ≀ 17/5. 3. Results of computations Problem 4. Characterise cyclically 4-connected snarks The exhaustive lists of snarks with given order and cyclic 𝐺 with πœ’β€²π‘ (𝐺) > 10/3. Is the set 𝑀>10/3 of such snarks connectivity we used come from [10]. The counts of cycli- finite? Is the set of the values of πœ’β€²π‘ of such snarks finite? cally 4-connected snarks with girth 5 up to 30 vertices We have found 17 members of 𝑀>10/3 , described in with particular πœ’π‘ were presented in [11]. The results of β€² more detail in Section 3. this diploma thesis were not published properly and per- haps are not widely known. We have fully confirmed the results of [11] and extended them for snarks of girth 4, 2. Computing πœ’β€²π‘ see Table 1 (rows are ordered according to the increasing value of πœ’β€²π‘ ). In light of the conjectures in Section 1, our computations All the results presented in this section were obtained are primarily focused on proving that there are no snarks using the CaDiCaL_vivinst, one of the winning solvers with πœ’π‘ bigger than some value π‘Ÿ. This is the easier of the 2023 SAT Competition [12]. We used a machine β€² thing to doβ€”one only needs to find a suitable circular with 20 cores (Intel Xeon Gold 5220R CPU @ 2.20GHz). π‘Ÿ-edge-colouring. On the other hand, determining πœ’β€²π‘ Because the computations for different graphs are com- requires proving a lower bound, which takes much more pletely independent, the jobs within a batch are well time. Anyway, where computationally feasible, we fully suited for parallelisation, yielding the speedup approach- determine πœ’β€²π‘ , not just verify the conjectures. ing the number of CPU cores. The most demanding batch For a given input graph and a fraction 𝑝/π‘ž, we con- comprised all snarks of order 30 and girth greater or equal struct a boolean formula that is satisfiable if and only to 4; it took two weeks to complete. We verified the com- if 𝐺 is circularly 𝑝/π‘ž-edge-colourable. This formula puted indices by using SBVA combined with Kissat [12], uses a variable π‘₯𝑒,𝑐 for each element (𝑒, 𝑐) ∈ 𝐸(𝐺) Γ— but so far only with the same formula-generation algo- {0, 1, . . . 𝑝 βˆ’ 1}; it states that each edge gets exactly one Table 1 We suggest starting with a formula minimizing Counts of snarks with girth at least 4 and specific πœ’β€²π‘ . the chance of a mistake (either conceptual or in implementationβ€”we made plenty of both kinds, so do not Order 10 18 20 22 24 26 28 30 underestimate it, and if you can, make sure you verify πœ’β€²π‘ your implementation against some independently ob- 16/5 - - - - - - - 3 tained data). Of course, it pays off to employ known 29/9 - - - - - 1 - 13 tricks allowing translation of disjunctive normal forms 13/4 - - - - - 17 849 24070 into small equisatisfiable conjunctive normal forms1 , 36/11 - - - - - - - 1 thus avoiding the exponential blowup in the number 23/7 - - - - 19 396 5438 61838 33/10 - - - - - - - 2 of clauses. 10/3 - 1 5 29 136 883 6229 53925 17/5 - - 1 2 - - 1 2 4.2. Number of variables and clauses 7/2 - 1 Internally, almost all current leading SAT solvers use the 11/3 1 CDCL algorithm. They thus learn new clauses along the way and operate with many clauses that were not part of the original input. Consequently, including some seem- rithm; we are working on additional verification and ingly redundant clauses in the input might even help extension of the results to snarks on 32 or more vertices. (though it usually does not). Also, solvers use prepro- On the other hand, our code is completely independent of cessing which significantly rewrites the given formula: what KunertovΓ‘ used, and the results also agree with the- while colouring problems typically yield clauses of size 2 oretically determined indices for graphs that we checked and 3, it seems solvers prefer bigger clauses of size about (e.g. Isaacs and generalized BlanuΕ‘a snarks), which gives 10 (at least in the couple of situations we were able to us confidence in the results. check). Thanks to technical tricks like watched literals, Conjecture 3 suggests that non-trivial snarks with the clauses are not manipulated over and over, but are πœ’β€²π‘ > 10/3 are quite exceptional. This is supported accessed only when relevant. The takeaway here is that also by Table 1 which is sorted by index value. The mem- the number of clauses is of very little practical concern bers of the set 𝑀>10/3 from Section 1 are below a line: (unless it is really extreme). the Petersen graph, the type 2 BlanuΕ‘a snark, the flower On the other hand, the number of variables is criti- snark on 20 vertices and five other snarks on 22, 28 cal because it affects the depth (and thus the number and 30 vertices. Additional computations for all cycli- of nodes) of the CDCL search tree. For SAT instances cally 4-connected snarks on up to 36 vertices (girth at derived from graphs, the number of variables is typically least 4) identified one more snark of order 34 and two some polynomial dependent on the size π‘š of the graph, snarks of order 36 with πœ’β€²π‘ = 17/5. In the incomplete say, π‘šπ‘˜ . The resulting theoretical worst-case complexity set of generated snarks of order 38, there were six ad- π‘˜ of roughly 1.3π‘š seems terrifying, but in practice, SAT ditional snarks (three of them have πœ’β€²π‘ = 27/8, three solvers do much better. We will illustrate this with our of them have πœ’β€²π‘ = 37/11). All these snarks are avail- experience with several problems on cubic graphs. able at https://github.com/janmazak/research-data (see circular_chromatic_index). β€’ For 3-edge-colouring with integer colours, π‘˜ = 1. Solvers easily beat other approaches2 and can deal with graphs with hundreds or even thousands of 4. SAT solvers for graph theory vertices. β€’ For circular edge-colouring, the number of 4.1. Construction of Boolean formulas colours linearly depends on the size of the graph, We experimented with different ways of constructing and we need a variable for each pair [edge, Boolean formulas capturing 3-edge-colouring of cubic colour], so π‘˜ = 2 at worst. The number of clauses graphs. For instance, one can say that for every colour 𝑐 is cubic. Solvers work decently for small graphs, and every two incident edges, at least one of the edges but somewhere around 60 edges the computa- does not have colour 𝑐. Or that every colour is used on the tion time significantly increases (from minutes three edges incident to a vertex at least once; or some- to days per single graph). However, solvers are thing based on combinatorial nullstellensatz etc. The running times were very similar, somewhat depended on 1 For instance, the Tseytin transformation, or the approach men- the input graphs, and our experiences show that arcane tioned in https://en.wikipedia.org/wiki/Conjunctive_normal_form# Other_approaches. ways of formula construction are likely not worth it for 2 Except tiny graphs and possibly except a recent algorithm based smaller-scale computations. on path-width decomposition [13]. Table 2 Comparison of SAT solvers. Consumed CPU time in seconds for πœ’β€²π‘ of all snarks of order 24 and girth greater or equal to 4. Solver lingeling MergeSat Kissat Kissat Kissat CaDiCaL SeqFROST (2017) (two threads* ) 3.1.0 hywalk-exp MAB_DeepWalk+ vivinst T[s] 3024 7431 2575 1906 1880 2096 958 T/Tβ€² [%] 144 355* 123 91 90 100 46 S20 16 18 14 17 16 15 15 much faster than our backtracking algorithm3 at tually shorter, in theory, the real time might be half of that threshold. the CPU time. The Kissat variants do about 10% better β€’ For Hamiltonian cycles, the best formula con- than the CaDiCaL. The solver lingeling used in previous struction we are aware of uses variables for pairs work is about 7 years old but was only 1.5 times slower. [vertex, order of vertex along the cycle], i.e. π‘˜ = The SeqFROST solver appeared to do much better on our 2. The number of clauses is also cubic. Again, benchmark task than the reference SAT solver. Repeated there is a threshold around 60–75 vertices after runs for each solver gave almost the same results, the which computation takes days for a single graph. differences in time consumption were all less than 0.5%. In contrast to circular colouring, backtracking In another experiment we let the solvers search for competes with solvers fairly well. πœ’β€²π‘ of one single graph on 36 vertices with girth 5 (the result is 10/3). The results presented in Table 3 show In summary, SAT solvers are likely to be all you would a different perspective than previous benchmark. For ever need if you can keep the number of variables linear. this kind of task, all solvers except plain Kissat beats the If quadratic, they are helpful, but large graphs (some- CaDiCaL. Even several years old lingeling was almost where above 50–80 edges) are out of their reach, and twice as fast. For MergeSat, the total time consumed you are likely to run into trouble if you want to do com- by two threads is shown, while the running time was putations for sizeable complete lists of graphs of a given only 1304 seconds, which is 44% of the time needed order. by CaDiCaL. Interestingly, SeqFROST4 repeated the best performance as it took only one quarter of the time of 4.3. Which solver should I use? the reference solver. For computations taking hours, solver selection is not We conducted several simple experiments in order to eval- worth the effort. But for longer tasks taking weeks, it uate different SAT solvers. We considered state-of-the-art is likely to pay off. A reasonable way is to randomly solvers available from the website of SAT Competition pick a small sample of the instances in question and test [12]. We included also lingeling, used in the 2017 work them on solvers that are available. A word of warning: [11]. The criterion we used was the overall CPU user time solvers might contain rarely-encountered bugs; it has consumed by all the spawned processes. The test case for happened in the past for the solvers submitted to the performance evaluation was the computation of πœ’β€²π‘ for all competition. So in situations where you are proving cyclically 4-connected snarks on 24 vertices. There are something for all instances, it would be better to stay 155 such graphs and the computation for each of them with a more mainstream and seasoned solver; if you are involved solving several SAT instances as explained in trying to just find some suitable object that can be verified Section 2. later, possible bugs in a freshly implemented solver are The results are shown in Table 2 which shows total run not a critical problem. time 𝑇 and comparison to the CaDiCaL_vivinst, denoted 𝑇 β€² , which was one of the winners of the competition (the third place in main track). The table also shows 4.4. Should I strive for the best solver the speedup achieved on the 20 CPU machine denoted configuration? 𝑆20 . At first sight, the MergeSat solver looks like quite We experimented with tweaking configurable solver pa- a bad choice but as it was always using two computa- rameters a bit (for instance, lingeling has hundreds of tional threads the real time of result delivery was ac- them). The best speedup we were able to get is 2-4x for 3 The algorithm first constructs a linear ordering of edges such that a single graph and less than 2x for a large set of graphs. the next edge in the ordering has the most incident edges among the However, it is unclear if the gains are transferable to edges already included in the ordering, and then tries all possible other input instances. For instance, the distribution of colours for each edge in the ordering subsequently, backtracking 4 when a colouring conflict arises. Our other attempts at backtracking A winner of SAT Competition 2022, https://gears.win.tue.nl/papers/ did not yield anything meaningfully faster. sc2022_seqfrost.pdf, https://github.com/muhos/SeqFROST Table 3 Comparison of SAT solvers. Consumed CPU time in seconds for πœ’β€²π‘ of one snark on 36 vertices with girth 5. Solver lingeling MergeSat Kissat Kissat Kissat CaDiCaL SeqFROST (2017) (two threads* ) 3.1.0 hywalk-exp MAB_DeepWalk+ vivinstβ€² T[s] 1599 2387 3758 1917 2220 2943 775 T/Tβ€² [%] 54 81* 128 65 75 100 26 graph features allowing the speedup for smaller graphs solver by repeatedly adding clauses excluding already might be different for larger graphs. Additionally, fine- found solutions to the input formula). There is a fair tuning the parameters takes quite some time because chance this might work if the number of solutions is in of the necessary repeated solver runs. Overall, if your thousands or perhaps millions. With billions of solutions computations are going to run for weeks, it might be (or larger input instances in general), solvers tend to run worthwhile to work on this, but for quick verification out of memory or experience a significant slowdown. of conjectures and the like, not really. Also, note that As an example of this method, it is much easier to in Section 4.3, lingeling turned out to be slow for small describe a 2-factor than a Hamiltonian cycle (because instances, but fast for large instances, thus solver config- the conditions encoded into the Boolean formula are uration should be focused on bigger instances primarily local, around a single vertex)β€”the resulting formula has a or even exclusively. linear number of variables. For each 2-factor 𝐹 computed Your time might be better spent on trying to break the by an AllSAT solver, we then check if 𝐹 is connected. symmetry of your Boolean formulas [14]. For instance, This approach is comparable to or even somewhat faster for circular edge-colouring, one can pre-colour an edge than direct SAT solving for cubic graphs with around 30 with 0 without a loss of generality, and immediately get vertices, but it fails for graphs above 40 vertices because rid of a handful of variables, potentially gaining a better the number of 2-factors grows exponentially [16]. speedup than anything that could be gained by tweaking One possible reason for the success of generic SAT solver parameters. solvers on graph problems (versus other approaches tai- Our experience with parallelism is that it does not pay lored to solve specific problems) is that a solver can see off to use multiple threads per single SAT instance. It more than is obvious. We have experienced this when seems preferable to solve many instances in parallel, each considering an alternative approach to colourings: in- in its own thread. stead of running an exponential algorithm on the whole graph at once, what if we split the graph along a small 4.5. Alternatives to SAT cut, ran the slow algorithm on the much smaller parts separately, and then combined the results? It turned out KunertovΓ‘ [11] described several alternatives for comput- it is no big win (unless the graph in question contains ing πœ’β€²π‘ , some of them with measurements of computation many isomorphic subgraphs), possibly because all the time. It seems that they all fall far short of SAT solvers small cuts are reflected in the Boolean formula (as subsets (unless we are talking about very small instances, where of clauses barely sharing variables), and thus the solver backtracking is king). These alternatives typically rely can work with all the cuts as it sees fit anyway. Also, on some specific properties of circular colourings, so are leading solvers include tricks like random restarts, so not generalizable and we will not discuss them. One of e.g. if the colouring conflict is in a specific subgraph, the the approaches, though, deserves attention. solver does not get stuck outside of this subgraph for too For a graph 𝐺 with πœ’β€²π‘ (𝐺) = π‘Ÿ, one way to prove long. the lower bound is to refute the existence of an π‘Ÿβ€² -edge- SAT solvers also have a disadvantage: there is no ef- colouring for π‘Ÿβ€² being the largest relevant fraction smaller fective way of reporting computation progress (unlike than π‘Ÿ. Another is finding all π‘Ÿ-edge-colourings of 𝐺 and for plain backtracking having at least a somewhat bal- checking that each of them contains a so-called tight anced search tree). In case one wants to solve a single cycle. While it is not particularly fruitful for circular particularly hard instance, when does one give up?. . . colourings [11], it might sometimes be the most efficient A note on integer/mixed linear programming (ILP): approach for graphs of limited size. The problem of find- every SAT instance can be expressed as a problem of ing all satisfying assignments to a given Boolean formula ILP, and there are powerful ILP solvers, so ILP might be is called AllSAT and there are specialized solvers for it worth a try for your problem. Our limited experience [15], although not many, and they are not heavily em- shows that ILP is significantly slower, and it comes with ployed, so there are concerns about reliability (but any numerical and rounding problems, so perhaps the best ordinary SAT solver can be easily turned into an AllSAT use of it would be for refuting working hypotheses or for guessing optimal values which are then proved otherwise [8] T. Kaiser, D. KrΓ‘l’, R. Ε krekovski, X. Zhu, The circu- (by hand or using a SAT solver). lar chromatic index of graphs of high girth, Journal Our feeling is that a SAT solver should perhaps be the of Combinatorial Theory, Series B 97 (2007) 1–13. first tool to try (unless there exists a solver specifically doi:10.1016/j.jctb.2006.03.002. designed or easily adaptable for your purpose, e.g. for [9] R. LukoΕ₯ka, J. MazΓ‘k, Cubic graphs with given the travelling salesman problem). circular chromatic index, SIAM Journal on Discrete Mathematics 24 (2010) 1091–1103. doi:10.1137/ 090752316. Acknowledgments [10] K. Coolsaet, S. D’hondt, J. Goedgebeur, House of graphs 2.0: A database of interesting graphs and We thank J. KarabΓ‘Ε‘, R. LukoΕ₯ka, and R. Nedela for in- more, Discrete Applied Mathematics 325 (2023) teresting discussions related to the topics covered in this 97–107. doi:10.1016/j.dam.2022.10.013. article. [11] O. KunertovΓ‘, Circular chromatic index of small This work was partially supported from the research snarks, Diploma thesis supervised by J. MazΓ‘k, 2017. grants APVV-19-0308, VEGA 1/0743/21, VEGA 1/0727/22 URL: http://www.dcs.fmph.uniba.sk/diplomovky/ and Operational Program Integrated Infrastructure for obhajene/getfile.php/kunertova.pdf?id=426&fid= the project Advancing University Capacity and Compe- 756&type=application%2Fpdf. tence in Research, Development a Innovation (ACCORD, [12] T. Balyo, M. Heule, M. Iser, M. JΓ€rvisalo, M. Suda ITMS2014+:313021X329), co-financed by the European (Eds.), Proceedings of SAT Competition 2023: Regional Development Fund. Solver, Benchmark and Proof Checker Descriptions, Part of the research results was obtained using the Department of Computer Science Series of Publica- computational resources procured in the national project tions B, Department of Computer Science, Univer- National competence centre for high performance com- sity of Helsinki, Finland, 2023. puting (project code: 311070AKF2) funded by European [13] R. LukoΕ₯ka, J. TΔ›tek, A 3-edge-coloring algorithm, Regional Development Fund, EU Structural Funds In- Bordeaux Graph Workshop (2019). URL: https:// formatization of society, Operational Program Integrated bgw.labri.fr/2019/booklet.pdf. Infrastructure. [14] H. Metin, S. Baarir, M. Colange, F. Kordon, Cd- clsym: Introducing effective symmetry breaking in References sat solving, in: D. Beyer, M. Huisman (Eds.), Tools and Algorithms for the Construction and Analy- [1] J. MazΓ‘k, J. RajnΓ­k, M. Ε koviera, Morphology of sis of Systems, Springer International Publishing, small snarks, Electronic Journal of Combinatorics Cham, 2018, pp. 99–114. 29(4) (2022) P4.30. [15] T. Toda, T. Soh, Implementing efficient all solutions [2] J. KarabΓ‘Ε‘, E. MÑčajovΓ‘, R. Nedela, M. Ε koviera, sat solvers, ACM J. Exp. Algorithmics 21 (2016). Girth, oddness, and colouring defect of snarks, Dis- doi:10.1145/2975585. crete Mathematics 345 (2022) 113040. doi:10.1016/ [16] L. Esperet, F. KardoΕ‘, A. D. King, D. KrΓ‘ΔΎ, S. Norine, j.disc.2022.113040. Exponentially many perfect matchings in cubic [3] G. Mazzuoccolo, E. Steffen, Nowhere-zero 5- graphs, Advances in Mathematics 227 (2011) 1646– flows on cubic graphs with oddness 4, Journal 1664. doi:10.1016/j.aim.2011.03.015. of Graph Theory 85 (2017) 363–371. doi:10.1002/ jgt.22065. [4] X. Zhu, Circular chromatic number: a survey, Discrete Mathematics 229 (2001) 371–410. doi:10. 1016/S0012-365X(00)00217-X. [5] P. Afshani, M. Ghandehari, M. Ghandehari, H. Hatami, R. Tusserkani, X. Zhu, Circular chro- matic index of graphs of maximum degree 3, Jour- nal of Graph Theory 49 (2005) 325–335. [6] D. KrΓ‘ΔΎ, E. MÑčajovΓ‘, J. MazΓ‘k, J.-S. Sereni, Circular edge-colorings of cubic graphs with girth six, Jour- nal of Combinatorial Theory, Series B 100 (2010) 351–358. doi:10.1016/j.jctb.2009.10.003. [7] J. MazΓ‘k, Circular edge-colourings of cubic graphs, PhD thesis, 2011.