Hardware/Software Implementation of FPGA-Targeted Matrix-Oriented SAT Solvers

The paper describes two methods for the design of matrix-oriented SAT solvers based on data compression. The first one provides matrix compression in a host computer and decompression in an FPGA. It is shown that although some improvements have been achieved in this case, there exists a better solution. The second method makes possible to execute operations required for solving the SAT problem over compressed matrices.

• Type: Conference
• Year: 2004
• Where: FPL
• Authors: Valery Sklyarov, Iouliia Skliarova, Bruno Figueiredo Pimentel, Joel Arrais
• Keywords: Data Compression, FPL 2004, Matrix Compression, Matrix-oriented Sat Solvers