If you would like additional instances for the benchmarks
below, drop me an email at faloul@eecs.umich.edu.
· Unsatisfiable: (FPGA_SB_UNS.tar.gz)
· Satisfiable: (FPGA_SB_SAT.tar.gz)
The following is a collection of conjunctive-normal-form (CNF) problems for SAT solvers based on FPGA switch-boxes. All problems are expressed in the DIMACS format.
References:
1.
F. Aloul, A. Ramani, I. Markov, and K. Sakallah, “Solving
Difficult SAT Instances in the Presence of Symmetry,” in Proc. of the
Design Automation Conference (DAC), New Orleans, Louisiana, 2002.
2.
The benchmarks were submitted to the SAT’02 competition.
· Array Multiplier: (difp_a.tar.gz)
· Wallace Tree Multiplier: (difp_w.tar.gz)
The following is a collection of conjunctive-normal-form (CNF) problems for SAT solvers. A multiplier circuit is generated that reads two n-bit prime numbers and generates a 2n-bit product number. Two types of multipliers are used: Array and Wallace Tree multipliers. All instances are satisfiable. All problems are expressed in the DIMACS format.
References:
1.
The benchmarks were submitted to the SAT’02 competition.
To decompress and unpack:
% gunzip file.tar.gz
% tar –xvf file.tar
Contact: Fadi A. Aloul (faloul@eecs.umich.edu)
Last edited on Monday, May 09, 2002.