A Synthesis of Reversible Digital Circuits to Solve the Boolean Satisfiability

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26220%2F20%3APU131775" target="_blank" >RIV/00216305:26220/20:PU131775 - isvavai.cz</a>
Result on the web
<a href="https://www.scopus.com/record/display.uri?eid=2-s2.0-85092094569&origin=resultslist&sort=plf-f&src=s&st1=boolean+satisfiability&st2=&sid=e25bcdaf87ef4bc2eced1790a94cd2ed&sot=b&sdt=b&sl=29&s=TITLE%28boolean+satisfiability%29&relpos=0&citeCnt=0&searchTerm=" target="_blank" >https://www.scopus.com/record/display.uri?eid=2-s2.0-85092094569&origin=resultslist&sort=plf-f&src=s&st1=boolean+satisfiability&st2=&sid=e25bcdaf87ef4bc2eced1790a94cd2ed&sot=b&sdt=b&sl=29&s=TITLE%28boolean+satisfiability%29&relpos=0&citeCnt=0&searchTerm=</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-981-15-5546-6_19" target="_blank" >10.1007/978-981-15-5546-6_19</a>

Result language
angličtina
Original language name
A Synthesis of Reversible Digital Circuits to Solve the Boolean Satisfiability
Original language description
The paper presents a methodology of synthesising the reversible digital circuits that solve the Boolean satisfiability (SAT). There is a full range of applications of such circuits; for example, accelerating SAT solvers, generating compacted tests for the sequential circuits designed for testability (with a scan chain), producing a set of results for the relation inverse to combinational functions, generating input vectors of a circuit from output ones, etc. Further, compacted representation of functions, and the straightforward and reverse approaches to obtain responses are discussed. The methodology comprises a few rules to synthesise a combinational function (circuit) into a reversible circuit in a way to implement them into FPGAs. A method of shortening the truth table for implementation in an FPGA is presented and the architecture of reversible circuits is described. The experimental data and features of the physical implementation of the circuits reverse to the ISCAS’85 benchmarks are presented for Xilinx FPGA Spartan 2E – the area overhead and computing complexity of generating the first valid input vector. The experiments show that both the features have asymptotically polynomial complexity.
Czech name
—
Czech description
—

Project
<a href="/en/project/LO1401" target="_blank" >LO1401: Interdisciplinary Research of Wireless Technologies</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2020
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)