CINXE.COM

<!DOCTYPE html> <html class="client-nojs" lang="de" dir="ltr"> <head> <meta charset="UTF-8"> <title>Erfüllbarkeitsproblem der Aussagenlogik – Wikipedia</title> <script>(function(){var className="client-js";var cookie=document.cookie.match(/(?:^|; )dewikimwclientpreferences=([^;]+)/);if(cookie){cookie[1].split('%2C').forEach(function(pref){className=className.replace(new RegExp('(^| )'+pref.replace(/-clientpref-\w+$|[^\w-]+/g,'')+'-clientpref-\\w+( |$)'),'$1'+pref+'$2');});}document.documentElement.className=className;}());RLCONF={"wgBreakFrames":false,"wgSeparatorTransformTable":[",\t.",".\t,"],"wgDigitTransformTable":["",""],"wgDefaultDateFormat":"dmy","wgMonthNames":["","Januar","Februar","März","April","Mai","Juni","Juli","August","September","Oktober","November","Dezember"],"wgRequestId":"a0ec3a17-4a44-4913-8741-0d6bde2f1dfd","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"Erfüllbarkeitsproblem_der_Aussagenlogik","wgTitle":"Erfüllbarkeitsproblem der Aussagenlogik","wgCurRevisionId":248841235,"wgRevisionId":248841235,"wgArticleId":116802,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view", "wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Komplexitätstheorie","Mathematische Logik","Aussagenlogik"],"wgPageViewLanguage":"de","wgPageContentLanguage":"de","wgPageContentModel":"wikitext","wgRelevantPageName":"Erfüllbarkeitsproblem_der_Aussagenlogik","wgRelevantArticleId":116802,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable":true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject":"wikipedia","wgCiteReferencePreviewsActive":true,"wgFlaggedRevsParams":{"tags":{"accuracy":{"levels":1}}},"wgStableRevisionId":248841235,"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"de","pageLanguageDir":"ltr","pageVariantFallbacks":"de"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":true,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":40000,"wgRelatedArticlesCompat":[],"wgCentralAuthMobileDomain":false, "wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage","wgULSisCompactLinksEnabled":true,"wgVector2022LanguageInHeader":false,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q875276","wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"],"GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled":false,"wgGEStructuredTaskRejectionReasonTextInputEnabled":false,"wgGELevelingUpEnabledForUser":false};RLSTATE={"ext.gadget.citeRef":"ready","ext.gadget.defaultPlainlinks":"ready","ext.gadget.dewikiCommonHide":"ready","ext.gadget.dewikiCommonLayout":"ready","ext.gadget.dewikiCommonStyle":"ready","ext.gadget.NavFrame":"ready","ext.globalCssJs.user.styles":"ready","site.styles":"ready","user.styles":"ready","ext.globalCssJs.user":"ready","user":"ready","user.options":"loading","ext.math.styles":"ready","ext.cite.styles":"ready","mediawiki.page.gallery.styles":"ready", "skins.vector.styles.legacy":"ready","ext.flaggedRevs.basic":"ready","mediawiki.codex.messagebox.styles":"ready","ext.visualEditor.desktopArticleTarget.noscript":"ready","codex-search-styles":"ready","ext.uls.interlanguage":"ready","wikibase.client.init":"ready","ext.wikimediaBadges":"ready"};RLPAGEMODULES=["ext.cite.ux-enhancements","mediawiki.page.media","site","mediawiki.page.ready","mediawiki.toc","skins.vector.legacy.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.flaggedRevs.advanced","ext.gadget.createNewSection","ext.gadget.WikiMiniAtlas","ext.gadget.OpenStreetMap","ext.gadget.CommonsDirekt","ext.gadget.donateLink","ext.urlShortener.toolbar","ext.centralauth.centralautologin","mmv.bootstrap","ext.popups","ext.visualEditor.desktopArticleTarget.init","ext.visualEditor.targetLoader","ext.echo.centralauth","ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.uls.compactlinks","ext.uls.interface","ext.cx.eventlogging.campaigns", "ext.checkUser.clientHints","ext.growthExperiments.SuggestedEditSession","wikibase.sidebar.tracking"];</script> <script>(RLQ=window.RLQ||[]).push(function(){mw.loader.impl(function(){return["user.options@12s5i",function($,jQuery,require,module){mw.user.tokens.set({"patrolToken":"+\\","watchToken":"+\\","csrfToken":"+\\"}); }];});});</script> <link rel="stylesheet" href="/w/load.php?lang=de&modules=codex-search-styles%7Cext.cite.styles%7Cext.flaggedRevs.basic%7Cext.math.styles%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediaBadges%7Cmediawiki.codex.messagebox.styles%7Cmediawiki.page.gallery.styles%7Cskins.vector.styles.legacy%7Cwikibase.client.init&only=styles&skin=vector"> <script async="" src="/w/load.php?lang=de&modules=startup&only=scripts&raw=1&skin=vector"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=de&modules=ext.gadget.NavFrame%2CciteRef%2CdefaultPlainlinks%2CdewikiCommonHide%2CdewikiCommonLayout%2CdewikiCommonStyle&only=styles&skin=vector"> <link rel="stylesheet" href="/w/load.php?lang=de&modules=site.styles&only=styles&skin=vector"> <meta name="generator" content="MediaWiki 1.44.0-wmf.4"> <meta name="referrer" content="origin"> <meta name="referrer" content="origin-when-cross-origin"> <meta name="robots" content="max-image-preview:standard"> <meta name="format-detection" content="telephone=no"> <meta name="viewport" content="width=1120"> <meta property="og:title" content="Erfüllbarkeitsproblem der Aussagenlogik – Wikipedia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//de.m.wikipedia.org/wiki/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik"> <link rel="alternate" type="application/x-wiki" title="Seite bearbeiten" href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit"> <link rel="apple-touch-icon" href="/static/apple-touch/wikipedia.png"> <link rel="icon" href="/static/favicon/wikipedia.ico"> <link rel="search" type="application/opensearchdescription+xml" href="/w/rest.php/v1/search" title="Wikipedia (de)"> <link rel="EditURI" type="application/rsd+xml" href="//de.wikipedia.org/w/api.php?action=rsd"> <link rel="canonical" href="https://de.wikipedia.org/wiki/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.de"> <link rel="alternate" type="application/atom+xml" title="Atom-Feed für „Wikipedia“" href="/w/index.php?title=Spezial:Letzte_%C3%84nderungen&feed=atom"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="//login.wikimedia.org"> </head> <body class="skin-vector-legacy mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-Erfüllbarkeitsproblem_der_Aussagenlogik rootpage-Erfüllbarkeitsproblem_der_Aussagenlogik skin-vector action-view"><div id="mw-page-base" class="noprint"></div> <div id="mw-head-base" class="noprint"></div> <div id="content" class="mw-body" role="main"> <a id="top"></a> <div id="siteNotice"></div> <div class="mw-indicators"> </div> <h1 id="firstHeading" class="firstHeading mw-first-heading">Erfüllbarkeitsproblem der Aussagenlogik</h1> <div id="bodyContent" class="vector-body"> <div id="siteSub" class="noprint">aus Wikipedia, der freien Enzyklopädie</div> <div id="contentSub"><div id="mw-content-subtitle"></div></div> <div id="contentSub2"></div> <div id="jump-to-nav"></div> <a class="mw-jump-link" href="#mw-head">Zur Navigation springen</a> <a class="mw-jump-link" href="#searchInput">Zur Suche springen</a> <div id="mw-content-text" class="mw-body-content"><div class="mw-content-ltr mw-parser-output" lang="de" dir="ltr">Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von <a href="/wiki/Englische_Sprache" title="Englische Sprache">englisch</a> satisfiability „Erfüllbarkeit“) ist ein <a href="/wiki/Entscheidbar" class="mw-redirect" title="Entscheidbar">Entscheidungsproblem</a> der <a href="/wiki/Theoretische_Informatik" title="Theoretische Informatik">theoretischen Informatik</a>. Es beschäftigt sich mit der Frage, ob eine gegebene <a href="/wiki/Aussagenlogik" title="Aussagenlogik">aussagenlogische</a> <a href="/wiki/Formel" title="Formel">Formel</a> <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> erfüllbar ist. Mit anderen Worten: Existiert eine Belegung der Variablen von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> mit den Werten wahr oder falsch, sodass <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> zu wahr ausgewertet wird? SAT gehört zur <a href="/wiki/Komplexit%C3%A4tsklasse" title="Komplexitätsklasse">Komplexitätsklasse</a> <a href="/wiki/NP_(Komplexit%C3%A4tsklasse)" title="NP (Komplexitätsklasse)">NP</a> der Probleme, die von einer <a href="/wiki/Nichtdeterministische_Turingmaschine" title="Nichtdeterministische Turingmaschine">nichtdeterministischen Turingmaschine</a> in polynomieller Zeit verifiziert werden können. Außerdem war SAT das erste Problem, für das <a href="/wiki/NP-Vollst%C3%A4ndigkeit" title="NP-Vollständigkeit">NP-Vollständigkeit</a> nachgewiesen wurde (<a href="/wiki/Satz_von_Cook" title="Satz von Cook">Satz von Cook</a>). Damit kann jedes Problem aus NP in polynomieller Zeit auf SAT zurückgeführt werden (<a href="/wiki/Polynomialzeitreduktion" title="Polynomialzeitreduktion">Polynomialzeitreduktion</a>). NP-vollständige Probleme stellen also eine Art obere Schranke für die Schwierigkeit von Problemen in NP dar. Eine deterministische <a href="/wiki/Turingmaschine" title="Turingmaschine">Turingmaschine</a> (etwa ein konventioneller Computer) kann SAT in <a href="/wiki/EXPTIME" title="EXPTIME">exponentieller Zeit</a> <a href="/wiki/Entscheidbar" class="mw-redirect" title="Entscheidbar">entscheiden</a>, zum Beispiel durch das Aufstellen einer <a href="/wiki/Wahrheitstabelle" title="Wahrheitstabelle">Wahrheitstabelle</a>. Es ist kein effizienter Algorithmus für SAT bekannt und es wird allgemein vermutet, dass ein solcher <a href="/wiki/Polynomialzeit" title="Polynomialzeit">Polynomialzeitalgorithmus</a> nicht existiert. Die Frage, ob SAT in polynomieller Zeit gelöst werden kann, ist äquivalent zum <a href="/wiki/P-NP-Problem" title="P-NP-Problem">P-NP-Problem</a>, einem der bekanntesten offenen Probleme der theoretischen Informatik Ein Großteil der Forschung beschäftigt sich mit der Entwicklung möglichst effizienter Verfahren zur Lösung von SAT in der Praxis (sogenannter SAT-Solver). Moderne SAT-Solver können Instanzen mittlerer Schwierigkeit mit hunderten Millionen Variablen oder Klauseln in praktikabler Zeit lösen.<a href="#cite_note-1">[1]</a> Das ist ausreichend für praktische Anwendungen, z. B. in der <a href="/wiki/Verifizierung#Automatisierte/formale_Verifikation" title="Verifizierung">formalen Verifikation</a><a href="#cite_note-Verification-2">[2]</a>, in der <a href="/wiki/K%C3%BCnstliche_Intelligenz" title="Künstliche Intelligenz">künstlichen Intelligenz</a><a href="#cite_note-10.5555/145448.146725-3">[3]</a>, in der <a href="/wiki/Electronic_Design_Automation" title="Electronic Design Automation">Electronic Design Automation</a><a href="#cite_note-10.1145/337292.337611-4">[4]</a> und in verschiedenen Planungs- und <a href="/wiki/Scheduling_(Informatik)" class="mw-redirect" title="Scheduling (Informatik)">Schedulingalgorithmen</a><a href="#cite_note-10.2991/icmse-18.2018.126-5">[5]</a>. Sie gehören zu den <a href="/wiki/Constraint_Satisfaction_Problem" class="mw-redirect" title="Constraint Satisfaction Problem">Constraint Satisfaction Problems</a> (CSP). <div id="toc" class="toc" role="navigation" aria-labelledby="mw-toc-heading"><input type="checkbox" role="button" id="toctogglecheckbox" class="toctogglecheckbox" style="display:none" /><div class="toctitle" lang="de" dir="ltr"><h2 id="mw-toc-heading">Inhaltsverzeichnis</h2><label class="toctogglelabel" for="toctogglecheckbox"></label></div> <ul> <li class="toclevel-1 tocsection-1"><a href="#Terminologie">1 Terminologie</a></li> <li class="toclevel-1 tocsection-2"><a href="#Definition_und_Varianten">2 Definition und Varianten</a> <ul> <li class="toclevel-2 tocsection-3"><a href="#Polynomiell_entscheidbare_Varianten_von_SAT">2.1 Polynomiell entscheidbare Varianten von SAT</a></li> <li class="toclevel-2 tocsection-4"><a href="#3-SAT">2.2 3-SAT</a></li> <li class="toclevel-2 tocsection-5"><a href="#P3-SAT">2.3 P3-SAT</a></li> <li class="toclevel-2 tocsection-6"><a href="#MAX-SAT_und_MAJ-SAT">2.4 MAX-SAT und MAJ-SAT</a></li> <li class="toclevel-2 tocsection-7"><a href="#MAJ-SAT">2.5 MAJ-SAT</a></li> <li class="toclevel-2 tocsection-8"><a href="#QBF_(QSAT)">2.6 QBF (QSAT)</a></li> </ul> </li> <li class="toclevel-1 tocsection-9"><a href="#Algorithmen">3 Algorithmen</a> <ul> <li class="toclevel-2 tocsection-10"><a href="#Backtracking_und_DPLL">3.1 Backtracking und DPLL</a> <ul> <li class="toclevel-3 tocsection-11"><a href="#Einheitsresolution_(Unit_Propagation)">3.1.1 Einheitsresolution (Unit Propagation)</a></li> <li class="toclevel-3 tocsection-12"><a href="#Pure_Literal_Elimination">3.1.2 Pure Literal Elimination</a></li> </ul> </li> <li class="toclevel-2 tocsection-13"><a href="#Conflict-Driven_Clause_Learning_(CDCL)">3.2 Conflict-Driven Clause Learning (CDCL)</a> <ul> <li class="toclevel-3 tocsection-14"><a href="#Backjumping_und_Clause_Learning">3.2.1 Backjumping und Clause Learning</a></li> <li class="toclevel-3 tocsection-15"><a href="#Conflict_Clauses">3.2.2 Conflict Clauses</a></li> <li class="toclevel-3 tocsection-16"><a href="#Two_Watched_Literals_(TWL,_2WL)">3.2.3 Two Watched Literals (TWL, 2WL)</a></li> <li class="toclevel-3 tocsection-17"><a href="#Random_Restart">3.2.4 Random Restart</a></li> </ul> </li> <li class="toclevel-2 tocsection-18"><a href="#Lokale_Suche">3.3 Lokale Suche</a></li> </ul> </li> <li class="toclevel-1 tocsection-19"><a href="#Parallelisierung">4 Parallelisierung</a> <ul> <li class="toclevel-2 tocsection-20"><a href="#Portfolio">4.1 Portfolio</a></li> <li class="toclevel-2 tocsection-21"><a href="#Cube-And-Conquer">4.2 Cube-And-Conquer</a></li> <li class="toclevel-2 tocsection-22"><a href="#Parallele_lokale_Suche">4.3 Parallele lokale Suche</a></li> </ul> </li> <li class="toclevel-1 tocsection-23"><a href="#Praxis">5 Praxis</a></li> <li class="toclevel-1 tocsection-24"><a href="#Siehe_auch">6 Siehe auch</a></li> <li class="toclevel-1 tocsection-25"><a href="#Einzelnachweise">7 Einzelnachweise</a></li> </ul> </div> <div class="mw-heading mw-heading2"><h2 id="Terminologie">Terminologie</h2>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=1" title="Abschnitt bearbeiten: Terminologie" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=1" title="Quellcode des Abschnitts bearbeiten: Terminologie">Quelltext bearbeiten</a>]</div> Eine aussagenlogische Formel besteht aus Variablen, Klammern und den aussagenlogischen Verknüpfungen <a href="/wiki/Konjunktion_(Logik)" title="Konjunktion (Logik)">Konjunktion</a> („und“, oft notiert mit ∧), <a href="/wiki/Disjunktion" title="Disjunktion">Disjunktion</a> („oder“, ∨) und <a href="/wiki/Negationszeichen" title="Negationszeichen">Negation</a> („nicht“, ¬). Eine Variable kann entweder den Wert wahr oder den Wert falsch annehmen. Ein Literal ist ein Auftreten einer Variable (positives Literal) oder ihrer Negation (negatives Literal). Ein Literal heißt pur, wenn es nur in einer Ausprägung, also entweder positiv oder negativ, vorkommt. Ein <a href="/wiki/Konjunktionsterm" title="Konjunktionsterm">Monom</a> ist eine endliche Menge von Literalen, die ausschließlich konjunktiv verknüpft sind. Eine <a href="/wiki/Disjunktionsterm" title="Disjunktionsterm">Klausel</a> ist eine endliche Menge von Literalen, die ausschließlich disjunktiv verknüpft sind. Eine Einheitsklausel ist eine Klausel, die nur aus einem einzelnen Literal besteht. Eine Horn-Klausel ist eine Klausel mit höchstens einem positiven Literal. Eine aussagenlogische Formel ist in <a href="/wiki/Konjunktive_Normalform" title="Konjunktive Normalform">konjunktiver Normalform</a> (KNF), wenn sie nur aus Konjunktionen von Klauseln besteht. Eine <a href="/wiki/Horn-Formel" title="Horn-Formel">Horn-Formel</a> ist eine konjunktive Normalform, die ausschließlich aus Horn-Klauseln besteht. Die Formel <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (x_{1}\lor \lnot x_{2})\land (\lnot x_{1}\lor x_{2}\lor x_{3})\land \lnot x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msub> <mo stretchy="false">)</mo> <mo>∧</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> <mo>∨</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msub> <mo>∨</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> <mo stretchy="false">)</mo> <mo>∧</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (x_{1}\lor \lnot x_{2})\land (\lnot x_{1}\lor x_{2}\lor x_{3})\land \lnot x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/ca330f9d3e56b4e98a0cd170a28643e1b7e258f5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:35.486ex; height:2.843ex;" alt="{\displaystyle (x_{1}\lor \lnot x_{2})\land (\lnot x_{1}\lor x_{2}\lor x_{3})\land \lnot x_{1}}"> befindet sich in konjunktiver Normalform. Da nur die erste und die dritte Klausel Horn-Klauseln sind, ist sie aber keine Horn-Formel. Die dritte Klausel ist eine Einheitsklausel. Eine aussagenlogische Formel ist in <a href="/wiki/Disjunktive_Normalform" title="Disjunktive Normalform">disjunktiver Normalform</a> (DNF), wenn sie nur aus Disjunktionen von Monomen besteht. Die Formel <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (x_{1}\land \lnot x_{2})\lor (\lnot x_{1}\land x_{2}\land x_{3})\lor \lnot x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> <mo>∧</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msub> <mo stretchy="false">)</mo> <mo>∨</mo> <mo stretchy="false">(</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> <mo>∧</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msub> <mo>∧</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> <mo stretchy="false">)</mo> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (x_{1}\land \lnot x_{2})\lor (\lnot x_{1}\land x_{2}\land x_{3})\lor \lnot x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/865e99b6f58ddb1581f45ec313ffd212eabe1262" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:35.486ex; height:2.843ex;" alt="{\displaystyle (x_{1}\land \lnot x_{2})\lor (\lnot x_{1}\land x_{2}\land x_{3})\lor \lnot x_{1}}"> befindet sich in disjunktiver Normalform. <div class="mw-heading mw-heading2"><h2 id="Definition_und_Varianten">Definition und Varianten</h2>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=2" title="Abschnitt bearbeiten: Definition und Varianten" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=2" title="Quellcode des Abschnitts bearbeiten: Definition und Varianten">Quelltext bearbeiten</a>]</div> Eine Formel <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> heißt genau dann erfüllbar, wenn eine Zuweisung von Werten wahr oder falsch zu jeder Variable existiert, sodass die Formel wahr ist. Formal ist SAT definiert als die <a href="/wiki/Formale_Sprache" title="Formale Sprache">formale Sprache</a> <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle SAT=\{F\ |\ F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>S</mi> <mi>A</mi> <mi>T</mi> <mo>=</mo> <mo fence="false" stretchy="false">{</mo> <mi>F</mi> <mtext> </mtext> <mrow class="MJX-TeXAtom-ORD"> <mo stretchy="false">|</mo> </mrow> <mtext> </mtext> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle SAT=\{F\ |\ F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4fff83e4c3fa201306328e3bc67f9af0206d3cdc" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:14.429ex; height:2.843ex;" alt="{\displaystyle SAT=\{F\ |\ F}"> ist aussagenlogische Formel und erfüllbar <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo fence="false" stretchy="false">}</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2cf208e5d370391e66767f13641bd5ee6ad93825" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:1.162ex; height:2.843ex;" alt="{\displaystyle \}}"> In der Praxis versteht man unter SAT meistens das Problem, herauszufinden ob eine Formel <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> erfüllbar ist. Es existieren zahlreiche Varianten und für die meisten <a href="/wiki/Komplexit%C3%A4tsklasse" title="Komplexitätsklasse">Komplexitätsklassen</a> existiert eine Variante von SAT, die bezüglich dieser Klasse <a href="/wiki/Schwere_und_Vollst%C3%A4ndigkeit_(theoretische_Informatik)" title="Schwere und Vollständigkeit (theoretische Informatik)">vollständig</a> ist. <div class="mw-heading mw-heading3"><h3 id="Polynomiell_entscheidbare_Varianten_von_SAT">Polynomiell entscheidbare Varianten von SAT</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=3" title="Abschnitt bearbeiten: Polynomiell entscheidbare Varianten von SAT" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=3" title="Quellcode des Abschnitts bearbeiten: Polynomiell entscheidbare Varianten von SAT">Quelltext bearbeiten</a>]</div> <ul><li>HORNSAT beschränkt SAT auf Horn-Formeln, das heißt auf Formeln in konjunktiver Normalform bei der jede Klausel höchstens ein positives Literal enthält. HORNSAT ist <a href="/wiki/P-Vollst%C3%A4ndigkeit" class="mw-redirect" title="P-Vollständigkeit">P-vollständig</a> und in Linearzeit entscheidbar.<a href="#cite_note-6">[6]</a></li> <li>DNF-SAT beschränkt SAT auf Formeln, die in disjunktiver Normalform gegeben sind. DNF-SAT ist in polynomieller Zeit entscheidbar, da eine in DNF gegebene Formel genau dann erfüllbar ist, wenn es ein Monom gibt das keine komplementären Literale enthält.</li> <li>2-SAT beschränkt SAT auf Formeln, deren Klauseln maximal 2 Literale enthalten. 2-SAT ist in Linearzeit entscheidbar.<a href="#cite_note-7">[7]</a></li></ul> <div class="mw-heading mw-heading3"><h3 id="3-SAT">3-SAT</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=4" title="Abschnitt bearbeiten: 3-SAT" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=4" title="Quellcode des Abschnitts bearbeiten: 3-SAT">Quelltext bearbeiten</a>]</div> Das Problem <a href="/wiki/3-SAT" title="3-SAT">3-SAT</a> schränkt die Anzahl Literale auf 3 Literale pro Klausel ein. Trotz dieser Einschränkung ist 3-SAT NP-vollständig, da SAT sich in polynomieller Zeit auf 3-SAT reduzieren lässt. Dasselbe gilt für alle Probleme k-SAT mit k > 3. <div class="mw-heading mw-heading3"><h3 id="P3-SAT">P3-SAT</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=5" title="Abschnitt bearbeiten: P3-SAT" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=5" title="Quellcode des Abschnitts bearbeiten: P3-SAT">Quelltext bearbeiten</a>]</div> Eine Instanz des Problems 3-SAT, bestehend aus p Variablen und q Klauseln, lässt sich auch mittels eines <a href="/wiki/Graph_(Graphentheorie)" title="Graph (Graphentheorie)">Graphen</a> mit (p + q) vielen <a href="/wiki/Knoten_(Graphentheorie)" title="Knoten (Graphentheorie)">Knoten</a> darstellen. Eine Formel ist in P3-SAT, wenn sie in 3-SAT ist und dieser Graph planar ist. P3-SAT ist NP-vollständig. <div class="mw-heading mw-heading3"><h3 id="MAX-SAT_und_MAJ-SAT">MAX-SAT und MAJ-SAT</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=6" title="Abschnitt bearbeiten: MAX-SAT und MAJ-SAT" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=6" title="Quellcode des Abschnitts bearbeiten: MAX-SAT und MAJ-SAT">Quelltext bearbeiten</a>]</div> Das Problem MAX-SAT besteht darin, die maximale Anzahl erfüllbarer Klauseln einer gegebenen Formel zu bestimmen. MAX-SAT ist NP-vollständig und sogar <a href="/wiki/Approximationsalgorithmus#APX" title="Approximationsalgorithmus">APX</a>-vollständig. Daraus folgt, dass kein <a href="/wiki/Approximationsalgorithmus#PTAS/PAS" title="Approximationsalgorithmus">PTAS</a> für MAX-SAT existieren kann, falls P ≠ NP.<a href="#cite_note-8">[8]</a> <div class="mw-heading mw-heading3"><h3 id="MAJ-SAT">MAJ-SAT</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=7" title="Abschnitt bearbeiten: MAJ-SAT" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=7" title="Quellcode des Abschnitts bearbeiten: MAJ-SAT">Quelltext bearbeiten</a>]</div> MAJ-SAT ist das Problem zu entscheiden, ob die Mehrzahl aller möglichen Variablenbelegungen die Formel erfüllt. MAJ-SAT ist <a href="/wiki/Probabilistische_Polynomialzeit" title="Probabilistische Polynomialzeit">PP-vollständig</a>.<a href="#cite_note-9">[9]</a> <div class="mw-heading mw-heading3"><h3 id="QBF_(QSAT)">QBF (QSAT)</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=8" title="Abschnitt bearbeiten: QBF (QSAT)" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=8" title="Quellcode des Abschnitts bearbeiten: QBF (QSAT)">Quelltext bearbeiten</a>]</div> QBF verallgemeinert SAT für quantifizierte, aussagenlogische Formeln, also Formeln, die <a href="/wiki/Quantor" title="Quantor">Quantoren</a> enthalten. QBF ist <a href="/wiki/PSPACE" title="PSPACE">PSPACE</a>-vollständig. <div class="mw-heading mw-heading2"><h2 id="Algorithmen">Algorithmen</h2>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=9" title="Abschnitt bearbeiten: Algorithmen" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=9" title="Quellcode des Abschnitts bearbeiten: Algorithmen">Quelltext bearbeiten</a>]</div> Da SAT NP-vollständig ist, sind ausschließlich Exponentialzeitalgorithmen für SAT bekannt. Seit den 2000er-Jahren werden aber effiziente und skalierbare Algorithmen (SAT-Solver) entwickelt, die praktikables SAT-Solving für zahlreiche Anwendungen erlauben. Beispiele für Anwendungen sind <a href="/wiki/Verifizierung#Automatisierte/formale_Verifikation" title="Verifizierung">formale Verifikation</a>,<a href="#cite_note-Verification-2">[2]</a> <a href="/wiki/K%C3%BCnstliche_Intelligenz" title="Künstliche Intelligenz">Künstliche Intelligenz</a>,<a href="#cite_note-10.5555/145448.146725-3">[3]</a> <a href="/wiki/Electronic_Design_Automation" title="Electronic Design Automation">Electronic Design Automation</a><a href="#cite_note-10.1145/337292.337611-4">[4]</a> und verschiedene Planungs- und <a href="/wiki/Scheduling_(Informatik)" class="mw-redirect" title="Scheduling (Informatik)">Schedulingalgorithmen</a>.<a href="#cite_note-10.2991/icmse-18.2018.126-5">[5]</a> SAT-Solver können aufgrund ihrer Funktionsweise in verschiedene Klassen eingeteilt werden. Ein grundlegender randomisierter Algorithmus zur Lösung des k-SAT-Problems stammt von <a href="/wiki/Uwe_Sch%C3%B6ning" title="Uwe Schöning">Uwe Schöning</a> (1999), die Randomisierung konnte später von <a href="/wiki/Robin_A._Moser" title="Robin A. Moser">Robin A. Moser</a> vollständig entfernt werden (um 2009). Der schnellste bekannte (randomisierte) Algorithmus für allgemeines k-SAT ist PPSZ (Ramamohan Paturi, Pavel Pudlák, <a href="/wiki/Michael_E._Saks" class="mw-redirect" title="Michael E. Saks">Michael E. Saks</a>, Francis Zane),<a href="#cite_note-10">[10]</a><a href="#cite_note-11">[11]</a> entstanden aus dem Vorläufer PPZ von 1999, der nicht so gut wie der Algorithmus von Schöning war, und basierend auf Encoding. 2014 gab <a href="/w/index.php?title=Timon_Hertli&action=edit&redlink=1" class="new" title="Timon Hertli (Seite nicht vorhanden)">Timon Hertli</a> Verbesserungen für den Fall unique 3-SAT.<a href="#cite_note-12">[12]</a> <div class="mw-heading mw-heading3"><h3 id="Backtracking_und_DPLL">Backtracking und DPLL</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=10" title="Abschnitt bearbeiten: Backtracking und DPLL" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=10" title="Quellcode des Abschnitts bearbeiten: Backtracking und DPLL">Quelltext bearbeiten</a>]</div> Der Davis-Putnam-Logemann-Loveland-Algorithmus (DPLL oder DLL) aus den 1960er-Jahren war der erste SAT-Solver, der eine systematische Suche mittels Backtracking implementierte.<a href="#cite_note-13">[13]</a><a href="#cite_note-14">[14]</a> Er ist nicht zu verwechseln mit dem <a href="/wiki/Davis-Putnam-Verfahren" title="Davis-Putnam-Verfahren">Davis-Putnam-Algorithmus</a>, auf dem er basiert. Viele moderne Ansätze basieren auf dem gleichen Konzept und optimieren oft lediglich die Effizienz des Algorithmus für bestimmte Klassen von Eingaben, wie z. B. zufällige SAT-Instanzen oder Instanzen, die in Anwendungen der Industrie auftreten.<a href="#cite_note-15">[15]</a> DPLL löst das CNF-SAT-Problem. Das bedeutet, die aussagenlogischen Formeln müssen in der konjunktiven Normalform vorliegen (Menge von Klauseln). Ein grundlegender Backtracking-Algorithmus für eine Formel <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> funktioniert wie folgt: <ol><li>Wähle ein Literal <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/829091f745070b9eb97a80244129025440a1cfac" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}"> aus <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}">.</li> <li>Weise <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/829091f745070b9eb97a80244129025440a1cfac" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}"> einen Wahrheitswert wahr oder falsch zu.</li> <li>Vereinfache <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> zu <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F_{l}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>F</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>l</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F_{l}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b6bb069206e29d27efd08fa7d04ba7463fa4e0a9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.217ex; height:2.509ex;" alt="{\displaystyle F_{l}}">, indem alle Klauseln entfernt werden, die nun wahr sind und alle Literale entfernt werden, die nun falsch sind.</li> <li>Splitting Rule. Prüfe rekursiv, ob <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F_{l}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>F</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>l</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F_{l}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b6bb069206e29d27efd08fa7d04ba7463fa4e0a9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.217ex; height:2.509ex;" alt="{\displaystyle F_{l}}"> erfüllbar ist. <ul><li><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F_{l}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>F</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>l</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F_{l}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b6bb069206e29d27efd08fa7d04ba7463fa4e0a9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.217ex; height:2.509ex;" alt="{\displaystyle F_{l}}"> ist erfüllbar <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \implies }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mspace width="thickmathspace" /> <mo stretchy="false">⟹</mo> <mspace width="thickmathspace" /> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \implies }</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/913c2e89ea94dfa446f69b056d4bf505e01fcc5f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.096ex; height:1.843ex;" alt="{\displaystyle \implies }"> <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> ist erfüllbar.</li> <li><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F_{l}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>F</mi> <mrow class="MJX-TeXAtom-ORD"> <mi>l</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F_{l}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b6bb069206e29d27efd08fa7d04ba7463fa4e0a9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.217ex; height:2.509ex;" alt="{\displaystyle F_{l}}"> ist nicht erfüllbar: Weise <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/829091f745070b9eb97a80244129025440a1cfac" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}"> den komplementären Wahrheitswert zu. Vereinfache und prüfe dann erneut rekursiv, ob die resultierende Formel <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F_{\lnot l}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>F</mi> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">¬</mi> <mi>l</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F_{\lnot l}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5ca0fbcfc13cc01c26b7d26f8dbf2dc7e23a3ec9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.313ex; height:2.509ex;" alt="{\displaystyle F_{\lnot l}}"> erfüllbar ist. Ist <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F_{\lnot l}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>F</mi> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">¬</mi> <mi>l</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F_{\lnot l}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5ca0fbcfc13cc01c26b7d26f8dbf2dc7e23a3ec9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.313ex; height:2.509ex;" alt="{\displaystyle F_{\lnot l}}"> erfüllbar, so ist auch <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> erfüllbar. Ist <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F_{\lnot l}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>F</mi> <mrow class="MJX-TeXAtom-ORD"> <mi mathvariant="normal">¬</mi> <mi>l</mi> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F_{\lnot l}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5ca0fbcfc13cc01c26b7d26f8dbf2dc7e23a3ec9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.313ex; height:2.509ex;" alt="{\displaystyle F_{\lnot l}}"> nicht erfüllbar, so ist auch <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>F</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle F}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/545fd099af8541605f7ee55f08225526be88ce57" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}"> nicht erfüllbar.</li></ul></li></ol> Der Algorithmus terminiert, wenn eine Klausel leer wird (nicht erfüllbar, ihr letztes Literal wurde falsch) oder wenn alle Variablen belegt sind (erfüllbar). DPLL verbessert den simplen Backtracking-Algorithmus durch zwei Regeln. <div class="mw-heading mw-heading4"><h4 id="Einheitsresolution_(Unit_Propagation)">Einheitsresolution (Unit Propagation)</h4>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=11" title="Abschnitt bearbeiten: Einheitsresolution (Unit Propagation)" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=11" title="Quellcode des Abschnitts bearbeiten: Einheitsresolution (Unit Propagation)">Quelltext bearbeiten</a>]</div> Tritt eine Einheitsklausel <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \psi }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>ψ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \psi }</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/45e5789e5d9c8f7c79744f43ecaaf8ba42a8553a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.513ex; height:2.509ex;" alt="{\displaystyle \psi }"> auf, so muss ihr einziges Literal wahr sein. Weise dem Literal den entsprechenden Wahrheitswert zu und entferne alle Klauseln, die <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \psi }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>ψ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \psi }</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/45e5789e5d9c8f7c79744f43ecaaf8ba42a8553a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:1.513ex; height:2.509ex;" alt="{\displaystyle \psi }"> enthalten. Entferne Vorkommen des Literals <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot \psi }"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi>ψ</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot \psi }</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e95306a224ed882b91ba0a7f0e7f297f49b9023d" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.063ex; height:2.509ex;" alt="{\displaystyle \lnot \psi }"> aus allen Klauseln. In der Praxis führt Einheitsresolution oft dazu, dass wiederum Einheitsklauseln erzeugt werden und somit der naive Suchraum signifikant verkleinert wird. <div class="mw-heading mw-heading4"><h4 id="Pure_Literal_Elimination">Pure Literal Elimination</h4>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=12" title="Abschnitt bearbeiten: Pure Literal Elimination" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=12" title="Quellcode des Abschnitts bearbeiten: Pure Literal Elimination">Quelltext bearbeiten</a>]</div> Kommt ein Literal als pures Literal vor, so kann ihm ein Wert zugewiesen werden, sodass alle Klauseln, die das Literal enthalten, wahr werden. Entferne diese Klauseln. Der Algorithmus zusammengefasst im Pseudocode: <pre>function DPLL(F : set of clauses) # Konsistent bedeutet, es kommt ausschließlich ¬l oder l vor if F is a consistent set of literals then # Hier können zusätzlich die Literale zurückgegeben werden return true; if F contains an empty clause then return false; for every unit clause {l} in F do F ← unit-propagate(l, F); for every literal l that occurs pure in F do F ← pure-literal-assign(l, F); l ← choose-literal(F); # Mit <a href="/wiki/Kurzschlussauswertung" title="Kurzschlussauswertung">Kurzschlussauswertung</a> für das Oder return DPLL({F : l = true}) or DPLL({F : l = true}); # </pre> Dabei wenden unit-propagate(l, F) und pure-literal-assign(l, F) die beiden Regeln entsprechend an und geben die vereinfachte Formel zurück. Die Effizienz von DPLL hängt sehr stark von der Auswahl des Literals <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/829091f745070b9eb97a80244129025440a1cfac" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}"> (Branching Literal) ab. Für manche Instanzen kann diese Wahl den Unterschied zwischen konstanter und exponentieller Laufzeit ausmachen.<a href="#cite_note-16">[16]</a> Darum definiert DPLL vielmehr eine ganze Familie von Algorithmen, die unterschiedliche <a href="/wiki/Heuristik" title="Heuristik">Heuristiken</a> für die Wahl von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/829091f745070b9eb97a80244129025440a1cfac" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}"> verwenden. Die Probleme von DPLL können in drei Punkten zusammengefasst werden: <ol><li>Die Entscheidungen für Branching Literals werden naiv getroffen.</li> <li>Aus Konflikten wird nichts gelernt, außer dass die aktuelle (partielle) Variablenbelegung zu einem Konflikt führt. Dabei lassen sich mehr Informationen über die Ursache des Konfliktes extrahieren und so große Teile des Suchraumes ausschließen.</li> <li>Backtracking springt nur jeweils eine Ebene im Suchbaum nach oben, was zu einem sehr großen Suchraum führt.</li></ol> In der Praxis werden diese Probleme gelöst durch <ol><li>Heuristiken, z. B. in einem Look-Ahead-Solver</li> <li>Clause Learning (CDCL)</li> <li>Backjumping (CDCL)</li></ol> <div class="mw-heading mw-heading3"><h3 id="Conflict-Driven_Clause_Learning_(CDCL)">Conflict-Driven Clause Learning (CDCL)</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=13" title="Abschnitt bearbeiten: Conflict-Driven Clause Learning (CDCL)" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=13" title="Quellcode des Abschnitts bearbeiten: Conflict-Driven Clause Learning (CDCL)">Quelltext bearbeiten</a>]</div> Modernes Conflict-driven Clause Learning (CDCL) erweitert DPLL um die Konzepte Clause Learning und Backjumping, implementiert Two Watched Literals (TWL, 2WL), um die Suche nach Einheitsklauseln zu beschleunigen und verwendet Random Restarts, um schwierigen Situationen nach einer Reihe von schlechten Entscheidungen für Variablenbelegungen zu entfliehen. <div class="mw-heading mw-heading4"><h4 id="Backjumping_und_Clause_Learning">Backjumping und Clause Learning</h4>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=14" title="Abschnitt bearbeiten: Backjumping und Clause Learning" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=14" title="Quellcode des Abschnitts bearbeiten: Backjumping und Clause Learning">Quelltext bearbeiten</a>]</div> Bei CDCL findet das Backtracking nicht mehr chronologisch statt, sondern es werden Ebenen des Suchbaumes übersprungen. Außerdem werden Informationen über Variablenbelegungen, die in Kombination einen Konflikt verursachen, als Klausel der Klauselmenge hinzugefügt. <ul class="gallery mw-gallery-nolines center"> <li class="gallerybox" style="width: 205px"> <div class="thumb" style="width: 200px;"><a href="/wiki/Datei:Backtracking-no-backjumping.svg" class="mw-file-description" title="Backtracking ohne Backjumping"><img alt="Backtracking ohne Backjumping" src="//upload.wikimedia.org/wikipedia/commons/thumb/1/1e/Backtracking-no-backjumping.svg/200px-Backtracking-no-backjumping.svg.png" decoding="async" width="200" height="179" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/1/1e/Backtracking-no-backjumping.svg/300px-Backtracking-no-backjumping.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/1/1e/Backtracking-no-backjumping.svg/400px-Backtracking-no-backjumping.svg.png 2x" data-file-width="171" data-file-height="153" /></a></div> <div class="gallerytext">Backtracking ohne Backjumping</div> </li> <li class="gallerybox" style="width: 205px"> <div class="thumb" style="width: 200px;"><a href="/wiki/Datei:Backtracking-with-backjumping.svg" class="mw-file-description" title="Backtracking mit Backjumping"><img alt="Backtracking mit Backjumping" src="//upload.wikimedia.org/wikipedia/commons/thumb/9/9e/Backtracking-with-backjumping.svg/200px-Backtracking-with-backjumping.svg.png" decoding="async" width="200" height="180" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/9/9e/Backtracking-with-backjumping.svg/300px-Backtracking-with-backjumping.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/9/9e/Backtracking-with-backjumping.svg/400px-Backtracking-with-backjumping.svg.png 2x" data-file-width="180" data-file-height="162" /></a></div> <div class="gallerytext">Backtracking mit Backjumping</div> </li> </ul> Um Backjumping zu ermöglichen, merkt sich CDCL, welche Zuweisungen von Wahrheitswerten zu Variablen willkürlich waren und welche Zuweisungen durch Unit Propagation erzwungen wurden. In der Praxis funktioniert das mittels eines Implikationsgraphen. Ein Implikationsgraph ist ein <a href="/wiki/Gerichteter_azyklischer_Graph" class="mw-redirect" title="Gerichteter azyklischer Graph">gerichteter, azyklischer Graph</a> <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle G=(V,E)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>G</mi> <mo>=</mo> <mo stretchy="false">(</mo> <mi>V</mi> <mo>,</mo> <mi>E</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle G=(V,E)}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/644a8d85ee410b6159ca2bdb5dcb9097e2c8f182" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:11.331ex; height:2.843ex;" alt="{\displaystyle G=(V,E)}">. Jeder Knoten <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle v\in V}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>v</mi> <mo>∈</mo> <mi>V</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle v\in V}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/99886ebbde63daa0224fb9bf56fa11b3c8a6f4fb" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.756ex; height:2.176ex;" alt="{\displaystyle v\in V}"> besteht dabei aus einem Tupel <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle (x\in \{false,true\},\ d)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mo stretchy="false">(</mo> <mi>x</mi> <mo>∈</mo> <mo fence="false" stretchy="false">{</mo> <mi>f</mi> <mi>a</mi> <mi>l</mi> <mi>s</mi> <mi>e</mi> <mo>,</mo> <mi>t</mi> <mi>r</mi> <mi>u</mi> <mi>e</mi> <mo fence="false" stretchy="false">}</mo> <mo>,</mo> <mtext> </mtext> <mi>d</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle (x\in \{false,true\},\ d)}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/1f1469a73236bde0fc0d21324a95f369f0d85d2c" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:21.846ex; height:2.843ex;" alt="{\displaystyle (x\in \{false,true\},\ d)}"> oder einem Element <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle c}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>c</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle c}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/86a67b81c2de995bd608d5b2df50cd8cd7d92455" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.007ex; height:1.676ex;" alt="{\displaystyle c}">. Während das Tupel für eine Zuweisung von wahr oder falsch für ein Literal <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>x</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87f9e315fd7e2ba406057a97300593c4802b53e4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.33ex; height:1.676ex;" alt="{\displaystyle x}"> auf Ebene <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle d}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>d</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle d}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e85ff03cbe0c7341af6b982e47e9f90d235c66ab" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.216ex; height:2.176ex;" alt="{\displaystyle d}"> des Suchbaumes steht, steht <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle c}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>c</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle c}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/86a67b81c2de995bd608d5b2df50cd8cd7d92455" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.007ex; height:1.676ex;" alt="{\displaystyle c}"> für einen aufgetretenen Konflikt. Ein Konflikt tritt auf, wenn ein Literal gleichzeitig den Wert wahr und den Wert falsch annehmen müsste. Wenn der Algorithmus ein Literal willkürlich mit einem Wahrheitswert belegt, wird der entsprechende Knoten <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle v}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>v</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle v}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/e07b00e7fc0847fbd16391c778d65bc25c452597" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.128ex; height:1.676ex;" alt="{\displaystyle v}"> mit dem Tupel, das diese Zuweisung repräsentiert, zu <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle G}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>G</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle G}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f5f3c8921a3b352de45446a6789b104458c9f90b" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.827ex; height:2.176ex;" alt="{\displaystyle G}"> hinzugefügt. Erzwingt diese Zuweisung durch Unit Propagation eine weitere Zuweisung, so wird ein weiterer Knoten <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle w}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>w</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle w}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/88b1e0c8e1be5ebe69d18a8010676fa42d7961e6" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.664ex; height:1.676ex;" alt="{\displaystyle w}"> und eine Kante <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle e=(v,w)}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>e</mi> <mo>=</mo> <mo stretchy="false">(</mo> <mi>v</mi> <mo>,</mo> <mi>w</mi> <mo stretchy="false">)</mo> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle e=(v,w)}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/4c44f467603bbe85d35f31ae56985ec911a67f3a" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:9.817ex; height:2.843ex;" alt="{\displaystyle e=(v,w)}"> zum Graphen hinzugefügt. Im Folgenden ein Beispiel mit der Formel: (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{4}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>4</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{4}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fb828766e82e496666b179ff70d8e2fd24a79e5f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{4}}">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{3}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{3}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d90c8066ee21a9039561dc2e0a7cb75c389d15ba" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{3}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/291ec3a472eae5b24a9dfe6dbfa209ebdc01bcf4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{8}}">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a631ca7c0ec07097af0806f818d3ace2f06429b5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{8}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{12}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>12</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{12}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fbe6f173e4f67cb34854ec175b0f7bce5389ab87" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.206ex; height:2.009ex;" alt="{\displaystyle x_{12}}">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{2}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{2}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d7af1b928f06e4c7e3e8ebfd60704656719bd766" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{2}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{11}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>11</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{11}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/df6e8ee8613c2c8514687bd2db19c01df4d068e5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.206ex; height:2.009ex;" alt="{\displaystyle x_{11}}">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b6d4ae4ceda45261c1e9445a93715d6a93d08ad3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{7}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{3}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{3}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d90c8066ee21a9039561dc2e0a7cb75c389d15ba" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{3}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{9}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>9</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{9}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c315560c3dacd659df30f39c951b82f45fa461f9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{9}}">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b6d4ae4ceda45261c1e9445a93715d6a93d08ad3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{7}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a631ca7c0ec07097af0806f818d3ace2f06429b5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{8}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{9}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>9</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{9}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/38ad1988b64b22da4f4645a971bf337d848ecdb5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{9}}">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/954c46116945ae4026c359eec235f65b6c408df8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{7}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a631ca7c0ec07097af0806f818d3ace2f06429b5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{8}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{10}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>10</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{10}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2eda03d236b0a3c47969e9be89e42e143af1d4fe" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.756ex; height:2.009ex;" alt="{\displaystyle \lnot x_{10}}">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/954c46116945ae4026c359eec235f65b6c408df8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{7}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{12}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>12</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{12}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87554ad5d7c5c21711e18034639b74dba18ed178" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.756ex; height:2.009ex;" alt="{\displaystyle \lnot x_{12}}">) <ul class="gallery mw-gallery-nolines" style="float:right;"> <li class="gallerybox" style="width: 205px"> <div class="thumb" style="width: 200px;"><a href="/wiki/Datei:Cdcl_implication_graph_2.png" class="mw-file-description" title="Implikationsgraph nach dem 8. Schritt"><img alt="Implikationsgraph nach dem 8. Schritt" src="//upload.wikimedia.org/wikipedia/commons/thumb/5/5d/Cdcl_implication_graph_2.png/200px-Cdcl_implication_graph_2.png" decoding="async" width="200" height="200" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/5/5d/Cdcl_implication_graph_2.png 1.5x" data-file-width="300" data-file-height="300" /></a></div> <div class="gallerytext">Implikationsgraph nach dem 8. Schritt</div> </li> <li class="gallerybox" style="width: 205px"> <div class="thumb" style="width: 200px;"><a href="/wiki/Datei:Implication_graph_collision.png" class="mw-file-description" title="Implikationsgraph mit Konflikt"><img alt="Implikationsgraph mit Konflikt" src="//upload.wikimedia.org/wikipedia/commons/thumb/2/29/Implication_graph_collision.png/200px-Implication_graph_collision.png" decoding="async" width="200" height="200" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/2/29/Implication_graph_collision.png 1.5x" data-file-width="300" data-file-height="300" /></a></div> <div class="gallerytext">Implikationsgraph mit Konflikt</div> </li> </ul> <ol><li>Wähle <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> willkürlich und belege es (wieder willkürlich) mit false.</li> <li>Unit Propagation erzwingt eine Belegung von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{4}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>4</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{4}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fb828766e82e496666b179ff70d8e2fd24a79e5f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{4}}"> mit true. Damit wird die Klausel (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{4}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>4</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{4}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fb828766e82e496666b179ff70d8e2fd24a79e5f" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{4}}">) wahr.</li> <li>Wähle <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{3}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{3}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/766d09a498699be10e276ad49145c921f8cbe335" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{3}}"> und belege es mit true.</li> <li>Unit Propagation erzwingt nun die Belegung von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a631ca7c0ec07097af0806f818d3ace2f06429b5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{8}}"> mit false (wegen <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> = false). Die Klausel (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{3}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{3}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d90c8066ee21a9039561dc2e0a7cb75c389d15ba" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{3}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/291ec3a472eae5b24a9dfe6dbfa209ebdc01bcf4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{8}}">) wird wahr.</li> <li>Unit Propagation erzwingt die Belegung von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{12}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>12</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{12}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fbe6f173e4f67cb34854ec175b0f7bce5389ab87" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.206ex; height:2.009ex;" alt="{\displaystyle x_{12}}"> mit true (wegen <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a631ca7c0ec07097af0806f818d3ace2f06429b5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{8}}"> = false). Die Kausel (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a631ca7c0ec07097af0806f818d3ace2f06429b5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{8}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{12}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>12</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{12}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/fbe6f173e4f67cb34854ec175b0f7bce5389ab87" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.206ex; height:2.009ex;" alt="{\displaystyle x_{12}}">) wird wahr.</li> <li>Wähle <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{2}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{2}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d7af1b928f06e4c7e3e8ebfd60704656719bd766" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{2}}"> und belege es mit false.</li> <li>Unit Propagation erzwingt nun die Belegung von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{11}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>11</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{11}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/df6e8ee8613c2c8514687bd2db19c01df4d068e5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.206ex; height:2.009ex;" alt="{\displaystyle x_{11}}"> mit true. Die Klausel (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{2}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>2</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{2}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d7af1b928f06e4c7e3e8ebfd60704656719bd766" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{2}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{11}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>11</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{11}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/df6e8ee8613c2c8514687bd2db19c01df4d068e5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.206ex; height:2.009ex;" alt="{\displaystyle x_{11}}">) wird wahr.</li> <li>Wähle <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/954c46116945ae4026c359eec235f65b6c408df8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{7}}"> und belege es mit true. Die Klauseln (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/954c46116945ae4026c359eec235f65b6c408df8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{7}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a631ca7c0ec07097af0806f818d3ace2f06429b5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{8}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{10}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>10</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{10}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/2eda03d236b0a3c47969e9be89e42e143af1d4fe" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.756ex; height:2.009ex;" alt="{\displaystyle \lnot x_{10}}">) und (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/954c46116945ae4026c359eec235f65b6c408df8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{7}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{12}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>12</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{12}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/87554ad5d7c5c21711e18034639b74dba18ed178" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:4.756ex; height:2.009ex;" alt="{\displaystyle \lnot x_{12}}">) werden wahr.</li> <li>Ein Konflikt tritt auf für <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{9}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>9</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{9}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c315560c3dacd659df30f39c951b82f45fa461f9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{9}}">. Unit Propagation muss die Klauseln (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b6d4ae4ceda45261c1e9445a93715d6a93d08ad3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{7}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{3}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{3}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/d90c8066ee21a9039561dc2e0a7cb75c389d15ba" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{3}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{9}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>9</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{9}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c315560c3dacd659df30f39c951b82f45fa461f9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{9}}">) ∧ (<math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/b6d4ae4ceda45261c1e9445a93715d6a93d08ad3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{7}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a631ca7c0ec07097af0806f818d3ace2f06429b5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{8}}"> ∨ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{9}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>9</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{9}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/38ad1988b64b22da4f4645a971bf337d848ecdb5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{9}}">) erfüllen, die inzwischen zu <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{9}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>9</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{9}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/c315560c3dacd659df30f39c951b82f45fa461f9" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{9}}"> ∧ <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{9}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>9</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{9}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/38ad1988b64b22da4f4645a971bf337d848ecdb5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:3.934ex; height:2.009ex;" alt="{\displaystyle \lnot x_{9}}"> reduziert wurden. Der Konfliktknoten <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle c}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>c</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle c}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/86a67b81c2de995bd608d5b2df50cd8cd7d92455" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.007ex; height:1.676ex;" alt="{\displaystyle c}"> wird in den Implikationsgraphen eingefügt.</li></ol> Der Algorithmus analysiert nun den Konflikt mithilfe des Implikationsgraphen und entscheidet, welche Klausel gelernt werden soll und zu welchem Entscheidungslevel im Suchbaum zurückgesprungen werden soll. In Frage kommende Klauseln heißen conflict clause und sollen verhindern, dass die Fehlentscheidung des Algorithmus, die zum Konflikt geführt hat, wiederholt wird. Eine solche conflict clause wird zur Klauselmenge hinzugefügt. Das maximale Entscheidungslevel der Variablen aus der conflict clause bestimmt das Entscheidungslevel für das Backjumping. Eine abstrakte Beschreibung von CDCL im Pseudocode sieht wie folgt aus:<a href="#cite_note-17">[17]</a> <pre>function CDCL(F : set of clauses) G <- Implikationsgraph(); if unit-propagate(F, G) findet Konflikt then return false; level ← 0; while F hat nicht zugewiesene Variablen do level ← level + 1; choose-literal(F, G); while unit-propagate(F, G) findet Konflikt do # Ermittle Ebene für Backjump und zu lernende Klausel (d, c) ← analyzeConflict(G); # Lerne F ← F ∪ {c}; # Wenn der Konflikt nicht aufgelöst werden kann if d < 0 then return false; else backjump(F, d); level ← d; return true; </pre> Dabei aktualisieren unit-propagate(F, G) und choose-literal(F, G) jeweils entsprechend den Implikationsgraphen. Die Funktion analyzeConflict(G) wird durch die Strategie des clause learning bestimmt. <div class="mw-heading mw-heading4"><h4 id="Conflict_Clauses">Conflict Clauses</h4>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=15" title="Abschnitt bearbeiten: Conflict Clauses" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=15" title="Quellcode des Abschnitts bearbeiten: Conflict Clauses">Quelltext bearbeiten</a>]</div> <figure class="mw-default-size" typeof="mw:File/Thumb"><a href="/wiki/Datei:Implication_Graph_Partition.png" class="mw-file-description"><img alt="Implikationsgraph mit Decision Side und Conflict Side" src="//upload.wikimedia.org/wikipedia/commons/thumb/a/a7/Implication_Graph_Partition.png/220px-Implication_Graph_Partition.png" decoding="async" width="220" height="220" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/a/a7/Implication_Graph_Partition.png/330px-Implication_Graph_Partition.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/a/a7/Implication_Graph_Partition.png/440px-Implication_Graph_Partition.png 2x" data-file-width="528" data-file-height="528" /></a><figcaption>Implikationsgraph mit Decision Side und Conflict Side</figcaption></figure> Um eine conflict clause zu ermitteln untersucht man <a href="/wiki/Schnitt_(Graphentheorie)" title="Schnitt (Graphentheorie)">Schnitte</a> im Implikationsgraphen. Ein Schnitt generiert eine conflict clause genau dann, wenn er den Graph so in zwei Hälften partitioniert, dass eine Hälfte (die decision side) alle decision nodes enthält und die andere Hälfte den Konfliktknoten. Die decision nodes sind dabei die willkürlichen Entscheidungen, die zum Konflikt geführt haben. Aus dem Implikationsgraphen wird ersichtlich, dass z. B. für <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{3}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{3}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/766d09a498699be10e276ad49145c921f8cbe335" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{3}}"> und <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/954c46116945ae4026c359eec235f65b6c408df8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{7}}"> eine willkürliche Entscheidung getroffen wurde, aber die Entscheidung für die Belegung von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a631ca7c0ec07097af0806f818d3ace2f06429b5" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{8}}"> eine Konsequenz aus der Entscheidung für die Belegung von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}"> und <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{3}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{3}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/766d09a498699be10e276ad49145c921f8cbe335" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{3}}"> war. Die Knoten für <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a8788bf85d532fa88d1fb25eff6ae382a601c308" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{3}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{3}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/766d09a498699be10e276ad49145c921f8cbe335" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{3}}">, <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/954c46116945ae4026c359eec235f65b6c408df8" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{7}}"> sind also die decision nodes. Ein Beispiel für einen Schnitt, der eine conflict clause generiert, ist ein Schnitt durch die eingehenden Kanten des Konfliktknotens (roter Schnitt in der Abbildung). Die Knoten auf der decision side repräsentieren die Ursache des Konfliktes, nämlich <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{3}\land x_{7}\land \lnot x_{8}\implies Konflikt}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> <mo>∧</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> <mo>∧</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> <mspace width="thickmathspace" /> <mo stretchy="false">⟹</mo> <mspace width="thickmathspace" /> <mi>K</mi> <mi>o</mi> <mi>n</mi> <mi>f</mi> <mi>l</mi> <mi>i</mi> <mi>k</mi> <mi>t</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle x_{3}\land x_{7}\land \lnot x_{8}\implies Konflikt}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/a66ef8dac6bf2d9d3d2bcbe3e2c65f031e7753f3" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:29.667ex; height:2.509ex;" alt="{\displaystyle x_{3}\land x_{7}\land \lnot x_{8}\implies Konflikt}">. Durch <a href="/wiki/Kontraposition" title="Kontraposition">Kontraposition</a> erhält man <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot Konflikt\implies \lnot x_{3}\lor \lnot x_{7}\lor x_{8}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi>K</mi> <mi>o</mi> <mi>n</mi> <mi>f</mi> <mi>l</mi> <mi>i</mi> <mi>k</mi> <mi>t</mi> <mspace width="thickmathspace" /> <mo stretchy="false">⟹</mo> <mspace width="thickmathspace" /> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> <mo>∨</mo> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> <mo>∨</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>8</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot Konflikt\implies \lnot x_{3}\lor \lnot x_{7}\lor x_{8}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/f5c2359b4444197bb9577209ab9074580a4905f4" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:32.768ex; height:2.509ex;" alt="{\displaystyle \lnot Konflikt\implies \lnot x_{3}\lor \lnot x_{7}\lor x_{8}}">, ein Beispiel für eine conflict clause. Eine andere Möglichkeit stellt der blaue Schnitt durch die ausgehenden Kanten der decision nodes dar. Er generiert die conflict clause <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot x_{1}\lor x_{3}\lor x_{7}}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>1</mn> </mrow> </msub> <mo>∨</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>3</mn> </mrow> </msub> <mo>∨</mo> <msub> <mi>x</mi> <mrow class="MJX-TeXAtom-ORD"> <mn>7</mn> </mrow> </msub> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot x_{1}\lor x_{3}\lor x_{7}}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/699a13e337f3c43374a292d3f2222b83e55a6984" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:13.867ex; height:2.343ex;" alt="{\displaystyle \lnot x_{1}\lor x_{3}\lor x_{7}}">. Diese Variante wurde in Rel_sat<a href="#cite_note-18">[18]</a> implementiert, einem der ersten CDCL SAT-Solver.<a href="#cite_note-19">[19]</a> Eine fortgeschrittene Variante wird von der Implementierung GRASP<a href="#cite_note-20">[20]</a> eingesetzt. <div class="mw-heading mw-heading4"><h4 id="Two_Watched_Literals_(TWL,_2WL)">Two Watched Literals (TWL, 2WL)</h4>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=16" title="Abschnitt bearbeiten: Two Watched Literals (TWL, 2WL)" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=16" title="Quellcode des Abschnitts bearbeiten: Two Watched Literals (TWL, 2WL)">Quelltext bearbeiten</a>]</div> Es bleibt das Problem, Einheitsklauseln für die Unit Propagation und Konflikte effizient zu finden. Lange Zeit haben Solver dafür die Anzahl Literale, die in einer Klausel noch nicht mit Wahrheitswerten belegt worden sind, mitgezählt. Wenn sich dieser Zähler von 2 auf 1 ändert wendet man Unit Propagation an. Da uns der genaue Wert des Zählers aber eigentlich nicht interessiert, sondern wir nur wissen müssen, wann sich die Zahl auf eins ändert, verfolgen wir nicht die Klauseln selbst, sondern jeweils zwei Literale pro Klausel – die two watched literals. TWL ist also eine Datenstruktur, die die Suche nach Konflikten oder Einheitsklauseln beschleunigt. Jede Klausel, die noch nicht erfüllt ist, besitzt zwei watched literals. Die Information wird dabei nicht von den Klauseln gespeichert, sondern von den Literalen selbst. Jeder Literal <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/829091f745070b9eb97a80244129025440a1cfac" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}"> besitzt also eine Liste mit Klauseln, in denen er vorkommt. Diese Klauseln werden in einer Liste verkettet, der watch list. Die TWL einer Klausel erfüllen folgende Invariante: <div class="Vorlage_Zitat" style="margin:1em 40px;"> <div style="margin:1em 0;"><blockquote style="margin:0;"> „Solange kein Konflikt gefunden wurde darf ein watched literal nur false sein, solange der andere watched literal true ist und alle unwatched literals false sind.“<a href="#cite_note-21">[21]</a> </blockquote> </div></div> Die Invariante führt dazu, dass die Belegung eines unwatched literals mit einem Wahrheitswert niemals zu einer unit propagation oder einem Konflikt führen wird. Wenn wir nun aber einem watched literal <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/829091f745070b9eb97a80244129025440a1cfac" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}"> einen Wahrheitswert zuweisen, müssen wir eventuell die Invariante reparieren, unit propagation anwenden oder einen Konflikt auflösen. Betrachten wir die Klauseln, in denen die Negation von <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/829091f745070b9eb97a80244129025440a1cfac" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:0.693ex; height:2.176ex;" alt="{\displaystyle l}">, also <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5b40680c11a08a2bd4c271307a04ece84c1db841" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.244ex; height:2.176ex;" alt="{\displaystyle \lnot l}"> vorkommt. Diese können durch die watch list effizient gefunden werden. Wir verfahren für diese wie folgt: <ol><li>Ist der andere watched literal der Klausel true, müssen wir nichts tun.</li> <li>Ist einer der unwatched literals <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l'}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi>l</mi> <mo>′</mo> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l'}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/efb2e54e32519bf534e146b9140c25b67e558d56" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.378ex; height:2.509ex;" alt="{\displaystyle l'}"> der Klausel nicht false, wählen wir <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l'}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi>l</mi> <mo>′</mo> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l'}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/efb2e54e32519bf534e146b9140c25b67e558d56" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.378ex; height:2.509ex;" alt="{\displaystyle l'}"> als watched literal, der <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \lnot l}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <mi mathvariant="normal">¬</mi> <mi>l</mi> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle \lnot l}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/5b40680c11a08a2bd4c271307a04ece84c1db841" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.244ex; height:2.176ex;" alt="{\displaystyle \lnot l}"> ersetzt.</li> <li>Ist der andere watched literal <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l'}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi>l</mi> <mo>′</mo> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l'}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/efb2e54e32519bf534e146b9140c25b67e558d56" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.378ex; height:2.509ex;" alt="{\displaystyle l'}"> für diese Klausel noch nicht mit einem Wahrheitswert belegt, führe unit propagation für <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l'}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi>l</mi> <mo>′</mo> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l'}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/efb2e54e32519bf534e146b9140c25b67e558d56" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.378ex; height:2.509ex;" alt="{\displaystyle l'}"> durch. Ansonsten ist <math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle l'}"> <semantics> <mrow class="MJX-TeXAtom-ORD"> <mstyle displaystyle="true" scriptlevel="0"> <msup> <mi>l</mi> <mo>′</mo> </msup> </mstyle> </mrow> <annotation encoding="application/x-tex">{\displaystyle l'}</annotation> </semantics> </math><img src="https://wikimedia.org/api/rest_v1/media/math/render/svg/efb2e54e32519bf534e146b9140c25b67e558d56" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.378ex; height:2.509ex;" alt="{\displaystyle l'}"> false und ein Konflikt wurde gefunden.</li></ol> TWL wurde für den SAT-Solver Chaff<a href="#cite_note-22">[22]</a> entwickelt, um die unit propagation in der Praxis zu optimieren. <div class="mw-heading mw-heading4"><h4 id="Random_Restart">Random Restart</h4>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=17" title="Abschnitt bearbeiten: Random Restart" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=17" title="Quellcode des Abschnitts bearbeiten: Random Restart">Quelltext bearbeiten</a>]</div> Random Restarts setzen alle Variablenbelegungen zurück und starten die Suche mit einer anderen Reihenfolge der Variablenbelegung neu. Damit wird das Problem umgangen, dass manche dieser Zuweisungsreihenfolgen zu sehr viel länger andauernden Berechnungen mit vielen Konflikten führen, während geeignete Reihenfolgen das Problem schneller lösen. Dabei werden gelernte Klauseln und die aktuell zugewiesenen Werte der Variablen übernommen. Wann ein Restart durchgeführt wird bestimmt eine Strategie, z. B. fixed nach n Konflikten, in Abständen, die einer Reihe wie der <a href="/wiki/Geometrische_Reihe" title="Geometrische Reihe">geometrischen Reihe</a> folgen oder dynamisch, wenn sich Konflikte beginnen zu häufen. Restart-Strategien sind häufig an eine bestimmte Klasse von Instanzen angepasst und aggressivere Strategien haben sich in vielen Fällen als effizient herausgestellt.<a href="#cite_note-23">[23]</a> <div class="mw-heading mw-heading3"><h3 id="Lokale_Suche">Lokale Suche</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=18" title="Abschnitt bearbeiten: Lokale Suche" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=18" title="Quellcode des Abschnitts bearbeiten: Lokale Suche">Quelltext bearbeiten</a>]</div> SAT-Solver, die auf dem Prinzip der <a href="/wiki/Lokale_Suche" title="Lokale Suche">lokalen Suche</a> basieren, führen im Grunde folgende Schritte aus: <ol><li>Weise jeder Variable einen Zufallswert true oder false zu.</li> <li>Wenn alle Klauseln erfüllt sind, terminiere und gebe die Variablenbelegung zurück.</li> <li>Ansonsten negiere eine Variable und wiederhole.</li></ol> Die aussagenlogische Formel ist dabei als konjunktive Normalform gegeben. Unterschiede zwischen SAT-Solvern, die lokale Suche implementieren, finden sich vor allem bei der Wahl der Variable, die negiert wird. GSAT<a href="#cite_note-24">[24]</a> negiert die Variable, die die Zahl an nicht erfüllten Klauseln minimiert oder wählt mit einer gewissen Wahrscheinlichkeit eine zufällige Variable. WalkSAT<a href="#cite_note-25">[25]</a> wählt eine zufällige, nicht erfüllte Klausel und negiert eine Variable. Dabei wird die Variable ausgewählt, die am wenigsten bereits erfüllte Klauseln nicht erfüllt werden lässt. Die Wahrscheinlichkeit, dass eine falsche Variablenzuweisung korrigiert wird, ist der Kehrwert der Anzahl der Variablen in der Klausel. Mit einer gewissen Wahrscheinlichkeit wird auch hier einfach eine zufällige Variable der Klausel ausgewählt. Beide Varianten erlauben zufällige Zuweisungen mit einer gewissen Wahrscheinlichkeit, um das Problem der lokalen Maxima zu umgehen. Außerdem werden zufällige Neustarts erlaubt, wenn für eine zu lange Zeit keine Lösung gefunden wurde. <div class="mw-heading mw-heading2"><h2 id="Parallelisierung">Parallelisierung</h2>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=19" title="Abschnitt bearbeiten: Parallelisierung" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=19" title="Quellcode des Abschnitts bearbeiten: Parallelisierung">Quelltext bearbeiten</a>]</div> <div class="hauptartikel" role="navigation">→ Hauptartikel: <a href="/wiki/Parallele_Algorithmen_f%C3%BCr_das_Erf%C3%BCllbarkeitsproblem" title="Parallele Algorithmen für das Erfüllbarkeitsproblem">Parallele Algorithmen für das Erfüllbarkeitsproblem</a></div> <a href="/wiki/Parallele_Algorithmen_f%C3%BCr_das_Erf%C3%BCllbarkeitsproblem" title="Parallele Algorithmen für das Erfüllbarkeitsproblem">Parallele SAT-Solver</a> können in drei Kategorien eingeteilt werden: Portfolio, <a href="/wiki/Teile-und-herrsche-Verfahren" title="Teile-und-herrsche-Verfahren">Divide-and-conquer</a> und parallele lokale Suche. <div class="mw-heading mw-heading3"><h3 id="Portfolio">Portfolio</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=20" title="Abschnitt bearbeiten: Portfolio" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=20" title="Quellcode des Abschnitts bearbeiten: Portfolio">Quelltext bearbeiten</a>]</div> Portfolio SAT-Solver beruhen auf der Tatsache, dass die meisten SAT-Solver auf bestimmten Probleminstanzen effizient sind, aber auf anderen Instanzen langsamer sind als andere Algorithmen. Gegeben eine beliebige Instanz von SAT, so gibt es keine verlässliche Möglichkeit, um vorherzusagen, welcher Algorithmus die Instanz am schnellsten lösen wird. Der Portfolio-Ansatz verwendet nun verschiedene Ansätze parallel, um die Vorteile verschiedener SAT-Solver zu kombinieren. Ein Nachteil der Methode ist natürlich, dass alle parallelen Prozesse im Prinzip die gleiche Arbeit verrichten. Trotzdem haben sich Portfolio-Solver in der Praxis als effizient herausgestellt. <div class="mw-heading mw-heading3"><h3 id="Cube-And-Conquer">Cube-And-Conquer</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=21" title="Abschnitt bearbeiten: Cube-And-Conquer" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=21" title="Quellcode des Abschnitts bearbeiten: Cube-And-Conquer">Quelltext bearbeiten</a>]</div> Divide-and-conquer Algorithmen beruhen auf dem Ansatz, ein Problem in kleinere Teilprobleme aufzuteilen, diese rekursiv zu bearbeiten und die Teilergebnisse zu kombinieren. DPLL und CDCL sind divide-and-conquer Algorithmen, die den Suchraum bei jeder Entscheidung für eine Variablenbelegung in zwei Hälften aufteilen. Durch unit propagation und pure literal elimination können diese Hälften aber sehr unterschiedlich schwer zu lösende Teilinstanzen von SAT darstellen. CDCL verschärft dieses Problem durch die Anwendung weiterer Techniken. Cube-and-conquer ist ein Ansatz, der dieses Problem in zwei Phasen löst. <figure class="mw-default-size" typeof="mw:File/Thumb"><a href="/wiki/Datei:Cube_and_Conquer_example.svg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/f/f5/Cube_and_Conquer_example.svg/220px-Cube_and_Conquer_example.svg.png" decoding="async" width="220" height="111" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/f/f5/Cube_and_Conquer_example.svg/330px-Cube_and_Conquer_example.svg.png 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/f/f5/Cube_and_Conquer_example.svg/440px-Cube_and_Conquer_example.svg.png 2x" data-file-width="1496" data-file-height="753" /></a><figcaption>Cube phase der Formel F. Eine Entscheidungsheuristik wählt die Variablen aus, eine Richtungsheuristik bestimmt, welcher Wert (true oder false) als erstes bearbeitet wird und eine Cutoff-Heuristik bestimmt, ab wann die Teilprobleme klein genug sind und an den sequentiellen SAT-Solver übergeben werden.</figcaption></figure> <ol><li>Cube Phase. Die Instanz von SAT wird von einem SAT-Solver in viele (einige Tausend bis einige Millionen) Teilprobleme aufgeteilt, sogenannte Würfel. Ein Würfel ist dabei eine Konjunktion einer Teilmenge der Literale der Originalformel F.</li> <li>Konjunktiv mit F verknüpft ergibt sich eine neue Formel F', die unabhängig von den anderen Teilproblemen gelöst werden kann (z. B. CDCL). Die Disjunktion aller F' ist äquivalent zu F. Der Algorithmus terminiert also, sobald ein Teilproblem erfüllbar ist.</li></ol> Für die Cube Phase wird in der Regel ein Look-Ahead-Solver eingesetzt, da diese sich für kleine, aber schwere Probleme bewährt haben und globaler arbeiten als z. B. CDCL.<a href="#cite_note-26">[26]</a> <div class="mw-heading mw-heading3"><h3 id="Parallele_lokale_Suche">Parallele lokale Suche</h3>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=22" title="Abschnitt bearbeiten: Parallele lokale Suche" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=22" title="Quellcode des Abschnitts bearbeiten: Parallele lokale Suche">Quelltext bearbeiten</a>]</div> Parallele lokale Suche ist leicht zu parallelisieren: Flips von verschiedenen Variablen werden parallel durchgeführt oder ein Portfolio-Ansatz wird verwendet, indem unterschiedliche Strategien für die Variablenauswahl gleichzeitig angewandt werden. <div class="mw-heading mw-heading2"><h2 id="Praxis">Praxis</h2>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=23" title="Abschnitt bearbeiten: Praxis" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=23" title="Quellcode des Abschnitts bearbeiten: Praxis">Quelltext bearbeiten</a>]</div> Die SAT-Competition ist ein Wettbewerb<a href="#cite_note-27">[27]</a> für SAT-Solver, der jährlich im Rahmen der International Conference on Theory and Applications of Satisfiability Testing stattfindet.<a href="#cite_note-28">[28]</a> In verschiedenen Disziplinen werden unterschiedliche Qualitäten von SAT-Solvern evaluiert: <ul><li>Sequentielle Performance (teilweise existieren separate Wettbewerbe für bestimmte Klassen von Instanzen, z. B. Instanzen aus dem Automated Planning)</li> <li>Mäßige Parallelisierung auf einer einzelnen Maschine mit <a href="/wiki/Shared_Memory" title="Shared Memory">Shared Memory</a></li> <li>Massive Parallelisierung auf <a href="/wiki/Verteiltes_System" title="Verteiltes System">verteilten Maschinen</a></li> <li>Inkrementelle SAT-Solver, also SAT-Solving für Anwendungen, die mehrere Lösungsschritte benötigen. Dabei wird eine Sequenz verwandter SAT-Instanzen gelöst, wobei bereits gelernte Informationen aus früheren Instanzen wiederverwendet werden.<a href="#cite_note-29">[29]</a></li></ul> Die SAT-Association ist eine Vereinigung, die sich zum Ziel gesetzt hat, Forschung im Bereich SAT, SAT-Solver und der formalen Verifikation voranzubringen und die SAT-Community zu repräsentieren.<a href="#cite_note-30">[30]</a> Sie beaufsichtigt die Organisation der genannten Konferenzen und Wettbewerbe und gibt das Journal on Satisfiability, Boolean Modeling, and Computation (JSAT) heraus.<a href="#cite_note-31">[31]</a> <div class="mw-heading mw-heading2"><h2 id="Siehe_auch">Siehe auch</h2>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=24" title="Abschnitt bearbeiten: Siehe auch" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=24" title="Quellcode des Abschnitts bearbeiten: Siehe auch">Quelltext bearbeiten</a>]</div> <ul><li><a href="/wiki/Aussagenlogik" title="Aussagenlogik">Aussagenlogik</a></li> <li><a href="/wiki/Resolution_(Logik)" title="Resolution (Logik)">Resolution (Logik)</a></li> <li><a href="/wiki/Komplexit%C3%A4tstheorie" title="Komplexitätstheorie">Komplexitätstheorie</a></li> <li><a href="/wiki/NP-Vollst%C3%A4ndigkeit" title="NP-Vollständigkeit">NP-Vollständigkeit</a></li> <li><a href="/wiki/Formale_Verifikation" class="mw-redirect" title="Formale Verifikation">Formale Verifikation</a></li> <li><a href="/wiki/Erf%C3%BCllbarkeitsproblem_f%C3%BCr_Schaltkreise" title="Erfüllbarkeitsproblem für Schaltkreise">Erfüllbarkeitsproblem für Schaltkreise</a></li></ul> <div class="mw-heading mw-heading2"><h2 id="Einzelnachweise">Einzelnachweise</h2>[<a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit&section=25" title="Abschnitt bearbeiten: Einzelnachweise" class="mw-editsection-visualeditor">Bearbeiten</a> | <a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit&section=25" title="Quellcode des Abschnitts bearbeiten: Einzelnachweise">Quelltext bearbeiten</a>]</div> <ol class="references"> <li id="cite_note-1"><a href="#cite_ref-1">↑</a> <a rel="nofollow" class="external text" href="https://satcompetition.github.io/2020/downloads.html">SAT Competition 2020.</a> Abgerufen am 9. November 2020.<span style="display: none;" class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rfr_id=info%3Asid%2Fde.wikipedia.org%3AErf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.title=SAT+Competition+2020&rft.description=SAT+Competition+2020&rft.identifier=https%3A%2F%2Fsatcompetition.github.io%2F2020%2Fdownloads.html">  </li> <li id="cite_note-Verification-2">↑ <a href="#cite_ref-Verification_2-0">a</a> <a href="#cite_ref-Verification_2-1">b</a> Randal E. Bryant, Steven German, Miroslav N. Velev: <cite style="font-style:italic">Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions</cite>. In: <cite style="font-style:italic">Lecture Notes in Computer Science</cite>. Springer, Berlin / Heidelberg 1999, <a href="/wiki/Spezial:ISBN-Suche/3540660860" class="internal mw-magiclink-isbn">ISBN 3-540-66086-0</a>, S. 1–13.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=Microprocessor+Verification+Using+Efficient+Decision+Procedures+for+a+Logic+of+Equality+with+Uninterpreted+Functions&rft.au=Randal+E.+Bryant%2C+Steven+German%2C+Miroslav+N.+Velev&rft.btitle=Lecture+Notes+in+Computer+Science&rft.date=1999&rft.genre=book&rft.isbn=3540660860&rft.pages=1-13&rft.place=Berlin+%2F+Heidelberg&rft.pub=Springer" style="display:none">  </li> <li id="cite_note-10.5555/145448.146725-3">↑ <a href="#cite_ref-10.5555/145448.146725_3-0">a</a> <a href="#cite_ref-10.5555/145448.146725_3-1">b</a> Henry Kautz, Bart Selman: <cite style="font-style:italic">Planning as satisfiability</cite>. In: <cite style="font-style:italic">Proceedings of the 10th European conference on Artificial intelligence</cite> (= <cite style="font-style:italic">ECAI ’92</cite>). John Wiley & Sons, Wien 1992, <a href="/wiki/Spezial:ISBN-Suche/0471936081" class="internal mw-magiclink-isbn">ISBN 0-471-93608-1</a>, S. 359–363, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.5555/145448.146725">10.5555/145448.146725</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=Planning+as+satisfiability&rft.au=Henry+Kautz%2C+Bart+Selman&rft.btitle=Proceedings+of+the+10th+European+conference+on+Artificial+intelligence&rft.date=1992&rft.doi=10.5555%2F145448.146725&rft.genre=book&rft.isbn=0471936081&rft.pages=359-363&rft.place=Wien&rft.pub=John+Wiley+%26+Sons&rft.series=ECAI+%E2%80%9992" style="display:none">  </li> <li id="cite_note-10.1145/337292.337611-4">↑ <a href="#cite_ref-10.1145/337292.337611_4-0">a</a> <a href="#cite_ref-10.1145/337292.337611_4-1">b</a> João P. Marques-Silva, Karem A. Sakallah: <cite style="font-style:italic">Boolean satisfiability in electronic design automation</cite>. In: <cite style="font-style:italic">Proceedings of the 37th Annual Design Automation Conference</cite> (= <cite style="font-style:italic">DAC ’00</cite>). Association for Computing Machinery, Los Angeles CA 2000, <a href="/wiki/Spezial:ISBN-Suche/1581131879" class="internal mw-magiclink-isbn">ISBN 1-58113-187-9</a>, S. 675–680, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145/337292.337611">10.1145/337292.337611</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=Boolean+satisfiability+in+electronic+design+automation&rft.au=Jo%C3%A3o+P.+Marques-Silva%2C+Karem+A.+Sakallah&rft.btitle=Proceedings+of+the+37th+Annual+Design+Automation+Conference&rft.date=2000&rft.doi=10.1145%2F337292.337611&rft.genre=book&rft.isbn=1581131879&rft.pages=675-680&rft.place=Los+Angeles+CA&rft.pub=Association+for+Computing+Machinery&rft.series=DAC+%E2%80%9900" style="display:none">  </li> <li id="cite_note-10.2991/icmse-18.2018.126-5">↑ <a href="#cite_ref-10.2991/icmse-18.2018.126_5-0">a</a> <a href="#cite_ref-10.2991/icmse-18.2018.126_5-1">b</a> Hong Huang, Shaohua Zhou: <cite style="font-style:italic">An efficient SAT algorithm for complex job-shop scheduling</cite>. In: <cite style="font-style:italic">Proceedings of the 2018 8th International Conference on Manufacturing Science and Engineering (ICMSE 2018)</cite>. Atlantis Press, Paris 2018, <a href="/wiki/Spezial:ISBN-Suche/9789462525023" class="internal mw-magiclink-isbn">ISBN 978-94-6252-502-3</a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.2991/icmse-18.2018.126">10.2991/icmse-18.2018.126</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=An+efficient+SAT+algorithm+for+complex+job-shop+scheduling&rft.au=Hong+Huang%2C+Shaohua+Zhou&rft.btitle=Proceedings+of+the+2018+8th+International+Conference+on+Manufacturing+Science+and+Engineering+%28ICMSE+2018%29&rft.date=2018&rft.doi=10.2991%2Ficmse-18.2018.126&rft.genre=book&rft.isbn=9789462525023&rft.place=Paris&rft.pub=Atlantis+Press" style="display:none">  </li> <li id="cite_note-6"><a href="#cite_ref-6">↑</a> William F. Dowling, Jean H. Gallier: <cite style="font-style:italic">Linear-time algorithms for testing the satisfiability of propositional horn formulae</cite>. In: <cite style="font-style:italic">The Journal of Logic Programming</cite>. Band 1, Nr. 3, 1984, S. 267–284, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016/0743-1066%2884%2990014-1">10.1016/0743-1066(84)90014-1</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=Linear-time+algorithms+for+testing+the+satisfiability+of+propositional+horn+formulae&rft.au=William+F.+Dowling%2C+Jean+H.+Gallier&rft.date=1984&rft.doi=10.1016%2F0743-1066%2884%2990014-1&rft.genre=journal&rft.issue=3&rft.jtitle=The+Journal+of+Logic+Programming&rft.pages=267-284&rft.volume=1" style="display:none">  </li> <li id="cite_note-7"><a href="#cite_ref-7">↑</a> Bengt Aspvall, Michael F. Plass, Robert Endre Tarjan: <cite style="font-style:italic">A linear-time algorithm for testing the truth of certain quantified boolean formulas</cite>. In: <cite style="font-style:italic">Information Processing Letters</cite>. Band 8, Nr. 3, März 1979, S. 121–123, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1016/0020-0190%2879%2990002-4">10.1016/0020-0190(79)90002-4</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=A+linear-time+algorithm+for+testing+the+truth+of+certain+quantified+boolean+formulas&rft.au=Bengt+Aspvall%2C+Michael+F.+Plass%2C+Robert+Endre+Tarjan&rft.date=1979-03&rft.doi=10.1016%2F0020-0190%2879%2990002-4&rft.genre=journal&rft.issue=3&rft.jtitle=Information+Processing+Letters&rft.pages=121-123&rft.volume=8" style="display:none">  </li> <li id="cite_note-8"><a href="#cite_ref-8">↑</a> Christos Papadimitriou: <cite style="font-style:italic">Computational Complexity</cite>. Addison-Wesley, 1994.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.au=Christos+Papadimitriou&rft.btitle=Computational+Complexity&rft.date=1994&rft.genre=book&rft.pub=Addison-Wesley" style="display:none">  </li> <li id="cite_note-9"><a href="#cite_ref-9">↑</a> Pierluigi Crescenzi, Daniel Pierre Bovet: <cite style="font-style:italic">Introduction to the theory of complexity</cite>. Prentice Hall, New York 1994, <a href="/wiki/Spezial:ISBN-Suche/0139153802" class="internal mw-magiclink-isbn">ISBN 0-13-915380-2</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.au=Pierluigi+Crescenzi%2C+Daniel+Pierre+Bovet&rft.btitle=Introduction+to+the+theory+of+complexity&rft.date=1994&rft.genre=book&rft.isbn=0139153802&rft.place=New+York&rft.pub=Prentice+Hall" style="display:none">  </li> <li id="cite_note-10"><a href="#cite_ref-10">↑</a> Paturi, Pudlàk, Saks, Zane, An improved exponential-time algorithm for K-SAT, J. ACM, Band 52, 2005, S. 337–364 </li> <li id="cite_note-11"><a href="#cite_ref-11">↑</a> Dominik Schweder, John P. Steinberger, PPSZ for General k-SAT – Making Hertli’s Analysis Simpler and 3-SAT Faster, 2017, <a rel="nofollow" class="external text" href="https://drops.dagstuhl.de/opus/volltexte/2017/7535/">Online</a> </li> <li id="cite_note-12"><a href="#cite_ref-12">↑</a> Hertli: Breaking the PPSZ Barrier for Unique 3-SAT. In: Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, Elias Koutsoupias (Hrsg.): Automata, Languages, and Programming – 41st International Colloquium, ICALP 2014, Kopenhagen, Juli 2014. Teil 1: Proceedings, Part I: Lecture Notes in Computer Science 8572. Springer 2014, S. 600–611 </li> <li id="cite_note-13"><a href="#cite_ref-13">↑</a> Martin Davis, Hilary Putnam: <cite style="font-style:italic">A Computing Procedure for Quantification Theory</cite>. In: <cite style="font-style:italic">Journal of the ACM</cite>. Band 7, Nr. 3, Juli 1960, <a href="/wiki/Internationale_Standardnummer_f%C3%BCr_fortlaufende_Sammelwerke" title="Internationale Standardnummer für fortlaufende Sammelwerke">ISSN</a> <a rel="nofollow" class="external text" href="https://zdb-katalog.de/list.xhtml?t=iss%3D%220004-5411%22&key=cql">0004-5411</a>, S. 201–215, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145/321033.321034">10.1145/321033.321034</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=A+Computing+Procedure+for+Quantification+Theory&rft.au=Martin+Davis%2C+Hilary+Putnam&rft.date=1960-07&rft.doi=10.1145%2F321033.321034&rft.genre=journal&rft.issn=0004-5411&rft.issue=3&rft.jtitle=Journal+of+the+ACM&rft.pages=201-215&rft.volume=7" style="display:none">  </li> <li id="cite_note-14"><a href="#cite_ref-14">↑</a> Martin Davis, George Logemann, Donald Loveland: <cite style="font-style:italic">A machine program for theorem-proving</cite>. In: <cite style="font-style:italic">Communications of the ACM</cite>. Band 5, Nr. 7, Juli 1962, <a href="/wiki/Internationale_Standardnummer_f%C3%BCr_fortlaufende_Sammelwerke" title="Internationale Standardnummer für fortlaufende Sammelwerke">ISSN</a> <a rel="nofollow" class="external text" href="https://zdb-katalog.de/list.xhtml?t=iss%3D%220001-0782%22&key=cql">0001-0782</a>, S. 394–397, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145/368273.368557">10.1145/368273.368557</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=A+machine+program+for+theorem-proving&rft.au=Martin+Davis%2C+George+Logemann%2C+Donald+Loveland&rft.date=1962-07&rft.doi=10.1145%2F368273.368557&rft.genre=journal&rft.issn=0001-0782&rft.issue=7&rft.jtitle=Communications+of+the+ACM&rft.pages=394-397&rft.volume=5" style="display:none">  </li> <li id="cite_note-15"><a href="#cite_ref-15">↑</a> Lintao Zhang, Sharad Malik: <cite style="font-style:italic">The Quest for Efficient Boolean Satisfiability Solvers</cite>. In: <cite style="font-style:italic">Computer Aided Verification</cite>. Band 2404. Springer, Berlin / Heidelberg 2002, <a href="/wiki/Spezial:ISBN-Suche/3540439978" class="internal mw-magiclink-isbn">ISBN 3-540-43997-8</a>, S. 17–36, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007/3-540-45657-0_2">10.1007/3-540-45657-0_2</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=The+Quest+for+Efficient+Boolean+Satisfiability+Solvers&rft.au=Lintao+Zhang%2C+Sharad+Malik&rft.btitle=Computer+Aided+Verification&rft.date=2002&rft.doi=10.1007%2F3-540-45657-0_2&rft.genre=book&rft.isbn=3540439978&rft.pages=17-36&rft.place=Berlin+%2F+Heidelberg&rft.pub=Springer&rft.volume=2404" style="display:none">  </li> <li id="cite_note-16"><a href="#cite_ref-16">↑</a> João Marques-Silva: <cite style="font-style:italic">The Impact of Branching Heuristics in Propositional Satisfiability Algorithms</cite>. In: <cite style="font-style:italic">Progress in Artificial Intelligence</cite>. Band 1695. Springer, Berlin / Heidelberg 1999, <a href="/wiki/Spezial:ISBN-Suche/354066548X" class="internal mw-magiclink-isbn">ISBN 3-540-66548-X</a>, S. 62–74, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007/3-540-48159-1_5">10.1007/3-540-48159-1_5</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=The+Impact+of+Branching+Heuristics+in+Propositional+Satisfiability+Algorithms&rft.au=Jo%C3%A3o+Marques-Silva&rft.btitle=Progress+in+Artificial+Intelligence&rft.date=1999&rft.doi=10.1007%2F3-540-48159-1_5&rft.genre=book&rft.isbn=354066548X&rft.pages=62-74&rft.place=Berlin+%2F+Heidelberg&rft.pub=Springer&rft.volume=1695" style="display:none">  </li> <li id="cite_note-17"><a href="#cite_ref-17">↑</a> Emina Torlak: <a rel="nofollow" class="external text" href="https://courses.cs.washington.edu/courses/cse507/17wi/lectures/L02.pdf">A Modern SAT Solver Lecture, University of Washington.</a> (PDF) Abgerufen am 8. November 2020 (englisch).<span style="display: none;" class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rfr_id=info%3Asid%2Fde.wikipedia.org%3AErf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.title=A+Modern+SAT+Solver+Lecture%2C+University+of+Washington&rft.description=A+Modern+SAT+Solver+Lecture%2C+University+of+Washington&rft.identifier=https%3A%2F%2Fcourses.cs.washington.edu%2Fcourses%2Fcse507%2F17wi%2Flectures%2FL02.pdf&rft.creator=Emina+Torlak&rft.language=en">  </li> <li id="cite_note-18"><a href="#cite_ref-18">↑</a> Roberto J. Bayardo, Robert Schrag: <cite style="font-style:italic">Using CSP look-back techniques to solve exceptionally hard SAT instances</cite>. In: <cite style="font-style:italic">Lecture Notes in Computer Science</cite>. Springer, Berlin / Heidelberg 1996, <a href="/wiki/Spezial:ISBN-Suche/3540615512" class="internal mw-magiclink-isbn">ISBN 3-540-61551-2</a>, S. 46–60.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=Using+CSP+look-back+techniques+to+solve+exceptionally+hard+SAT+instances&rft.au=Roberto+J.+Bayardo%2C+Robert+Schrag&rft.btitle=Lecture+Notes+in+Computer+Science&rft.date=1996&rft.genre=book&rft.isbn=3540615512&rft.pages=46-60&rft.place=Berlin+%2F+Heidelberg&rft.pub=Springer" style="display:none">  </li> <li id="cite_note-19"><a href="#cite_ref-19">↑</a> Lintao Zhang, S. Malik: <cite style="font-style:italic">Conflict driven learning in a quantified Boolean satisfiability solver</cite>. In: <cite style="font-style:italic">IEEE/ACM International Conference on Computer Aided Design</cite>. IEEE, 2002, <a href="/wiki/Spezial:ISBN-Suche/0780376072" class="internal mw-magiclink-isbn">ISBN 0-7803-7607-2</a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109/iccad.2002.1167570">10.1109/iccad.2002.1167570</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=Conflict+driven+learning+in+a+quantified+Boolean+satisfiability+solver&rft.au=Lintao+Zhang%2C+S.+Malik&rft.btitle=IEEE%2FACM+International+Conference+on+Computer+Aided+Design&rft.date=2002&rft.doi=10.1109%2Ficcad.2002.1167570&rft.genre=book&rft.isbn=0780376072&rft.pub=IEEE" style="display:none">  </li> <li id="cite_note-20"><a href="#cite_ref-20">↑</a> J.P. Marques-Silva, K.A. Sakallah: <cite style="font-style:italic">GRASP: a search algorithm for propositional satisfiability</cite>. In: <cite style="font-style:italic">IEEE Transactions on Computers</cite>. Band 48, Nr. 5, Mai 1999, S. 506–521, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109/12.769433">10.1109/12.769433</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=GRASP%3A+a+search+algorithm+for+propositional+satisfiability&rft.au=J.P.+Marques-Silva%2C+K.A.+Sakallah&rft.date=1999-05&rft.doi=10.1109%2F12.769433&rft.genre=journal&rft.issue=5&rft.jtitle=IEEE+Transactions+on+Computers&rft.pages=506-521&rft.volume=48" style="display:none">  </li> <li id="cite_note-21"><a href="#cite_ref-21">↑</a> Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich: <cite style="font-style:italic">A verified SAT solver with watched literals using imperative HOL</cite>. In: <cite style="font-style:italic">Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs – CPP 2018</cite>. ACM Press, New York NY 2018, <a href="/wiki/Spezial:ISBN-Suche/9781450355865" class="internal mw-magiclink-isbn">ISBN 978-1-4503-5586-5</a>, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145/3167080">10.1145/3167080</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=A+verified+SAT+solver+with+watched+literals+using+imperative+HOL&rft.au=Mathias+Fleury%2C+Jasmin+Christian+Blanchette%2C+Peter+Lammich&rft.btitle=Proceedings+of+the+7th+ACM+SIGPLAN+International+Conference+on+Certified+Programs+and+Proofs+-+CPP+2018&rft.date=2018&rft.doi=10.1145%2F3167080&rft.genre=book&rft.isbn=9781450355865&rft.place=New+York+NY&rft.pub=ACM+Press" style="display:none">  </li> <li id="cite_note-22"><a href="#cite_ref-22">↑</a> Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik: <cite style="font-style:italic">Chaff: engineering an efficient SAT solver</cite>. In: <cite style="font-style:italic">Proceedings of the 38th conference on Design automation – DAC ’01</cite>. ACM Press, Las Vegas NV 2001, <a href="/wiki/Spezial:ISBN-Suche/1581132972" class="internal mw-magiclink-isbn">ISBN 1-58113-297-2</a>, S. 530–535, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1145/378239.379017">10.1145/378239.379017</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=Chaff%3A+engineering+an+efficient+SAT+solver&rft.au=Matthew+W.+Moskewicz%2C+Conor+F.+Madigan%2C+Ying+Zhao%2C+...&rft.btitle=Proceedings+of+the+38th+conference+on+Design+automation+-+DAC+%E2%80%9901&rft.date=2001&rft.doi=10.1145%2F378239.379017&rft.genre=book&rft.isbn=1581132972&rft.pages=530-535&rft.place=Las+Vegas+NV&rft.pub=ACM+Press" style="display:none">  </li> <li id="cite_note-23"><a href="#cite_ref-23">↑</a> Gilles Audemard, Laurent Simon: <cite style="font-style:italic">Predicting Learnt Clauses Quality in Modern SAT Solvers</cite>. In: <cite style="font-style:italic">Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI)</cite>. 2009.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=Predicting+Learnt+Clauses+Quality+in+Modern+SAT+Solvers&rft.au=Gilles+Audemard%2C+Laurent+Simon&rft.btitle=Proceedings+of+the+21st+International+Joint+Conference+on+Artificial+Intelligence+%28IJCAI%29&rft.date=2009&rft.genre=book" style="display:none">  </li> <li id="cite_note-24"><a href="#cite_ref-24">↑</a> B. Selman, H. J. Levesque, D. G. Mitchell: <cite style="font-style:italic">A new method for solving hard satisfiability problems</cite>. 10th AAAI. San Jose CA 1992, S. 440–446.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.au=B.+Selman%2C+H.+J.+Levesque%2C+D.+G.+Mitchell&rft.btitle=A+new+method+for+solving+hard+satisfiability+problems&rft.date=1992&rft.genre=book&rft.pages=440-446&rft.place=San+Jose+CA&rft.volume=10th+AAAI" style="display:none">  </li> <li id="cite_note-25"><a href="#cite_ref-25">↑</a> K Keefe: <cite style="font-style:italic">Local search strategies for equational satisfiability.</cite> Office of Scientific and Technical Information (OSTI), 21. September 2004.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.au=K+Keefe&rft.btitle=Local+search+strategies+for+equational+satisfiability.&rft.date=2004-09-21&rft.genre=book&rft.pub=Office+of+Scientific+and+Technical+Information++%28OSTI%29" style="display:none">  </li> <li id="cite_note-26"><a href="#cite_ref-26">↑</a> Marijn J.H. Heule and Hans van Maaren: <cite style="font-style:italic">Look-Ahead Based SAT Solvers, Handbook of Satisfiability</cite>. Hrsg.: IOS Press. EasyChair, 2009, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.29007/g7ss">10.29007/g7ss</a> (<a rel="nofollow" class="external text" href="https://www.cs.utexas.edu/~marijn/publications/p01c05_lah.pdf">utexas.edu</a> [PDF; abgerufen am 8. November 2020]).<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.au=Marijn+J.H.+Heule+and+Hans+van+Maaren&rft.btitle=Look-Ahead+Based+SAT+Solvers%2C+Handbook+of+Satisfiability&rft.date=2009&rft.doi=10.29007%2Fg7ss&rft.genre=book&rft.pub=EasyChair" style="display:none">  </li> <li id="cite_note-27"><a href="#cite_ref-27">↑</a> <a rel="nofollow" class="external text" href="http://www.satcompetition.org/">The International SAT Competition Web Page</a> </li> <li id="cite_note-28"><a href="#cite_ref-28">↑</a> <a rel="nofollow" class="external text" href="http://satisfiability.org/">The International Conferences on Theory and Applications of Satisfiability Testing (SAT)</a> </li> <li id="cite_note-29"><a href="#cite_ref-29">↑</a> Katalin Fazekas, Armin Biere, Christoph Scholl: <cite style="font-style:italic">Incremental Inprocessing in SAT Solving</cite>. In: <cite style="font-style:italic">Theory and Applications of Satisfiability Testing – SAT 2019</cite> (= <cite style="font-style:italic">Lecture Notes in Computer Science</cite>). Springer International Publishing, Cham 2019, <a href="/wiki/Spezial:ISBN-Suche/9783030242589" class="internal mw-magiclink-isbn">ISBN 978-3-03024258-9</a>, S. 136–154, <a href="/wiki/Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007/978-3-030-24258-9_9">10.1007/978-3-030-24258-9_9</a>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik&rft.atitle=Incremental+Inprocessing+in+SAT+Solving&rft.au=Katalin+Fazekas%2C+Armin+Biere%2C+Christoph+Scholl&rft.btitle=Theory+and+Applications+of+Satisfiability+Testing+-+SAT+2019&rft.date=2019&rft.doi=10.1007%2F978-3-030-24258-9_9&rft.genre=book&rft.isbn=9783030242589&rft.pages=136-154&rft.place=Cham&rft.pub=Springer+International+Publishing&rft.series=Lecture+Notes+in+Computer+Science" style="display:none">  </li> <li id="cite_note-30"><a href="#cite_ref-30">↑</a> <a rel="nofollow" class="external text" href="http://satassociation.org/">The SAT Association</a> </li> <li id="cite_note-31"><a href="#cite_ref-31">↑</a> Journal on Satisfiability, Boolean Modeling and Computation <a href="/wiki/Internationale_Standardnummer_f%C3%BCr_fortlaufende_Sammelwerke" title="Internationale Standardnummer für fortlaufende Sammelwerke">ISSN</a> <a rel="nofollow" class="external text" href="https://zdb-katalog.de/list.xhtml?t=iss%3D%221574-0617%22&key=cql">1574-0617</a> </li> </ol> <style data-mw-deduplicate="TemplateStyles:r248673343">.mw-parser-output div.NavFrame{border-width:1px;border-style:solid;border-left-color:var(--dewiki-rahmenfarbe1);border-right-color:var(--dewiki-rahmenfarbe1);border-top-color:var(--dewiki-rahmenfarbe1);border-bottom-color:var(--dewiki-rahmenfarbe1);clear:both;font-size:95%;margin-top:1.5em;min-height:0;padding:2px;text-align:center}.mw-parser-output div.NavPic{float:left;padding:2px}.mw-parser-output div.NavHead{background-color:var(--dewiki-hintergrundfarbe5);font-weight:bold}.mw-parser-output div.NavFrame:after{clear:both;content:"";display:block}.mw-parser-output div.NavFrame+div.NavFrame,.mw-parser-output div.NavFrame+link+div.NavFrame,.mw-parser-output div.NavFrame+style+div.NavFrame{margin-top:-1px}.mw-parser-output .NavToggle{float:right;font-size:x-small}@media screen{html.skin-theme-clientpref-night .mw-parser-output .NavPic span[typeof="mw:File"] img{background-color:#c8ccd1}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .NavPic span[typeof="mw:File"] img{background-color:#c8ccd1}}</style><div class="NavFrame navigation-not-searchable" role="navigation"> <div class="NavHead"><a href="/wiki/Karps_21_NP-vollst%C3%A4ndige_Probleme" title="Karps 21 NP-vollständige Probleme">Karps 21 NP-vollständige Probleme</a></div> <div class="NavContent"> <a class="mw-selflink selflink">Erfüllbarkeitsproblem der Aussagenlogik</a> | <a href="/wiki/Cliquenproblem" title="Cliquenproblem">Cliquenproblem</a> | <a href="/wiki/Mengenpackungsproblem" title="Mengenpackungsproblem">Mengenpackungsproblem</a> | <a href="/wiki/Knoten%C3%BCberdeckungsproblem" class="mw-redirect" title="Knotenüberdeckungsproblem">Knotenüberdeckungsproblem</a> | <a href="/wiki/Mengen%C3%BCberdeckungsproblem" title="Mengenüberdeckungsproblem">Mengenüberdeckungsproblem</a> | <a href="/wiki/Feedback_Arc_Set" title="Feedback Arc Set">Feedback Arc Set</a> | <a href="/wiki/Feedback_Vertex_Set" title="Feedback Vertex Set">Feedback Vertex Set</a> | <a href="/wiki/Hamiltonkreisproblem" title="Hamiltonkreisproblem">Hamiltonkreisproblem</a> | <a href="/wiki/Ganzzahlige_lineare_Optimierung#0.2F1-Programmierung" title="Ganzzahlige lineare Optimierung">Integer Linear Programming</a> | <a href="/wiki/3-SAT" title="3-SAT">3-SAT</a> | <a href="/wiki/F%C3%A4rbung_(Graphentheorie)" title="Färbung (Graphentheorie)">graph coloring problem</a> | <a href="/w/index.php?title=Covering_by_cliques&action=edit&redlink=1" class="new" title="Covering by cliques (Seite nicht vorhanden)">Covering by cliques</a> | <a href="/wiki/Problem_der_exakten_%C3%9Cberdeckung" title="Problem der exakten Überdeckung">Problem der exakten Überdeckung</a> | <a href="/w/index.php?title=3-dimensional_matching&action=edit&redlink=1" class="new" title="3-dimensional matching (Seite nicht vorhanden)">3-dimensional matching</a> | <a href="/wiki/Steinerbaumproblem" title="Steinerbaumproblem">Steinerbaumproblem</a> | <a href="/wiki/Hitting-Set-Problem" title="Hitting-Set-Problem">Hitting set</a> | <a href="/wiki/Rucksackproblem" title="Rucksackproblem">Rucksackproblem</a> | <a href="/w/index.php?title=Job_sequencing&action=edit&redlink=1" class="new" title="Job sequencing (Seite nicht vorhanden)">Job sequencing</a> | <a href="/wiki/Partitionsproblem" title="Partitionsproblem">Partitionsproblem</a> | <a href="/wiki/Maximaler_Schnitt" title="Maximaler Schnitt">Maximaler Schnitt</a> </div> </div></div><noscript><img src="https://login.wikimedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" width="1" height="1" style="border: none; position: absolute;"></noscript> <div class="printfooter" data-nosnippet="">Abgerufen von „<a dir="ltr" href="https://de.wikipedia.org/w/index.php?title=Erfüllbarkeitsproblem_der_Aussagenlogik&oldid=248841235">https://de.wikipedia.org/w/index.php?title=Erfüllbarkeitsproblem_der_Aussagenlogik&oldid=248841235</a>“</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Wikipedia:Kategorien" title="Wikipedia:Kategorien">Kategorien</a>: <ul><li><a href="/wiki/Kategorie:Komplexit%C3%A4tstheorie" title="Kategorie:Komplexitätstheorie">Komplexitätstheorie</a></li><li><a href="/wiki/Kategorie:Mathematische_Logik" title="Kategorie:Mathematische Logik">Mathematische Logik</a></li><li><a href="/wiki/Kategorie:Aussagenlogik" title="Kategorie:Aussagenlogik">Aussagenlogik</a></li></ul></div></div> </div> </div> <div id="mw-navigation"> <h2>Navigationsmenü</h2> <div id="mw-head"> <nav id="p-personal" class="mw-portlet mw-portlet-personal vector-user-menu-legacy vector-menu" aria-labelledby="p-personal-label" > <h3 id="p-personal-label" class="vector-menu-heading " > Meine Werkzeuge </h3> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-anonuserpage" class="mw-list-item">Nicht angemeldet</li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Spezial:Meine_Diskussionsseite" title="Diskussion über Änderungen von dieser IP-Adresse [n]" accesskey="n">Diskussionsseite</a></li><li id="pt-anoncontribs" class="mw-list-item"><a href="/wiki/Spezial:Meine_Beitr%C3%A4ge" title="Eine Liste der Bearbeitungen, die von dieser IP-Adresse gemacht wurden [y]" accesskey="y">Beiträge</a></li><li id="pt-createaccount" class="mw-list-item"><a href="/w/index.php?title=Spezial:Benutzerkonto_anlegen&returnto=Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik" title="Wir ermutigen dich dazu, ein Benutzerkonto zu erstellen und dich anzumelden. Es ist jedoch nicht zwingend erforderlich.">Benutzerkonto erstellen</a></li><li id="pt-login" class="mw-list-item"><a href="/w/index.php?title=Spezial:Anmelden&returnto=Erf%C3%BCllbarkeitsproblem+der+Aussagenlogik" title="Anmelden ist zwar keine Pflicht, wird aber gerne gesehen. [o]" accesskey="o">Anmelden</a></li> </ul> </div> </nav> <div id="left-navigation"> <nav id="p-namespaces" class="mw-portlet mw-portlet-namespaces vector-menu-tabs vector-menu-tabs-legacy vector-menu" aria-labelledby="p-namespaces-label" > <h3 id="p-namespaces-label" class="vector-menu-heading " > Namensräume </h3> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-nstab-main" class="selected mw-list-item"><a href="/wiki/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik" title="Seiteninhalt anzeigen [c]" accesskey="c">Artikel</a></li><li id="ca-talk" class="mw-list-item"><a href="/wiki/Diskussion:Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik" rel="discussion" title="Diskussion zum Seiteninhalt [t]" accesskey="t">Diskussion</a></li> </ul> </div> </nav> <nav id="p-variants" class="mw-portlet mw-portlet-variants emptyPortlet vector-menu-dropdown vector-menu" aria-labelledby="p-variants-label" > <input type="checkbox" id="p-variants-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-variants" class="vector-menu-checkbox" aria-labelledby="p-variants-label" > <label id="p-variants-label" class="vector-menu-heading " > Deutsch </label> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </nav> </div> <div id="right-navigation"> <nav id="p-views" class="mw-portlet mw-portlet-views vector-menu-tabs vector-menu-tabs-legacy vector-menu" aria-labelledby="p-views-label" > <h3 id="p-views-label" class="vector-menu-heading " > Ansichten </h3> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-view" class="selected mw-list-item"><a href="/wiki/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik">Lesen</a></li><li id="ca-ve-edit" class="mw-list-item"><a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&veaction=edit" title="Diese Seite mit dem VisualEditor bearbeiten [v]" accesskey="v">Bearbeiten</a></li><li id="ca-edit" class="collapsible mw-list-item"><a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=edit" title="Den Quelltext dieser Seite bearbeiten [e]" accesskey="e">Quelltext bearbeiten</a></li><li id="ca-history" class="mw-list-item"><a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=history" title="Frühere Versionen dieser Seite [h]" accesskey="h">Versionsgeschichte</a></li> </ul> </div> </nav> <nav id="p-cactions" class="mw-portlet mw-portlet-cactions emptyPortlet vector-menu-dropdown vector-menu" aria-labelledby="p-cactions-label" title="Weitere Optionen" > <input type="checkbox" id="p-cactions-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-cactions" class="vector-menu-checkbox" aria-labelledby="p-cactions-label" > <label id="p-cactions-label" class="vector-menu-heading " > Weitere </label> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </nav> <div id="p-search" role="search" class="vector-search-box-vue vector-search-box-show-thumbnail vector-search-box-auto-expand-width vector-search-box"> <h3 >Suche</h3> <form action="/w/index.php" id="searchform" class="vector-search-box-form"> <div id="simpleSearch" class="vector-search-box-inner" data-search-loc="header-navigation"> <input class="vector-search-box-input" type="search" name="search" placeholder="Wikipedia durchsuchen" aria-label="Wikipedia durchsuchen" autocapitalize="sentences" title="Durchsuche die Wikipedia [f]" accesskey="f" id="searchInput" > <input type="hidden" name="title" value="Spezial:Suche"> <input id="mw-searchButton" class="searchButton mw-fallbackSearchButton" type="submit" name="fulltext" title="Suche nach Seiten, die diesen Text enthalten" value="Suchen"> <input id="searchButton" class="searchButton" type="submit" name="go" title="Gehe direkt zu der Seite mit genau diesem Namen, falls sie vorhanden ist." value="Artikel"> </div> </form> </div> </div> </div> <div id="mw-panel" class="vector-legacy-sidebar"> <div id="p-logo" role="banner"> <a class="mw-wiki-logo" href="/wiki/Wikipedia:Hauptseite" title="Hauptseite"></a> </div> <nav id="p-navigation" class="mw-portlet mw-portlet-navigation vector-menu-portal portal vector-menu" aria-labelledby="p-navigation-label" > <h3 id="p-navigation-label" class="vector-menu-heading " > Navigation </h3> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-mainpage-description" class="mw-list-item"><a href="/wiki/Wikipedia:Hauptseite" title="Hauptseite besuchen [z]" accesskey="z">Hauptseite</a></li><li id="n-topics" class="mw-list-item"><a href="/wiki/Portal:Wikipedia_nach_Themen">Themenportale</a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Spezial:Zuf%C3%A4llige_Seite" title="Zufällige Seite aufrufen [x]" accesskey="x">Zufälliger Artikel</a></li> </ul> </div> </nav> <nav id="p-Mitmachen" class="mw-portlet mw-portlet-Mitmachen vector-menu-portal portal vector-menu" aria-labelledby="p-Mitmachen-label" > <h3 id="p-Mitmachen-label" class="vector-menu-heading " > Mitmachen </h3> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-Artikel-verbessern" class="mw-list-item"><a href="/wiki/Wikipedia:Beteiligen">Artikel verbessern</a></li><li id="n-Neuerartikel" class="mw-list-item"><a href="/wiki/Hilfe:Neuen_Artikel_anlegen">Neuen Artikel anlegen</a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikipedia:Autorenportal" title="Info-Zentrum über Beteiligungsmöglichkeiten">Autorenportal</a></li><li id="n-help" class="mw-list-item"><a href="/wiki/Hilfe:%C3%9Cbersicht" title="Übersicht über Hilfeseiten">Hilfe</a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Spezial:Letzte_%C3%84nderungen" title="Liste der letzten Änderungen in Wikipedia [r]" accesskey="r">Letzte Änderungen</a></li><li id="n-contact" class="mw-list-item"><a href="/wiki/Wikipedia:Kontakt" title="Kontaktmöglichkeiten">Kontakt</a></li><li id="n-sitesupport" class="mw-list-item"><a href="//donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_de.wikipedia.org&uselang=de" title="Unterstütze uns">Spenden</a></li> </ul> </div> </nav> <nav id="p-tb" class="mw-portlet mw-portlet-tb vector-menu-portal portal vector-menu" aria-labelledby="p-tb-label" > <h3 id="p-tb-label" class="vector-menu-heading " > Werkzeuge </h3> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Spezial:Linkliste/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik" title="Liste aller Seiten, die hierher verlinken [j]" accesskey="j">Links auf diese Seite</a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Spezial:%C3%84nderungen_an_verlinkten_Seiten/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik" rel="nofollow" title="Letzte Änderungen an Seiten, die von hier verlinkt sind [k]" accesskey="k">Änderungen an verlinkten Seiten</a></li><li id="t-specialpages" class="mw-list-item"><a href="/wiki/Spezial:Spezialseiten" title="Liste aller Spezialseiten [q]" accesskey="q">Spezialseiten</a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&oldid=248841235" title="Dauerhafter Link zu dieser Seitenversion">Permanenter Link</a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=info" title="Weitere Informationen über diese Seite">Seiteninformationen</a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Spezial:Zitierhilfe&page=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&id=248841235&wpFormIdentifier=titleform" title="Hinweise, wie diese Seite zitiert werden kann">Artikel zitieren</a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Spezial:URL-K%C3%BCrzung&url=https%3A%2F%2Fde.wikipedia.org%2Fwiki%2FErf%25C3%25BCllbarkeitsproblem_der_Aussagenlogik">Kurzlink</a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Spezial:QrCode&url=https%3A%2F%2Fde.wikipedia.org%2Fwiki%2FErf%25C3%25BCllbarkeitsproblem_der_Aussagenlogik">QR-Code herunterladen</a></li> </ul> </div> </nav> <nav id="p-coll-print_export" class="mw-portlet mw-portlet-coll-print_export vector-menu-portal portal vector-menu" aria-labelledby="p-coll-print_export-label" > <h3 id="p-coll-print_export-label" class="vector-menu-heading " > Drucken/exportieren </h3> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Spezial:DownloadAsPdf&page=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&action=show-download-screen">Als PDF herunterladen</a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&printable=yes" title="Druckansicht dieser Seite [p]" accesskey="p">Druckversion</a></li> </ul> </div> </nav> <nav id="p-wikibase-otherprojects" class="mw-portlet mw-portlet-wikibase-otherprojects vector-menu-portal portal vector-menu" aria-labelledby="p-wikibase-otherprojects-label" > <h3 id="p-wikibase-otherprojects-label" class="vector-menu-heading " > In anderen Projekten </h3> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li class="wb-otherproject-link wb-otherproject-commons mw-list-item"><a href="https://commons.wikimedia.org/wiki/Category:Boolean_satisfiability_problem" hreflang="en">Commons</a></li><li id="t-wikibase" class="wb-otherproject-link wb-otherproject-wikibase-dataitem mw-list-item"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q875276" title="Link zum verbundenen Objekt im Datenrepositorium [g]" accesskey="g">Wikidata-Datenobjekt</a></li> </ul> </div> </nav> <nav id="p-lang" class="mw-portlet mw-portlet-lang vector-menu-portal portal vector-menu" aria-labelledby="p-lang-label" > <h3 id="p-lang-label" class="vector-menu-heading " > In anderen Sprachen </h3> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li class="interlanguage-link interwiki-ar mw-list-item"><a href="https://ar.wikipedia.org/wiki/%D9%85%D8%B3%D8%A3%D9%84%D8%A9_%D9%82%D8%A7%D8%A8%D9%84%D9%8A%D8%A9_%D8%A7%D9%84%D8%A5%D8%B1%D8%B6%D8%A7%D8%A1_%D8%A7%D9%84%D9%85%D9%86%D8%B7%D9%82%D9%8A%D8%A9" title="مسألة قابلية الإرضاء المنطقية – Arabisch" lang="ar" hreflang="ar" data-title="مسألة قابلية الإرضاء المنطقية" data-language-autonym="العربية" data-language-local-name="Arabisch" class="interlanguage-link-target">العربية</a></li><li class="interlanguage-link interwiki-ca mw-list-item"><a href="https://ca.wikipedia.org/wiki/Problema_de_satisfacibilitat_booleana" title="Problema de satisfacibilitat booleana – Katalanisch" lang="ca" hreflang="ca" data-title="Problema de satisfacibilitat booleana" data-language-autonym="Català" data-language-local-name="Katalanisch" class="interlanguage-link-target">Català</a></li><li class="interlanguage-link interwiki-cs mw-list-item"><a href="https://cs.wikipedia.org/wiki/Probl%C3%A9m_splnitelnosti_booleovsk%C3%A9_formule" title="Problém splnitelnosti booleovské formule – Tschechisch" lang="cs" hreflang="cs" data-title="Problém splnitelnosti booleovské formule" data-language-autonym="Čeština" data-language-local-name="Tschechisch" class="interlanguage-link-target">Čeština</a></li><li class="interlanguage-link interwiki-en mw-list-item"><a href="https://en.wikipedia.org/wiki/Boolean_satisfiability_problem" title="Boolean satisfiability problem – Englisch" lang="en" hreflang="en" data-title="Boolean satisfiability problem" data-language-autonym="English" data-language-local-name="Englisch" class="interlanguage-link-target">English</a></li><li class="interlanguage-link interwiki-eo mw-list-item"><a href="https://eo.wikipedia.org/wiki/Bulea_plenumebloproblemo" title="Bulea plenumebloproblemo – Esperanto" lang="eo" hreflang="eo" data-title="Bulea plenumebloproblemo" data-language-autonym="Esperanto" data-language-local-name="Esperanto" class="interlanguage-link-target">Esperanto</a></li><li class="interlanguage-link interwiki-es mw-list-item"><a href="https://es.wikipedia.org/wiki/Problema_de_satisfacibilidad_booleana" title="Problema de satisfacibilidad booleana – Spanisch" lang="es" hreflang="es" data-title="Problema de satisfacibilidad booleana" data-language-autonym="Español" data-language-local-name="Spanisch" class="interlanguage-link-target">Español</a></li><li class="interlanguage-link interwiki-fa mw-list-item"><a href="https://fa.wikipedia.org/wiki/%D9%85%D8%B3%D8%A6%D9%84%D9%87_%D8%B5%D8%AF%D9%82%E2%80%8C%D9%BE%D8%B0%DB%8C%D8%B1%DB%8C_%D8%A8%D9%88%D9%84%DB%8C" title="مسئله صدق‌پذیری بولی – Persisch" lang="fa" hreflang="fa" data-title="مسئله صدق‌پذیری بولی" data-language-autonym="فارسی" data-language-local-name="Persisch" class="interlanguage-link-target">فارسی</a></li><li class="interlanguage-link interwiki-fi mw-list-item"><a href="https://fi.wikipedia.org/wiki/Lauselogiikan_toteutuvuusongelma" title="Lauselogiikan toteutuvuusongelma – Finnisch" lang="fi" hreflang="fi" data-title="Lauselogiikan toteutuvuusongelma" data-language-autonym="Suomi" data-language-local-name="Finnisch" class="interlanguage-link-target">Suomi</a></li><li class="interlanguage-link interwiki-fr mw-list-item"><a href="https://fr.wikipedia.org/wiki/Probl%C3%A8me_SAT" title="Problème SAT – Französisch" lang="fr" hreflang="fr" data-title="Problème SAT" data-language-autonym="Français" data-language-local-name="Französisch" class="interlanguage-link-target">Français</a></li><li class="interlanguage-link interwiki-he mw-list-item"><a href="https://he.wikipedia.org/wiki/%D7%91%D7%A2%D7%99%D7%99%D7%AA_%D7%94%D7%A1%D7%A4%D7%99%D7%A7%D7%95%D7%AA" title="בעיית הספיקות – Hebräisch" lang="he" hreflang="he" data-title="בעיית הספיקות" data-language-autonym="עברית" data-language-local-name="Hebräisch" class="interlanguage-link-target">עברית</a></li><li class="interlanguage-link interwiki-hu mw-list-item"><a href="https://hu.wikipedia.org/wiki/Logikai_kiel%C3%A9g%C3%ADt%C3%A9si_probl%C3%A9ma" title="Logikai kielégítési probléma – Ungarisch" lang="hu" hreflang="hu" data-title="Logikai kielégítési probléma" data-language-autonym="Magyar" data-language-local-name="Ungarisch" class="interlanguage-link-target">Magyar</a></li><li class="interlanguage-link interwiki-it mw-list-item"><a href="https://it.wikipedia.org/wiki/Soddisfacibilit%C3%A0_booleana" title="Soddisfacibilità booleana – Italienisch" lang="it" hreflang="it" data-title="Soddisfacibilità booleana" data-language-autonym="Italiano" data-language-local-name="Italienisch" class="interlanguage-link-target">Italiano</a></li><li class="interlanguage-link interwiki-ja mw-list-item"><a href="https://ja.wikipedia.org/wiki/%E5%85%85%E8%B6%B3%E5%8F%AF%E8%83%BD%E6%80%A7%E5%95%8F%E9%A1%8C" title="充足可能性問題 – Japanisch" lang="ja" hreflang="ja" data-title="充足可能性問題" data-language-autonym="日本語" data-language-local-name="Japanisch" class="interlanguage-link-target">日本語</a></li><li class="interlanguage-link interwiki-ko mw-list-item"><a href="https://ko.wikipedia.org/wiki/%EC%B6%A9%EC%A1%B1_%EA%B0%80%EB%8A%A5%EC%84%B1_%EB%AC%B8%EC%A0%9C" title="충족 가능성 문제 – Koreanisch" lang="ko" hreflang="ko" data-title="충족 가능성 문제" data-language-autonym="한국어" data-language-local-name="Koreanisch" class="interlanguage-link-target">한국어</a></li><li class="interlanguage-link interwiki-nl mw-list-item"><a href="https://nl.wikipedia.org/wiki/Vervulbaarheidsprobleem" title="Vervulbaarheidsprobleem – Niederländisch" lang="nl" hreflang="nl" data-title="Vervulbaarheidsprobleem" data-language-autonym="Nederlands" data-language-local-name="Niederländisch" class="interlanguage-link-target">Nederlands</a></li><li class="interlanguage-link interwiki-pl mw-list-item"><a href="https://pl.wikipedia.org/wiki/Problem_spe%C5%82nialno%C5%9Bci" title="Problem spełnialności – Polnisch" lang="pl" hreflang="pl" data-title="Problem spełnialności" data-language-autonym="Polski" data-language-local-name="Polnisch" class="interlanguage-link-target">Polski</a></li><li class="interlanguage-link interwiki-pt mw-list-item"><a href="https://pt.wikipedia.org/wiki/Problema_de_satisfatibilidade_booliana" title="Problema de satisfatibilidade booliana – Portugiesisch" lang="pt" hreflang="pt" data-title="Problema de satisfatibilidade booliana" data-language-autonym="Português" data-language-local-name="Portugiesisch" class="interlanguage-link-target">Português</a></li><li class="interlanguage-link interwiki-ru mw-list-item"><a href="https://ru.wikipedia.org/wiki/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_%D0%B2%D1%8B%D0%BF%D0%BE%D0%BB%D0%BD%D0%B8%D0%BC%D0%BE%D1%81%D1%82%D0%B8_%D0%B1%D1%83%D0%BB%D0%B5%D0%B2%D1%8B%D1%85_%D1%84%D0%BE%D1%80%D0%BC%D1%83%D0%BB" title="Задача выполнимости булевых формул – Russisch" lang="ru" hreflang="ru" data-title="Задача выполнимости булевых формул" data-language-autonym="Русский" data-language-local-name="Russisch" class="interlanguage-link-target">Русский</a></li><li class="interlanguage-link interwiki-sh mw-list-item"><a href="https://sh.wikipedia.org/wiki/SAT_problem" title="SAT problem – Serbokroatisch" lang="sh" hreflang="sh" data-title="SAT problem" data-language-autonym="Srpskohrvatski / српскохрватски" data-language-local-name="Serbokroatisch" class="interlanguage-link-target">Srpskohrvatski / српскохрватски</a></li><li class="interlanguage-link interwiki-simple mw-list-item"><a href="https://simple.wikipedia.org/wiki/Boolean_satisfiability_problem" title="Boolean satisfiability problem – einfaches Englisch" lang="en-simple" hreflang="en-simple" data-title="Boolean satisfiability problem" data-language-autonym="Simple English" data-language-local-name="einfaches Englisch" class="interlanguage-link-target">Simple English</a></li><li class="interlanguage-link interwiki-sr mw-list-item"><a href="https://sr.wikipedia.org/wiki/%D0%A1%D0%90%D0%A2_%D0%BF%D1%80%D0%BE%D0%B1%D0%BB%D0%B5%D0%BC" title="САТ проблем – Serbisch" lang="sr" hreflang="sr" data-title="САТ проблем" data-language-autonym="Српски / srpski" data-language-local-name="Serbisch" class="interlanguage-link-target">Српски / srpski</a></li><li class="interlanguage-link interwiki-th mw-list-item"><a href="https://th.wikipedia.org/wiki/%E0%B8%9B%E0%B8%B1%E0%B8%8D%E0%B8%AB%E0%B8%B2%E0%B8%84%E0%B8%A7%E0%B8%B2%E0%B8%A1%E0%B8%AA%E0%B8%AD%E0%B8%94%E0%B8%84%E0%B8%A5%E0%B9%89%E0%B8%AD%E0%B8%87%E0%B9%81%E0%B8%9A%E0%B8%9A%E0%B8%9A%E0%B8%B9%E0%B8%A5" title="ปัญหาความสอดคล้องแบบบูล – Thailändisch" lang="th" hreflang="th" data-title="ปัญหาความสอดคล้องแบบบูล" data-language-autonym="ไทย" data-language-local-name="Thailändisch" class="interlanguage-link-target">ไทย</a></li><li class="interlanguage-link interwiki-uk mw-list-item"><a href="https://uk.wikipedia.org/wiki/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_%D0%B7%D0%B4%D1%96%D0%B9%D1%81%D0%BD%D0%B5%D0%BD%D0%BD%D0%BE%D1%81%D1%82%D1%96_%D0%B1%D1%83%D0%BB%D0%B5%D0%B2%D0%B8%D1%85_%D1%84%D0%BE%D1%80%D0%BC%D1%83%D0%BB" title="Задача здійсненності булевих формул – Ukrainisch" lang="uk" hreflang="uk" data-title="Задача здійсненності булевих формул" data-language-autonym="Українська" data-language-local-name="Ukrainisch" class="interlanguage-link-target">Українська</a></li><li class="interlanguage-link interwiki-zh mw-list-item"><a href="https://zh.wikipedia.org/wiki/%E5%B8%83%E5%B0%94%E5%8F%AF%E6%BB%A1%E8%B6%B3%E6%80%A7%E9%97%AE%E9%A2%98" title="布尔可满足性问题 – Chinesisch" lang="zh" hreflang="zh" data-title="布尔可满足性问题" data-language-autonym="中文" data-language-local-name="Chinesisch" class="interlanguage-link-target">中文</a></li><li class="interlanguage-link interwiki-zh-yue mw-list-item"><a href="https://zh-yue.wikipedia.org/wiki/%E5%B8%83%E6%9E%97%E5%8F%AF%E6%BB%BF%E8%B6%B3%E5%BA%A6%E5%95%8F%E9%A1%8C" title="布林可滿足度問題 – Kantonesisch" lang="yue" hreflang="yue" data-title="布林可滿足度問題" data-language-autonym="粵語" data-language-local-name="Kantonesisch" class="interlanguage-link-target">粵語</a></li> </ul> <div class="after-portlet after-portlet-lang"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q875276#sitelinks-wikipedia" title="Links auf Artikel in anderen Sprachen bearbeiten" class="wbc-editpage">Links bearbeiten</a></div> </div> </nav> </div> </div> <footer id="footer" class="mw-footer" > <ul id="footer-info"> <li id="footer-info-lastmod"> Diese Seite wurde zuletzt am 23. September 2024 um 20:50 Uhr bearbeitet.</li> <li id="footer-info-copyright"><div id="footer-info-copyright-stats" class="noprint"><a rel="nofollow" class="external text" href="https://pageviews.wmcloud.org/?pages=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&project=de.wikipedia.org">Abrufstatistik</a> · <a rel="nofollow" class="external text" href="https://xtools.wmcloud.org/authorship/de.wikipedia.org/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik?uselang=de">Autoren</a> </div><div id="footer-info-copyright-separator"> </div><div id="footer-info-copyright-info"> Der Text ist unter der Lizenz <a rel="nofollow" class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.de">„Creative-Commons Namensnennung – Weitergabe unter gleichen Bedingungen“</a> verfügbar; Informationen zu den Urhebern und zum Lizenzstatus eingebundener Mediendateien (etwa Bilder oder Videos) können im Regelfall durch Anklicken dieser abgerufen werden. Möglicherweise unterliegen die Inhalte jeweils zusätzlichen Bedingungen. Durch die Nutzung dieser Website erklären Sie sich mit den <a class="external text" href="https://foundation.wikimedia.org/wiki/Policy:Terms_of_Use/de">Nutzungsbedingungen</a> und der <a class="external text" href="https://foundation.wikimedia.org/wiki/Policy:Privacy_policy/de">Datenschutzrichtlinie</a> einverstanden. Wikipedia® ist eine eingetragene Marke der Wikimedia Foundation Inc.</div></li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy/de">Datenschutz</a></li> <li id="footer-places-about"><a href="/wiki/Wikipedia:%C3%9Cber_Wikipedia">Über Wikipedia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikipedia:Impressum">Impressum</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Verhaltenskodex</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Entwickler</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/de.wikipedia.org">Statistiken</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Stellungnahme zu Cookies</a></li> <li id="footer-places-mobileview"><a href="//de.m.wikipedia.org/w/index.php?title=Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Mobile Ansicht</a></li> </ul> <ul id="footer-icons" class="noprint"> <li id="footer-copyrightico"><a href="https://wikimediafoundation.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/static/images/footer/wikimedia-button.svg" width="84" height="29" alt="Wikimedia Foundation" loading="lazy"></a></li> <li id="footer-poweredbyico"><a href="https://www.mediawiki.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/w/resources/assets/poweredby_mediawiki.svg" alt="Powered by MediaWiki" width="88" height="31" loading="lazy"></a></li> </ul> </footer> <script>(RLQ=window.RLQ||[]).push(function(){mw.log.warn("This page is using the deprecated ResourceLoader module \"codex-search-styles\".\n[1.43] Use a CodexModule with codexComponents to set your specific components used: https://www.mediawiki.org/wiki/Codex#Using_a_limited_subset_of_components");mw.config.set({"wgHostname":"mw-web.codfw.main-5767f597fb-wvx57","wgBackendResponseTime":166,"wgPageParseReport":{"limitreport":{"cputime":"0.409","walltime":"0.672","ppvisitednodes":{"value":2420,"limit":1000000},"postexpandincludesize":{"value":54070,"limit":2097152},"templateargumentsize":{"value":2747,"limit":2097152},"expansiondepth":{"value":11,"limit":100},"expensivefunctioncount":{"value":2,"limit":500},"unstrip-depth":{"value":0,"limit":20},"unstrip-size":{"value":47099,"limit":5000000},"entityaccesscount":{"value":0,"limit":400},"timingprofile":["100.00% 347.058 1 -total"," 29.62% 102.793 22 Vorlage:Literatur"," 26.70% 92.658 2 Vorlage:Internetquelle"," 9.24% 32.078 1 Vorlage:EnS"," 8.60% 29.830 1 Vorlage:Navigationsleiste_Karps_21_NP-vollständige_Probleme"," 7.18% 24.919 1 Vorlage:Navigationsleiste"," 5.78% 20.060 2 Vorlage:Str_len"," 5.15% 17.876 1 Vorlage:NavFrame"," 3.55% 12.324 1 Vorlage:Zitat"," 2.32% 8.056 1 Vorlage:ISSN"]},"scribunto":{"limitreport-timeusage":{"value":"0.119","limit":"10.000"},"limitreport-memusage":{"value":5480051,"limit":52428800}},"cachereport":{"origin":"mw-web.eqiad.main-5c7bc58d8b-vfzn2","timestamp":"20241126210226","ttl":2592000,"transientcontent":false}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"Erf\u00fcllbarkeitsproblem der Aussagenlogik","url":"https:\/\/de.wikipedia.org\/wiki\/Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik","sameAs":"http:\/\/www.wikidata.org\/entity\/Q875276","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q875276","author":{"@type":"Organization","name":"Autoren der Wikimedia-Projekte"},"publisher":{"@type":"Organization","name":"Wikimedia Foundation, Inc.","logo":{"@type":"ImageObject","url":"https:\/\/www.wikimedia.org\/static\/images\/wmf-hor-googpub.png"}},"datePublished":"2004-02-21T21:28:02Z","headline":"Entscheidungsproblem der theoretischen Informatik"}</script> </body> </html>