---
_id: '3373'
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: David
  full_name: Andrews, David
  last_name: Andrews
citation:
  ama: '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>'
  apa: '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>'
  bibtex: '@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} }'
  chicago: '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>.'
  ieee: '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.'
  mla: '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>.'
  short: 'T. Hansmeier, M. Platzner, D. Andrews, in: ARC 2018: Applied Reconfigurable
    Computing. Architectures, Tools, and Applications, Springer International Publishing,
    2018, pp. 153–165.'
conference:
  end_date: 2018-05-04
  location: Santorini, Greece
  name: 'ARC: International Symposium on Applied Reconfigurable Computing'
  start_date: 2018-05-02
date_created: 2018-06-27T09:30:24Z
date_updated: 2022-01-06T06:59:13Z
ddc:
- '000'
department:
- _id: '78'
doi: 10.1007/978-3-319-78890-6_13
file:
- access_level: closed
  content_type: application/pdf
  creator: ups
  date_created: 2018-11-02T13:55:07Z
  date_updated: 2018-11-02T13:55:07Z
  file_id: '5257'
  file_name: AnFPGAHMC-BasedAcceleratorForR.pdf
  file_size: 612367
  relation: main_file
  success: 1
file_date_updated: 2018-11-02T13:55:07Z
has_accepted_license: '1'
intvolume: '     10824'
language:
- iso: eng
page: 153-165
project:
- _id: '12'
  name: SFB 901 - Subproject B4
- _id: '1'
  name: SFB 901
- _id: '3'
  name: SFB 901 - Project Area B
publication: 'ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and
  Applications'
publication_identifier:
  isbn:
  - '9783319788890'
  - '9783319788906'
  issn:
  - 0302-9743
  - 1611-3349
publication_status: published
publisher: Springer International Publishing
series_title: Lecture Notes in Computer Science
status: public
title: An FPGA/HMC-Based Accelerator for Resolution Proof Checking
type: conference
user_id: '3118'
volume: 10824
year: '2018'
...