Date: 08-Dec-2008 Title: SAT Benchmarks stemming from an analysis of parity games by Oliver Friedmann Hits: 804 Contributed by: Daniel Le Berre Keywords: Benchmark, SAT application, SAT-Based         From the benchmarks web page: These benchmarks originate from my research investigating the structure of parity games that are found to be tough to solve for the standard strategy improvement algorithm. All following downloads are distributed under the BSD license. The generator is written in OCaml. You will therefore need an OCaml compiler to produce an executable. Additionally you can download precompiled binary executables for 32-bit Windows and Linux. Finally there is a pregenerated package of benchmarks that can be obtained as well.

Date: 14-Jul-2008 Title: A set of benchmarks steming from an in-depth analysis of parity games Hits: 1009 Contributed by: Anonymous Keywords:         This is a collection of very tough benchmarks steming from an in-depth analysis of the structure of parity games. If you need larger instances to test your sat solver - please let me know!

Date: 21-May-2008 Title: SAT benchmark encoding the key recovery attack of the stream cipher Bivium Hits: 1101 Contributed by: Daniel Le Berre Keywords: Benchmark, SAT application, null, null         SAT solvers can be used to attack cryptographic stream ciphers. In this benchmark, the solution of a cnf file recovers the internal state of the stream cipher "Brivium" - a reduced version of the eSTREAM cipher "Trivium". The benchmark contains instances of varying complexity (this is achieved by guessing more or less variable assignments). The benchmark provides 300 instances of each difficulty and each with the SAT and UNSAT case.

