Fadi Aloul SAT Benchmarks

SAT Benchmarks

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


The collection of instances used in the paper: Solving Difficult SAT Instances in the Presence of Symmetry, (DAC02), can be downloaded here. The collection includes instances from

  • FPGA Switch-Box (UNS & SAT)
  • Global Routing (SAT)
  • Pigeon-Hole (UNS)
  • Randomized Urquhart (UNS)

 

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. The variables and clauses have been randomly re-ordered.

 

References:

  1. F. Aloul, A. Ramani, I. Markov, and K. Sakallah, Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry, IEEE Transactions on Computer Aided Design, 22(9), pp. 1117-1137, Sept. 2003.
  2. 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.
  3. F. Aloul, A. Ramani, I. Markov, and K. Sakallah, Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry, Technical Report CSE-TR-463-02, University of Michigan, September 2002.
  4. The benchmarks were submitted to the SAT02 competition.

- FPGA_SB_SAT listed as Bart on the SAT'02 website.
- FPGA_SB_UNS listed as Homer on the SAT'02 website.

 

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. The variables and clauses have been randomly re-ordered.

 

References:

  1. The benchmarks were submitted to the SAT02 competition.
    - Benchmarks are labeled as Lisa on the SAT'02 website.

 

To decompress and unpack:

     %  gunzip file.tar.gz

     %  tar -xvf file.tar

 


Related Links

1.  Ke Xu's Forced Satisfiable SAT Benchmarks

Contact: Fadi A. Aloul (faloul@aus.edu)

Last edited on January 20, 2005.