TY - CHAP A1 - Clausecker, Robert A1 - Reinefeld, Alexander T1 - Zero-Aware Pattern Databases with 1-Bit Compression for Sliding Tile Puzzles T2 - Proceedings of the Twelfth International Symposium on Combinatorial Search (SoCS 2019) Y1 - 2019 UR - https://aaai.org/ocs/index.php/SOCS/SOCS19/paper/view/18326 SP - 35 EP - 43 ER - TY - CHAP A1 - Clausecker, Robert A1 - Schintke, Florian T1 - A Measure of Quality for IDA* Heuristics T2 - Proceedings of the Fourteenth International Symposium on Combinatorial Search (SoCS 2021) Y1 - 2021 N1 - Best SoCS21 paper award SP - 55 EP - 63 ER - TY - GEN A1 - Clausecker, Robert T1 - The Quality of Heuristic Functions for IDA* N2 - The aim of this thesis is to deepen our understand of how IDA* heuristics influence the number of nodes expanded during search. To this end, we develop Korf's formula for the number of expanded nodes into a heuristic quality η which expresses the quality of a heuristic function as a constant factor on the number of expanded nodes, independent of a particular problem instance. We proceed to show how to compute η for some common kinds of heuristics and how to estimate η by means of a random sample for arbitrary heuristics. Using the value of η for some concrete examples, we then inspect for which parts of the search space the values of h(v) are particularly critical to the performance of the heuristic, allowing us to build better heuristics for future problems. This report originally appeared as a master thesis at Humboldt University of Berlin. T3 - ZIB-Report - 20-17 KW - IDA* heuristic search sampling random walks Y1 - 2020 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:0297-zib-78489 SN - 1438-0064 ER - TY - GEN A1 - Clausecker, Robert T1 - Notes on the Construction of Pattern Databases N2 - This report aims to explain and extend pattern databases as a tool in finding optimal solutions to combination puzzles. Using sliding tile puzzles as an example, an overview over techniques to construct and use pattern databases is given, analysed, and extended. As novel results, zero aware additive pattern databases and PDB catalogues are introduced. This report originally appeared as a bachelor thesis at Humboldt University of Berlin under the title Notes on the Construction of Tablebases. T3 - ZIB-Report - 17-59 KW - pattern-database 15-puzzle 24-puzzle ida* heuristic-search pdb-catalogue zpdb Y1 - 2017 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:0297-zib-65586 SN - 1438-0064 ER - TY - THES A1 - Clausecker, Robert T1 - Notes on the Construction of Tablebases Y1 - 2017 ER - TY - CHAP A1 - Kaiser, Benjamin A1 - Clausecker, Robert T1 - CleanMaple_PriPro, CaDiCaL_PriPro and CaDiCaL_PriPro_no_bin T2 - Proceedings of SAT Competition 2021 : Solver and Benchmark Descriptions Y1 - 2021 UR - http://hdl.handle.net/10138/333647 N1 - CaDiCaL_PriPro won the Special Innovation Price at the SAT Competition 2021 SP - 25 ER - TY - CHAP A1 - Clausecker, Robert A1 - Kaiser, Benjamin T1 - Sliding Tile Puzzles T2 - Proceedings of SAT Competition 2021 : Solver and Benchmark Descriptions Y1 - 2021 UR - http://hdl.handle.net/10138/333647 SP - 57 ER - TY - CHAP A1 - Kaiser, Benjamin A1 - Clausecker, Robert T1 - CleanMaple T2 - Proceedings of SAT Competition 2021 : Solver and Benchmark Descriptions Y1 - 2021 UR - http://hdl.handle.net/10138/333647 SP - 24 ER - TY - JOUR A1 - Clausecker, Robert A1 - Lemire, Daniel T1 - Transcoding unicode characters with AVX-512 instructions JF - Software: Practice and Experience N2 - Intel includes in its recent processors a powerful set of instructions capable of processing 512-bit registers with a single instruction (AVX-512). Some of these instructions have no equivalent in earlier instruction sets. We leverage these instructions to efficiently transcode strings between the most common formats: UTF-8 and UTF-16. With our novel algorithms, we are often twice as fast as the previous best solutions. For example, we transcode Chinese text from UTF-8 to UTF-16 at more than 5 GiB s−1 using fewer than 2 CPU instructions per character. To ensure reproducibility, we make our software freely available as an open-source library. Our library is part of the popular Node.js JavaScript runtime. Y1 - 2023 U6 - https://doi.org/10.1002/spe.3261 VL - 53 IS - 12 SP - 2430 EP - 2462 PB - John Wiley & Sons Ltd. ER - TY - CHAP A1 - Kaiser, Benjamin A1 - Clausecker, Robert A1 - Mavroskoufis, Michael T1 - Prioritised Unit Propagation by Partitioning the Watch Lists T2 - Proceedings of the 14th International Workshop on Pragmatics of SAT co-located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) N2 - Conflict Driven Clause Learning (CDCL) SAT solvers spend most of their execution time iterating through clauses in unit propagation. Efficient implementations of unit propagation mostly rely on the two watched literals (TWL) scheme, a specialised data structure watching two literals per clause to prevent as many clause lookups as possible. In this paper, we present Priority Propagation (PriPro)—a minimally invasive method to adapt unit propagation in existing SAT solvers. With PriPro the traditional TWL scheme is partitioned to allow for rearranging the order in which clauses are examined. This is used to achieve a prioritisation of certain clauses. Using PriPro in combination with a dynamic heuristic to prioritise resolvents from recent conflicts, the effectiveness of unit propagation can be increased. In the state-of-the-art CDCL SAT solver CaDiCaL modified to use PriPro, we obtained a 5–10 % speedup on the SAT Competition 2021 benchmark set in a fair comparison with the unmodified CaDiCaL. Y1 - 2023 UR - https://ceur-ws.org/Vol-3545/paper2.pdf VL - 3545 SP - 14 EP - 34 PB - CEUR Workshop Proceedings ER -