Loading...
Please wait, while we are loading the content...
Similar Documents
Electronic Communications of the EASST Volume 70 ( 2014 ) Proceedings of the 14 th International Workshop on Automated Verification of Critical Systems ( AVoCS 2014 ) QBF with Soft Variables
| Content Provider | Semantic Scholar |
|---|---|
| Author | Reimer, Sven Sauer, Matthias Marin, Paolo Becker, Bernd |
| Copyright Year | 2014 |
| Abstract | QBF formulae are usually considered in prenex form, i.e. the quantifier block is completely separated from the propositional part of the QBF. Among others, the semantics of the QBF is defined by the sequence of the variables within the prefix, where existentially quantified variables depend on all universally quantified variables stated to the left. In this paper we extend that classical definition and consider a new quantification type which we call soft variable. The idea is to allow a flexible position and quantifier type for these variables. Hence the type of quantifier of the soft variable can also be altered. Based on this concept, we present an optimization problem seeking an optimal prefix as defined by user-given preferences. We state an algorithm based on MaxQBF, and present several applications – mainly from verification area – which can be naturally translated into the optimization problem for QBF with soft variables. We further implemented a prototype solver for this formalism, and compare our approach to previous work, that differently from ours does not guarantee optimality and completeness. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://journal.ub.tu-berlin.de/eceasst/article/download/973/951 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
