SAT Benchmarks

If you would like additional instances for the benchmarks below, drop me an email at faloul@eecs.umich.edu.

FPGA Switch-Box

·        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.

Difficult Integer Factorization Problems

·        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.