Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem Kapitel lesen Erstes Kapitel lesen

2018 | OriginalPaper | Buchkapitel

Extended Resolution Simulates DRAT

verfasst von : Benjamin Kiesl, Adrián Rebola-Pardo, Marijn J. H. Heule

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

We prove that extended resolution—a well-known proof system introduced by Tseitin—polynomially simulates \({\mathsf {DRAT}}\), the standard proof system in modern SAT solving. Our simulation procedure takes as input a \({\mathsf {DRAT}}\) proof and transforms it into an extended-resolution proof whose size is only polynomial with respect to the original proof. Based on our simulation, we implemented a tool that transforms \({\mathsf {DRAT}}\) proofs into extended-resolution proofs. We ran our tool on several benchmark formulas to estimate the increase in size caused by our simulation in practice. Finally, as a side note, we show how blocked-clause addition—a generalization of the extension rule from extended resolution—can be used to replace the addition of resolution asymmetric tautologies in \({\mathsf {DRAT}}\) without introducing new variables.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel A Resolution-Based Calculus for Preferential Logics
Nächstes Kapitel Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Fußnoten
1
The simulation tool, checkers, formulas, and proofs discussed in this section are available on http://​www.​cs.​utexas.​edu/​~marijn/​drat2er.
 
Literatur
1.
Baaz, M., Leitsch, A.: Methods of Cut-Elimination. Trends in Logic, vol. 3. Springer, Heidelberg (2011)MATH
2.
Biere, A.: Two pigeons per hole problem. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, p. 103 (2013)
3.
Chatalic, P., Simon, L.: Multi-resolution on compressed sets of clauses. In: Proceedings of the 12th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2000), pp. 2–10 (2000)
4.
Cook, S.A.: A short proof of the pigeon hole principle using extended resolution. SIGACT News 8(4), 28–32 (1976)CrossRef
5.
Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979)MathSciNetCrossRef
6.
7.
Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 75–92. Springer, Cham (2018)CrossRef
8.
Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 130–147. Springer, Cham (2017)CrossRef
9.
Järvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010)CrossRef
10.
Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355–370. Springer, Heidelberg (2012)CrossRef
11.
Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 54–60. Springer, Heidelberg (2006)CrossRef
12.
Konev, B., Lisitsa, A.: Computer-aided proof of Erdős discrepancy properties. Artif. Intell. 224(C), 103–118 (2015)CrossRef
13.
14.
Lee, C.T.: A completeness theorem and a computer program for finding theorems derivable from given axioms. Ph.D. thesis (1967)
15.
Philipp, T., Rebola-Pardo, A.: Towards a semantics of unsatisfiability proofs with inprocessing. In: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). EPiC Series in Computing, vol. 46, pp. 65–84. EasyChair (2017)
16.
Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 600–611. Springer, Heidelberg (2006)CrossRef
17.
Tseitin, G.S.: On the complexity of derivation in propositional calculus. Stud. Math. Math. Log. 2, 115–125 (1968)
18.
19.
Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: Proceedings of the 10th International Symposium on Artificial Intelligence and Mathematics (ISAIM 2008) (2008)
20.
Van Gelder, A.: Producing and verifying extremely large propositional refutations. Ann. Math. Artif. Intell. 65(4), 329–372 (2012)MathSciNetCrossRef
21.
Wetzler, N., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014)
Metadaten
Titel
Extended Resolution Simulates DRAT
verfasst von
Benjamin Kiesl
Adrián Rebola-Pardo
Marijn J. H. Heule
Copyright-Jahr
2018
Buch
Automated Reasoning

Print ISBN: 978-3-319-94204-9

Electronic ISBN: 978-3-319-94205-6

Copyright-Jahr: 2018

DOI
https://doi.org/10.1007/978-3-319-94205-6_34