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
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Metabolic Pathways as Temporal Logic Programs Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

DRAT Proofs for XOR Reasoning

verfasst von : Tobias Philipp, Adrián Rebola-Pardo

Erschienen in: Logics in Artificial Intelligence

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Unsatisfiability proofs in the DRAT format became the de facto standard to increase the reliability of contemporary SAT solvers. We consider the problem of generating proofs for the XOR reasoning component in SAT solvers and propose two methods: direct translation transforms every XOR constraint addition inference into a DRAT proof, whereas T-translation avoids the exponential blow-up in direct translations by using fresh variables. T-translation produces DRAT proofs from Gaussian elimination records that are polynomial in the size of the input CNF formula. Experiments show that a combination of both approaches with a simple prediction method outperforms the BDD-based method.

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 Kinetic Consistency and Relevance in Belief Revision
Nächstes Kapitel Understanding the Abstract Dialectical Framework
Fußnoten
Literatur
1.
Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult SAT instances in the presence of symmetry. In: DAC 2002, pp. 731–736. ACM (2002)
2.
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI 2009, pp. 399–404. Morgan Kaufmann Publishers Inc., Pasadena (2009)
3.
Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22(1), 319–351 (2004)MathSciNetMATH
4.
Belov, A., Diepold, D., Heule, M.J., Järvisalo, M. (eds.): Proceedings of SAT Competition 2014, Department of Computer Science Series of Publications B, vol. B-2014-2. University of Helsinki, Helsinki (2014)
5.
Biere, A.: Yet another local search solver and lingeling and friends entering the SAT competition 2014. In: Belov et al. [4], pp. 39–40
6.
Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: DAC, pp. 40–45 (1990)
7.
Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: Workshop SMT 2010, pp. 1–5. ACM (2009)
8.
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)CrossRefMATH
9.
Courtois, N.T., Bard, G.V.: Algebraic cryptanalysis of the data encryption standard. In: Galbraith, S.D. (ed.) Cryptography and Coding 2007. LNCS, vol. 4887, pp. 152–169. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-77272-9_​10 CrossRef
10.
11.
Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005). doi:10.​1007/​11499107_​5 CrossRef
12.
13.
Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. J. Satisf. Boolean Model. Comput. 2, 1–26 (2006)MATH
14.
Gwynne, M., Kullmann, O.: On SAT representations of XOR constraints. In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 409–420. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-04921-2_​33 CrossRef
15.
Heule, M.J.H., Hunt, W.A., Wetzler, N.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 591–606. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-21401-6_​40 CrossRef
16.
Heule, M.J.H., Biere, A.: Proofs for satisfiability problems. In: All About Proofs, Proofs for All (2015)
17.
Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean Triples problem via cube-and-conquer. CoRR abs/1605.00723 (2016)
18.
Heule, M.: March. Towards a lookahead SAT solver for general purposes. Master’s thesis (2004)
19.
20.
Laitinen, T.: Extending SAT solver with parity reasoning. Ph.D. thesis (2014)
21.
22.
23.
Manthey, N.: Riss 4.27. In: Belov et al. [4], pp. 65–67
24.
Manthey, N., Lindauer, M.: SpyBug: automated bug detection in the configuration space of SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 554–561. Springer, Heidelberg (2016). doi:10.​1007/​978-3-319-40970-2_​36 CrossRef
25.
Rebola-Pardo, A.: Unsatisfiability proofs in SAT solving with parity reasoning. Master thesis, Technische Universität Dresden, Informatik Fakultät (2015)
26.
Roussel, O., Manquinho, V.M.: Pseudo-Boolean and cardinality constraints. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 695–733. IOS Press (2009)
27.
Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: ICCAD 1996, pp. 220–227. IEEE Computer Society, Washington (1996)
28.
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). doi:10.​1007/​11753728_​60 CrossRef
29.
Soos, M.: Enhanced Gaussian elimination in DPLL-based SAT solvers. In: POS 2010 (2010)
30.
Soos, M.: Cryptominisat v4. In: Belov et al. [4], pp. 23–34
31.
32.
Wetzler, N., Heule, M.J.H., Hunt, 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, Heidelberg (2014). doi:10.​1007/​978-3-319-09284-3_​31
Metadaten
Titel
DRAT Proofs for XOR Reasoning
verfasst von
Tobias Philipp
Adrián Rebola-Pardo
Copyright-Jahr
2016
Buch
Logics in Artificial Intelligence

Print ISBN: 978-3-319-48757-1

Electronic ISBN: 978-3-319-48758-8

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-48758-8_27

Premium Partner

    Bildnachweise