Abstract
We present the framework [q]bfGen which allows the declarative specification of random models for generating SAT and QSAT formulas not necessarily in (prenex) conjunctive normal form. To this end, [q]bfGen realizes a generic formula generator which creates formula instances by interpreting the random model specification expressed in XML. Consequently, the implementation of specific random formula generators becomes obsolete, because our framework subsumes their functionality.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 6th International Conference on Tests and Proofs (TAP 2012) |
| Place of Publication | Heidelberg |
| Publisher | Springer |
| Pages | 163 - 168 |
| Number of pages | 6 |
| ISBN (Print) | 978-3-642-30472-9 |
| Publication status | Published - Jun 2012 |
Fields of science
- 102011 Formal languages
- 102 Computer Sciences
- 101 Mathematics
JKU Focus areas
- Computation in Informatics and Mathematics