 |
See all Benchmarks
30 elements available |  | |  | | | | | Date: | 05-Sep-2012 | | Title: | ASPCOMP 2013: 4th OPEN Answer Set Programming Competition: Call for Benchmark Problems (EXTENDED DEADLINE)
| | Hits: | 326 | | Contributed by: | Anonymous | | Keywords: | Deduction Rules, DPLL, Minimal models, #P, Computational logic, QBF, Structure of problems, Benchmark, SAT application, Randomised Problem Generation, SAT tools, CSP, Logic, QBF, programming language, General Interest, call for papers, conference information, Non-monotonic reasoning, Satisfiability Modulo Theory, Constraint Programming, SAT/CP, Answer Set Programming, null, null, null, null, null |
| | | |  |  | |
| |
........................................................................
4th OPEN Answer Set Programming Competition 2013
Call for Benchmark Problems
University of Calabria - Vienna University of Technology
Fall/Winter 2012/2013
http://aspcomp2013.mat.unical.it/
........................................................................
The 4th Open Answer Set Programming Competition is open to ASP systems
and *any other system* based on a declarative specification paradigm.
The event is currently finalizing its Call for Benchmarks stage.
== Call for Benchmark Problems ==
Participants will compete on a selected collection of declarative
specifications of benchmark problems, taken from a variety of domains as
well as real world applications, and instances thereof.
These include, but are not limited to:
- Deductive database tasks on large data-sets
- Sequential and Temporal Planning
- Classic and Applicative graph problems
- Puzzles and Combinatorics
- Scheduling, Timetabling, and other resource allocation problems
- Combinatorial Optimization Problems
- Ontology reasoning
- Automated Theorem Proving and Model Checking
- Reasoning tasks over large propositional instances
- Constraint Programming problems
- Other AI problems
We encourage to provide help by proposing and/or devising new challenging
benchmark problems.
The submission of problems arising from applications of practical impact
are strongly encouraged; problems used in the former ASP Competitions,
or variants thereof, can be re-submitted.
Benchmark authors are expected to produce a problem specification and an
instance set (or a generator thereof). The detailed benchmark problems
submission procedure is available at:
http://www.mat.unical.it/aspcomp2013/BenchmarkSubmission.
=== About the ASP Competition Series ===
Answer Set Programming is a well-established paradigm of declarative
programming with close relationship to other declarative modeling
paradigms and languages, such as SAT Modulo Theories, Constraint
Handling Rules, FO(.), PDDL, CASC, and many others.
Since the first informal editions (Dagstuhl 2002 and 2005), ASP systems
compare themselves in the nowadays customary ASP Competition: the 4th
ASP Competition will be run jointly at the University of Calabria
(Italy) and the Vienna University of Technology (Austria), in the first
half of 2013. The event is the sequel to the ASP Competition series,
held at the University of Potsdam (Germany) in 2006-2007, at the
University of Leuven (Belgium) in 2009, and at University of Calabria
(Italy) in 2011. The current competition takes place in cooperation with
the 13th International Conference on Logic Programming and Nonmonotonic
Reasoning (LPNMR 2013), where the results will be announced.
The ASP competition is held as an open tournament. The "Model & Solve"
competition track fosters the spirit of integration among communities,
and is thus open to all types of solvers: ASP systems, SAT solvers, SMT
solvers, CP systems, FOL theorem provers, Description Logics reasoners,
planning reasoners, or any other. The "System" competition track is
instead set up on a fixed language based on the answer set semantics.
== Important Dates ==
* Problem selection stage
- Problem submission deadline: Sep 20th, 2012 (*EXTENDED*)
* Competition stage
- "Model & Solve" submission deadline: Mar 1st, 2013
- "System" submission deadline: Mar 1st, 2013
* Sep 15-19th, 2013
- Announcement of results and awards at LPNMR 2013 - Corunna, Spain
== Further Information ==
For further information please visit the competition web site:
http://aspcomp2013.mat.unical.it/
or contact us by email: aspcomp2013@kr.tuwien.ac.at.
|
| |  | |  |
| | |
| | | These are benchmarks used in [1,2] for analyzing algorithms for high-level minimal unsatisfiable core (MUC) extraction. High-level MUC extraction is an extraction of MUCs in terms of “interesting” propositional constraints supplied by the user application (e.g., the user may want to find MUCs in terms of latches or assumptions only). High-level MUC extraction is very much relevant to real-world applications of MUC extraction [1,2].
The benchmarks were generated by Intel’s abstraction refinement flow, where each high-level constraint represents a latch. Please reference [1] in publications that use these benchmarks.
[1] Alexander Nadel, "Boosting Minimal Unsatisfiable Core Extraction". In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010, Lugano, October 20-23), 2010.
[2] Alexander Nadel, "Boosting Minimal Unsatisfiable Core Extraction: Paper Addendum". http://www.cs.tau.ac.il/research/alexander.nadel/Addendum_to_Boosting_Minimal_Unsatisfiable_Core_Extraction_final.pdf. |
| | | | |
| | |
| | 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.
|
| | | | |
| | |
| | | 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! |
| | | | |
| | |
| | | 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: | 3255 | | Contributed by: | | | | | | | | | Date: | 23-Mar-2004 | | Title: | An illustration of IBM CNF benchmark: zChaff vs Berkmin561
| | Hits: | 3013 | | Contributed by: | | | | 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). |
| | | | |
| | |
| | | Suites B27 (4 unsatisfiable formulas) and B28 (10 satisfiable formulas) |
| | | | |
| | |
| | | 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. |
| | | | |
| | |
| | | a total of 18 unsattisfiable and 30 satisfiable CNF formulas |
| | | | |
| | |
| | | A total of 43 unsatisfiable and 20 satisfiable CNF formulas (Suites B16-B21). |
| | | | |
| | |
| | | 32 CNF formulas from formal verification of DLX processors with multicycle functional units, exceptions, branch prediction, and instruction queues |
| | | | |
| | |
| | | 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: | 2635 | | Contributed by: | | | | 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: | 17-Feb-2003 | | Title: | The IBM Formal Verification Benchmark
| | Hits: | 2805 | | Contributed by: | | | | These SAT benchmarks are significantly more challenging compared to their counterparts from formal verification of safety, generated before. |
| | | | |
| | |
| | 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: | SAT2002 competition first stage results available
| | Hits: | 3293 | | 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 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. |
| | | | |
| | |
| | | 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. |
| | | | |
| | |
| | | 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. |
| | | | |
| | |
|
|
|
|
|
|
|
|
|
|
|
|
| |
