conference paper published Tim Hansmeier author 499920000-0003-1377-3339 Marco Platzner author 398 David Andrews author 78 department ARC: International Symposium on Applied Reconfigurable Computing SFB 901 - Subproject B4 project SFB 901 project SFB 901 - Project Area B project Modern Boolean satisfiability solvers can emit proofs of unsatisfiability. There is substantial interest in being able to verify such proofs and also in using them for further computations. In this paper, we present an FPGA accelerator for checking resolution proofs, a popular proof format. Our accelerator exploits parallelism at the low level by implementing the basic resolution step in hardware, and at the high level by instantiating a number of parallel modules for proof checking. Since proof checking involves highly irregular memory accesses, we employ Hybrid Memory Cube technology for accelerator memory. The results show that while the accelerator is scalable and achieves speedups for all benchmark proofs, performance improvements are currently limited by the overhead of transitioning the proof into the accelerator memory. https://ris.uni-paderborn.de/download/3373/5257/AnFPGAHMC-BasedAcceleratorForR.pdf application/pdf Springer International Publishing2018Santorini, Greece eng 0302-9743 1611-3349 9783319788890 978331978890610.1007/978-3-319-78890-6_13 10824153-165 Hansmeier, Tim, Marco Platzner, and David Andrews. “An FPGA/HMC-Based Accelerator for Resolution Proof Checking.” In <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i>, 10824:153–65. Lecture Notes in Computer Science. Springer International Publishing, 2018. <a href="https://doi.org/10.1007/978-3-319-78890-6_13">https://doi.org/10.1007/978-3-319-78890-6_13</a>. T. Hansmeier, M. Platzner, D. Andrews, in: ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications, Springer International Publishing, 2018, pp. 153–165. T. Hansmeier, M. Platzner, and D. Andrews, “An FPGA/HMC-Based Accelerator for Resolution Proof Checking,” in <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i>, Santorini, Greece, 2018, vol. 10824, pp. 153–165. Hansmeier, T., Platzner, M., &#38; Andrews, D. (2018). An FPGA/HMC-Based Accelerator for Resolution Proof Checking. In <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i> (Vol. 10824, pp. 153–165). Santorini, Greece: Springer International Publishing. <a href="https://doi.org/10.1007/978-3-319-78890-6_13">https://doi.org/10.1007/978-3-319-78890-6_13</a> @inproceedings{Hansmeier_Platzner_Andrews_2018, series={Lecture Notes in Computer Science}, title={An FPGA/HMC-Based Accelerator for Resolution Proof Checking}, volume={10824}, DOI={<a href="https://doi.org/10.1007/978-3-319-78890-6_13">10.1007/978-3-319-78890-6_13</a>}, booktitle={ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications}, publisher={Springer International Publishing}, author={Hansmeier, Tim and Platzner, Marco and Andrews, David}, year={2018}, pages={153–165}, collection={Lecture Notes in Computer Science} } Hansmeier T, Platzner M, Andrews D. An FPGA/HMC-Based Accelerator for Resolution Proof Checking. In: <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i>. Vol 10824. Lecture Notes in Computer Science. Springer International Publishing; 2018:153-165. doi:<a href="https://doi.org/10.1007/978-3-319-78890-6_13">10.1007/978-3-319-78890-6_13</a> Hansmeier, Tim, et al. “An FPGA/HMC-Based Accelerator for Resolution Proof Checking.” <i>ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications</i>, vol. 10824, Springer International Publishing, 2018, pp. 153–65, doi:<a href="https://doi.org/10.1007/978-3-319-78890-6_13">10.1007/978-3-319-78890-6_13</a>. 33732018-06-27T09:30:24Z2022-01-06T06:59:13Z