Name
Abstract | ||
|---|---|---|
In this paper we present sQueezeBF, an effective preprocessor for QBFs that combines various techniques for eliminating variables and/or redundant clauses. In particular sQueezeBF combines (i) variable elimination via Q-resolution, (ii) variable elimination via equivalence substitution and (iii) equivalence breaking via equivalence rewriting. The experimental analysis shows that sQueezeBF can produce significant reductions in the number of clauses and/or variables - up to the point that some instances are solved directly by sQueezeBF - and that it can significantly improve the efficiency of a range of state-of-the-art QBF solvers - up to the point that some instances cannot be solved without sQueezeBF preprocessing. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-14186-7_9 | SAT |
Keywords | Field | DocType |
significant reduction,present squeezebf,equivalence reasoning,squeezebf preprocessing,variable elimination,equivalence substitution,equivalence breaking,effective preprocessor,experimental analysis,particular squeezebf combine,redundant clause | Discrete mathematics,Variable elimination,Preprocessor,Equivalence (measure theory),Rewriting,True quantified Boolean formula,Propositional formula,Mathematics | Conference |
Volume | ISSN | ISBN |
6175 | 0302-9743 | 3-642-14185-4 |
Citations | PageRank | References |
26 | 0.92 | 19 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Enrico Giunchiglia | 1 | 2380 | 164.28 |
| Paolo Marin | 2 | 67 | 6.83 |
| Massimo Narizzano | 3 | 451 | 30.41 |