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
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
History and Prospects for First-Order Automated Deduction Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Expressing Symmetry Breaking in DRAT Proofs

verfasst von : Marijn J. H. Heule, Warren A. Hunt Jr., Nathan Wetzler

Erschienen in: Automated Deduction - CADE-25

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

An effective SAT preprocessing technique is the addition of symmetry-breaking predicates: auxiliary clauses that guide a SAT solver away from needless exploration of isomorphic sub-problems. Symmetry-breaking predicates have been in use for over a decade. However, it was not known how to express the addition of these predicates in proofs of unsatisfiability. Hence, results obtained by symmetry breaking cannot be validated by existing proof checkers. We present a method to express the addition of symmetry-breaking predicates in DRAT, a clausal proof format supported by top-tier solvers. We applied this method to generate SAT problems that have not been previously solved without symmetry-breaking predicates. We validated these proofs with an ACL2-based, mechanically-verified DRAT proof checker and the proof-checking tool of SAT Competition 2014.

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 Theorem Proving with Bounded Rigid E-Unification
Nächstes Kapitel MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers
Fußnoten
Literatur
1.
Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: KR 1996, pp. 148–159. Morgan Kaufmann (1996)
2.
Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: Solving difficult sat instances in the presence of symmetry. In: Proceedings of the 39th Design Automation Conference, pp. 731–736 (2002)
3.
Gent, I.P., Smith, B.M.: Symmetry breaking in constraint programming. In: Horn, W. (ed.) ECAI 2000, pp. 599–603. IOS Press (2000)
4.
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, Heidelberg (2014)
5.
Konev, B., Lisitsa, A.: A SAT attack on the Erdős discrepancy conjecture. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 219–226. Springer, Heidelberg (2014)
6.
7.
Codish, M., Cruz-Filipe, L., Frank, M., Schneider-Kamp, P.: Twenty-five comparators is optimal when sorting nine inputs (and twenty-nine for ten). In: ICTAI 2014, pp. 186–193. IEEE Computer Society (2014)
8.
Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for boolean satisfiability. IEEE Trans. Comput. 55(5), 549–558 (2006)CrossRefMATH
9.
Schaafsma, B., Heule, M.J.H., van Maaren, H.: Dynamic symmetry breaking by simulating zykov contraction. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 223–236. Springer, Heidelberg (2009) CrossRef
10.
Radziszowski, S.P.: Small Ramsey numbers. Electron. J. Comb. #DS1 (2014)
11.
Wetzler, N.D.: Efficient, mechanically-verified validation of satisfiability solvers. Ph.D. dissertation, The University of Texas at Austin, May 2015
12.
13.
Zhang, L., Malik, S.: Validating sat solvers using an independent resolution-based checker: practical implementations and other applications. In: DATE, pp. 10880–10885 (2003)
14.
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004) CrossRef
15.
Biere, A.: Picosat essentials. JSAT 4(2–4), 75–97 (2008)MATH
16.
Van Gelder, A.: Verifying rup proofs of propositional unsatisfiability. In: ISAIM (2008)
17.
Heule, M.J.H., Hunt Jr, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 345–359. Springer, Heidelberg (2013) CrossRef
18.
Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, pp. 181–188. IEEE (2013)
19.
Heule, M.J.H., Hunt Jr, W.A., Wetzler, N.: Bridging the gap between easy generation and efficient verification of unsatisfiability proofs. Softw. Test. Verif. Reliab. (STVR) 24(8), 593–607 (2014)CrossRef
20.
Järvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355–370. Springer, Heidelberg (2012) CrossRef
21.
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
22.
23.
Batcher, K.E.: Sorting networks and their applications. In: Proceedings of Spring Joint Computer Conference, AFIPS 1968, pp. 307–314. ACM (1968)
24.
Darga, P.T., Liffiton, M.H., Sakallah, K.A., Markov, I.L.: Exploiting structure in symmetry detection for cnf. In: DAC 2004, pp. 530–534. ACM (2004)
25.
Wetzler, N., Heule, M.J.H., Hunt Jr, W.A.: Mechanical verification of SAT refutations with extended resolution. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 229–244. Springer, Heidelberg (2013) CrossRef
26.
Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44–57. Springer, Heidelberg (2010) CrossRef
Metadaten
Titel
Expressing Symmetry Breaking in DRAT Proofs
verfasst von
Marijn J. H. Heule
Warren A. Hunt Jr.
Nathan Wetzler
Copyright-Jahr
2015
Buch
Automated Deduction - CADE-25

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

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

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-21401-6_40

Premium Partner

    Bildnachweise