---
_id: '12967'
abstract:
- lang: eng
  text: 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.
author:
- first_name: Tim
  full_name: Hansmeier, Tim
  id: '49992'
  last_name: Hansmeier
  orcid: 0000-0003-1377-3339
- first_name: Marco
  full_name: Platzner, Marco
  id: '398'
  last_name: Platzner
- first_name: Md Jubaer Hossain
  full_name: Pantho, Md Jubaer Hossain
  last_name: Pantho
- first_name: David
  full_name: Andrews, David
  last_name: Andrews
citation:
  ama: Hansmeier T, Platzner M, Pantho MJH, Andrews D. An Accelerator for Resolution
    Proof Checking based on FPGA and Hybrid Memory Cube Technology. <i>Journal of
    Signal Processing Systems</i>. 2019;91(11):1259-1272. doi:<a href="https://doi.org/10.1007/s11265-018-1435-y">10.1007/s11265-018-1435-y</a>
  apa: Hansmeier, T., Platzner, M., Pantho, M. J. H., &#38; Andrews, D. (2019). An
    Accelerator for Resolution Proof Checking based on FPGA and Hybrid Memory Cube
    Technology. <i>Journal of Signal Processing Systems</i>, <i>91</i>(11), 1259–1272.
    <a href="https://doi.org/10.1007/s11265-018-1435-y">https://doi.org/10.1007/s11265-018-1435-y</a>
  bibtex: '@article{Hansmeier_Platzner_Pantho_Andrews_2019, title={An Accelerator
    for Resolution Proof Checking based on FPGA and Hybrid Memory Cube Technology},
    volume={91}, DOI={<a href="https://doi.org/10.1007/s11265-018-1435-y">10.1007/s11265-018-1435-y</a>},
    number={11}, journal={Journal of Signal Processing Systems}, author={Hansmeier,
    Tim and Platzner, Marco and Pantho, Md Jubaer Hossain and Andrews, David}, year={2019},
    pages={1259–1272} }'
  chicago: 'Hansmeier, Tim, Marco Platzner, Md Jubaer Hossain Pantho, and David Andrews.
    “An Accelerator for Resolution Proof Checking Based on FPGA and Hybrid Memory
    Cube Technology.” <i>Journal of Signal Processing Systems</i> 91, no. 11 (2019):
    1259–72. <a href="https://doi.org/10.1007/s11265-018-1435-y">https://doi.org/10.1007/s11265-018-1435-y</a>.'
  ieee: T. Hansmeier, M. Platzner, M. J. H. Pantho, and D. Andrews, “An Accelerator
    for Resolution Proof Checking based on FPGA and Hybrid Memory Cube Technology,”
    <i>Journal of Signal Processing Systems</i>, vol. 91, no. 11, pp. 1259–1272, 2019.
  mla: Hansmeier, Tim, et al. “An Accelerator for Resolution Proof Checking Based
    on FPGA and Hybrid Memory Cube Technology.” <i>Journal of Signal Processing Systems</i>,
    vol. 91, no. 11, 2019, pp. 1259–72, doi:<a href="https://doi.org/10.1007/s11265-018-1435-y">10.1007/s11265-018-1435-y</a>.
  short: T. Hansmeier, M. Platzner, M.J.H. Pantho, D. Andrews, Journal of Signal Processing
    Systems 91 (2019) 1259–1272.
date_created: 2019-08-26T13:41:57Z
date_updated: 2022-01-06T06:51:27Z
department:
- _id: '78'
doi: 10.1007/s11265-018-1435-y
intvolume: '        91'
issue: '11'
language:
- iso: eng
page: 1259 - 1272
publication: Journal of Signal Processing Systems
publication_identifier:
  issn:
  - 1939-8018
  - 1939-8115
publication_status: published
status: public
title: An Accelerator for Resolution Proof Checking based on FPGA and Hybrid Memory
  Cube Technology
type: journal_article
user_id: '49992'
volume: 91
year: '2019'
...