Date: 01-Jul-2004 Title: More illustration of IBM CNF benchmark: zChaff vs Berkmin561 Hits: 2735 Contributed by:       Date: 23-Mar-2004 Title: An illustration of IBM CNF benchmark: zChaff vs Berkmin561 Hits: 2528 Contributed by:       Date: 03-Dec-2003 Title: More forced satisfiable instances of Model RB available now Hits: 2830 Contributed by: Ke Xu Keywords: Benchmark, Randomised Problem Generation, Satisfiable Problems Generation, CSP, phase transition, resolution complexity         Recently, we have added more forced satisfiable instances of Model RB. Now there are 8 groups of SAT benchmarks, ranging from 450 variables (relatively easy to solve) to 1534 variables (appearing very hard to solve based on the experimental results of ours and some other researchers).             Date: 05-Nov-2003 Title: 2 CNF benchmark suites Hits: 2773 Contributed by: Miroslav Velev Keywords: Verification, EDA, Benchmark, SAT application, SAT tools         Suites B27 (4 unsatisfiable formulas) and B28 (10 satisfiable formulas)             Date: 23-Oct-2003 Title: SAT benchmarks encoded from forced satisfiable instances of Model RB Hits: 2617 Contributed by: Ke Xu Keywords: Benchmark, Randomised Problem Generation, Satisfiable Problems Generation, CSP, phase transition, resolution complexity         All benchmarks were generated using the method proposed in the paper entitled "Many Hard Examples in Exact Phase Transitions with Application to Generating Hard Satisfiable Instances". There are totally 15 satisfiable CNF instances, all of which are expressed in the DIMACS format.             Date: 02-Oct-2003 Title: 5 new benchmark suites of CNF formulas (suites B22-B26) Hits: 2535 Contributed by: Miroslav Velev Keywords: Verification, EDA, Benchmark, SAT application         a total of 18 unsattisfiable and 30 satisfiable CNF formulas             Date: 09-Sep-2003 Title: 6 new Suites with challenging formulas from formal verification of processors Hits: 2451 Contributed by: Miroslav Velev Keywords: Verification, EDA, Benchmark, SAT application, SAT tools         A total of 43 unsatisfiable and 20 satisfiable CNF formulas (Suites B16-B21).             Date: 24-Aug-2003 Title: Formulas from formal verification of microprocessors (Suite B15) Hits: 2344 Contributed by: Miroslav Velev Keywords: Verification, EDA, Benchmark, SAT application, SAT tools         32 CNF formulas from formal verification of DLX processors with multicycle functional units, exceptions, branch prediction, and instruction queues             Date: 18-Aug-2003 Title: CNF formulas from formal verification of out-of-order processors with register renaming and a reorder buffer (Suite B14). Hits: 2302 Contributed by: Miroslav Velev Keywords: Verification, EDA, Benchmark, SAT application, SAT tools         10 CNF instances. Formula engine_6_nd.cnf is the most chalenging one.             Date: 10-Aug-2003 Title: New benchmarks from formal verificationof microprocessors Hits: 2118 Contributed by:       Date: 24-Jun-2003 Title: QBF'03 evaluation benchmarks Hits: 2206 Contributed by: Armando Tacchella Keywords: Repository, QBF, instance database         All the benchmarks used for the 2003 QBF evaluation have been added to QBFLIB, categorized according to their hardness with respect to the solvers that participated in the evaluation.             Date: 13-Jun-2003 Title: SAT 2003 benchmarks available on SATLIB! Hits: 2494 Contributed by: Daniel Le Berre Keywords: Benchmark         The benchmarks used during the SAT2003 competition are now available on SATLIB. Note that the IBM ZARPAS are not included, you need to collect them from IBM web site (link available in the benchmark category). [update] if the link to the benchmarks does not work, try this one             Date: 17-Feb-2003 Title: The IBM Formal Verification Benchmark Hits: 2293 Contributed by:       Date: 27-Nov-2002 Title: Two SAT benchmark suites from formal verification of liveness for pipelined and superscalar microprocessors Hits: 2297 Contributed by: Miroslav Velev Keywords: Verification         These SAT benchmarks are significantly more challenging compared to their counterparts from formal verification of safety, generated before.             Date: 28-Aug-2002 Title: SAT encoding of Board-Level Multi-Terminal Net Assignment. Xiaoyu Song, William N. N. Hung, Alan Mishchenko, Malzorgata Chrzanowska-Jeske, Alan Coppola and Andrew Kennings. Hits: 2331 Contributed by: Daniel Le Berre Keywords: Benchmark, SAT application         From the authors web site: The benchmarks presented here are the results of a satisfiability-based formulation for the board-level multi-terminal net routing problem in the digital design of Clos-Folded FPGA based logic emulation systems. We transform the FPGA board-level routing task into conjunctive normal form (CNF) such that the formula is satisfiable if and only if the problem is routable.             Date: 04-May-2002 Title: Experimental design SAT page under OpenExperiments! Hits: 2526 Contributed by: Daniel Le Berre Keywords: Repository, Benchmark, instance database         From the web site: Experimental evaluation of SAT algorithms has been practiced and debated with considerable intensity over the last decade. Typical comparisons involve a collection of unrelated benchmark instances. Algorithms are evaluated on the basis of their total or average execution time for the collection. Experiments archived on these pages represent a significant departure from this approach. By introducing equivalence classes of closely related instances for each reference formula (in cnf), we can experimentally deduce the 95% confidence interval of the mean time-to-solve and other significantly correlated metrics such as the total number of implications. Instances derived from the reference formula that are perceived `hard' by the algorithm under test may exhibit max/min ratios of a metric that can range anywhere from 2 to 1000 and beyond. In such cases, comparisons based on single formulas have no statistical merit. The site contains various equivalence classes ready to download.             Date: 04-May-2002 Title: SAT2002 competition first stage results available Hits: 2771 Contributed by: Daniel Le Berre Keywords: Deduction Rules, BMC, DPLL, Intelligent Backtracking, Local Search, Random 3SAT, EDA, Benchmark, SAT application, Equivalency Reasoning, Randomised Algorithms, Learning         The SAT2002 competition first stage results are finally available. For more infos about the competition: SAT competition home page             Date: 24-Mar-2002 Title: NPE-1.0: 6 CNF formulas generated in microprocessor formal verification without exploiting the property of Positive Equality. Hits: 2291 Contributed by: Miroslav Velev Keywords: Verification, EDA, Benchmark, SAT application         The two biggest benchmarks are 327 MB when uncompressed with 'gunzip', and have close to 900,000 CNF variables and 15 million clauses. If you use this benchmark suite, please reference the following paper: M.N. Velev, and R.E. Bryant, "Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors," 38th Design Automation Conference (DAC '01), June 2001, pp. 226-231.             Date: 15-Mar-2002 Title: FVP-SAT.3.0: 20 satisfiable CNF formulas from formal verification of buggy variants of an out-of-order superscalar processor that has 64 Reorder Buffer entries and can fetch/retire up to 4 instructions per cycle. Hits: 2268 Contributed by: Miroslav Velev Keywords: Verification, EDA, Benchmark, SAT application         If you use this benchmark suite, please reference the following paper: M.N. Velev, "Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-Of-Order Microprocessors with a Reorder Buffer," Design, Automation and Test in Europe (DATE '02), March 2002, pp. 28-35.             Date: 13-Mar-2002 Title: FVP-UNSAT.3.0: 6 unsatisfiable CNF formulas for correctness of out-of-order superscalar processors that have 64 Reorder Buffer entries, and do not implement register renaming. Hits: 2219 Contributed by: Miroslav Velev Keywords: Verification, EDA, Benchmark, SAT application         If you use this benchmark suite, please reference the following paper: M.N. Velev, "Using Rewriting Rules and Positive Equality to Formally Verify Wide-Issue Out-Of-Order Microprocessors with a Reorder Buffer," Design, Automation and Test in Europe (DATE '02), March 2002, pp. 28-35.             Date: 18-Jun-2001 Title: Clustered problem generator by Andrew Slater Hits: 2246 Contributed by:       Date: 17-May-2001 Title: SAT-encoded bounded model checking intances contributed by Ofer Shtrichman Hits: 2601 Contributed by: Laurent Simon Keywords: BMC, Benchmark, SAT application, Verification         From Satlib description: The 13 SAT instances given in the benchmark set are all taken from real industrial hardware designs, a contribution of the verification technologies department in the IBM research Laboratory in Haifa (home of RuleBase, the IBM Corporate Model-Checker), and Galileo (a leader in communication hardware design and a heavy user of model checking). In all cases the property is in the form of an invariant. For more infos: SATLIB Description             Date: 13-Oct-2000 Title: SSS-SAT.1.0 benchmark suite Hits: 2324 Contributed by:       Date: 11-Oct-2000 Title: VLIW-SAT.1.0 benchmark suite Hits: 2245 Contributed by:       Date: 14-Aug-2000 Title: Benchmark: formal verification of superscalar and VLIW microprocessors Hits: 2218 Contributed by:   © 2000-2001 Business & Technology Research Laboratory. © 2001-2005 Centre de Recherche en Informatique de Lens. Hosted by Innovation and Technology Research Lab. Please send any comment to daniel@satlive.org.