Abstract
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.
This work was partially supported by the German Research Foundation (DFG) within the Collaborative Research Centre “On-The-Fly Computing” (SFB 901).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Babb, J., Frank, M., Agarwal, A.: Solving graph problems with dynamic computation structures. In: Proceedings of SPIE: High-Speed Computing, Digital Signal Processing, and Filtering Using Reconfigurable Logic, vol. 2914, pp. 225–236 (1996)
Biere, A.: Picosat essentials. J. Satisf. Boolean Model. Comput. (JSAT) 4, 75–97 (2008)
Chatterjee, S., Mishchenko, A., Brayton, R., Kuehlmann, A.: On resolution proofs for combinational equivalence. In: 2007 44th ACM/IEEE Design Automation Conference, pp. 600–605, June 2007
Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC 1971, pp. 151–158. ACM, New York (1971)
Heule, M., Biere, A.: Proofs for satisfiability problems, vol. 55, pp. 1–22. College Publications (2015)
Hybrid Memory Cube Consortium: Hybrid memory cube specification 2.0 (2014)
Isenberg, T., Platzner, M., Wehrheim, H., Wiersema, T.: Proof-carrying hardware via inductive invariants. ACM Trans. Des. Autom. Electron. Syst. 22(4), 61:1–61:23 (2017)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_1
Nai, L., Hadidi, R., Sim, J., Kim, H., Kumar, P., Kim, H.: GraphPIM: enabling instruction-level PIM offloading in graph computing frameworks. In: 2017 IEEE International Symposium on High Performance Computer Architecture (HPCA), pp. 457–468, February 2017
Pawlowski, J.T.: Hybrid memory cube (HMC). In: 2011 IEEE Hot Chips 23 Symposium (HCS), pp. 1–24, August 2011
Skliarova, I., de Brito Ferrari, A.: Reconfigurable hardware SAT solvers: a survey of systems. IEEE Trans. Comput. 53(11), 1449–1461 (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Hansmeier, T., Platzner, M., Andrews, D. (2018). An FPGA/HMC-Based Accelerator for Resolution Proof Checking. In: Voros, N., Huebner, M., Keramidas, G., Goehringer, D., Antonopoulos, C., Diniz, P. (eds) Applied Reconfigurable Computing. Architectures, Tools, and Applications. ARC 2018. Lecture Notes in Computer Science(), vol 10824. Springer, Cham. https://doi.org/10.1007/978-3-319-78890-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-78890-6_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-78889-0
Online ISBN: 978-3-319-78890-6
eBook Packages: Computer ScienceComputer Science (R0)