Skip to main content

2018 | OriginalPaper | Buchkapitel

\({\textsf {QRAT}}^{+}\): Generalizing QRAT by a More Powerful QBF Redundancy Property

verfasst von : Florian Lonsing, Uwe Egly

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

The \(\mathsf {QRAT} \) (quantified resolution asymmetric tautology) proof system simulates virtually all inference rules applied in state of the art quantified Boolean formula (QBF) reasoning tools. It consists of rules to rewrite a QBF by adding and deleting clauses and universal literals that have a certain redundancy property. To check for this redundancy property in \(\mathsf {QRAT} \), propositional unit propagation (UP) is applied to the quantifier free, i.e., propositional part of the QBF. We generalize the redundancy property in the \(\mathsf {QRAT} \) system by QBF specific UP (QUP). QUP extends UP by the universal reduction operation to eliminate universal literals from clauses. We apply QUP to an abstraction of the QBF where certain universal quantifiers are converted into existential ones. This way, we obtain a generalization of \(\mathsf {QRAT} \) we call \(\mathsf {QRAT}^{+} \). The redundancy property in \(\mathsf {QRAT}^{+} \) based on QUP is more powerful than the one in \(\mathsf {QRAT} \) based on UP. We report on proof theoretical improvements and experimental results to illustrate the benefits of \(\mathsf {QRAT}^{+} \) for QBF preprocessing.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
In general, clauses C are always (implicitly) interpreted under a quantifier prefix \(\varPi \).
 
3
We excluded the top-performing solver AIGSolve due to observed assertion failures.
 
Literatur
2.
Zurück zum Zitat Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: STACS. LIPIcs, vol. 30, pp. 76–89. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015) Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: STACS. LIPIcs, vol. 30, pp. 76–89. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)
6.
Zurück zum Zitat Heule, M.J.H., Kiesl, B.: The potential of interference-based proof systems. In: ARCADE. EPiC Series in Computing, vol. 51, pp. 51–54. EasyChair (2017) Heule, M.J.H., Kiesl, B.: The potential of interference-based proof systems. In: ARCADE. EPiC Series in Computing, vol. 51, pp. 51–54. EasyChair (2017)
7.
Zurück zum Zitat Heule, M.J.H., Kullmann, O.: The science of brute force. Commun. ACM 60(8), 70–79 (2017)CrossRef Heule, M.J.H., Kullmann, O.: The science of brute force. Commun. ACM 60(8), 70–79 (2017)CrossRef
10.
Zurück zum Zitat Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reason. 58(1), 97–125 (2017)MathSciNetCrossRef Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reason. 58(1), 97–125 (2017)MathSciNetCrossRef
11.
Zurück zum Zitat Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–25 (2016)MathSciNetCrossRef Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–25 (2016)MathSciNetCrossRef
15.
Zurück zum Zitat Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995)MathSciNetCrossRef Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995)MathSciNetCrossRef
18.
20.
Zurück zum Zitat Rabe, M.N., Tentrup, L.: CAQE: A certifying QBF solver. In: FMCAD, pp. 136–143. IEEE (2015) Rabe, M.N., Tentrup, L.: CAQE: A certifying QBF solver. In: FMCAD, pp. 136–143. IEEE (2015)
25.
Zurück zum Zitat Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: ICCAD, pp. 442–449. ACM/IEEE Computer Society (2002) Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: ICCAD, pp. 442–449. ACM/IEEE Computer Society (2002)
Metadaten
Titel
: Generalizing QRAT by a More Powerful QBF Redundancy Property
verfasst von
Florian Lonsing
Uwe Egly
Copyright-Jahr
2018
DOI
https://doi.org/10.1007/978-3-319-94205-6_12