Video není dostupné.
Omlouváme se.
Propositional Logic #13 - SatSolving and the DPLL Algorithm
Vložit
- čas přidán 18. 08. 2024
- In this tutorial, I'll show you the theory behind solving propositional logic equations.
❤❤❤ Early access to tutorials, polls, live events, and downloads ❤❤❤
❤❤❤ www.patreon.co... ❤❤❤
❤❤❤ Not up for Patreon? ❤❤❤
❤❤❤ www.paypal.me/... ❤❤❤
🌍 Website
🌍 the-morpheus.de
¯\_(ツ)_/¯ Join the Community ¯\_(ツ)_/¯
** the-morpheus.d... **
** / themorpheustuts **
( ͡° ͜ʖ ͡°) More news? More code?
ℱ / themorpheustutorials
🐦 / themorpheustuts
🐙 github.com/The...
You order from Amazon? Order through me, costs you zero and you help me out
"-(¯`-.-'¯)-" amzn.to/2slBSgH
Video requests?
🎁 docs.google.co...
Questions? Feedback? Write me!
✉ www.patreon.co...
✉ / themorpheustutorials
✉ the-morpheus.d...
or just write a comment :)
Playlist: • Logik Tutorial
16 Stunden bis zur Klausur, konnte alles auch noch mit 1.25x Geschwindigkeit super nachvollziehen, toller Lehrer!
super, dann viel Erfolg!
Sehr ähnlich geht es mir gerade auch. =D
Your weakness digusts me XD Ich mache auf 2x Geschwindigkeit und verstehe auch noch alles
5 Studen zur Klausur XD mal schauen ob das reicht
Ich küss dein Auge Morpheus. Du rettest gerade Logik
😂❤️
Solche Qualitätsvideos findet man heutzutage selten. Normalerweise spuckt mir ein Inder mit seinem schlechten Englisch ins Gesicht.
Danke dafür!
Finde ich spannend. Habe mich gefragt ob man ab {{X,~Z},{X,Z}} überhaupt weitermachen muss mit DPLL, oder ob man das nicht viel einfacherŕund schneller einfach wegkürzen kann. {~Z},{Z} gleich streichen, bleibt {X},{X} -> true, aber hab dann einfach mal alle Varianten ausprobiert, ist bei allen true :)
Vielen Dank für deine Uploads! Bist wahrlich eine große Hilfe.
freut mich sehr =)
In welchem Semester studierst du?
2. Master
1. Bachelor bin ich. Welche Uni?
Du hast im 1. Semester schon Logik? Ich bin am KIT und selbst?
Jo, die Kommas sind mega verwirrend.
Was spricht denn gegen ein "v" und ein ^ Zeichen?
Ist wesentlich klarer
Das ist leider die offizielle Schreibweise für diesen Algorithmus
Wenn die ganze Konjunktion leer ist, ist aber keine 0 in der Konjunktion, sondern 1 && 1 && 1 && ..., da die Klauseln raus genommen werden, die true sind.
Hey eine kleine Frage, wenn ich bei 25:49, mich für Z entscheide zu wählen, bekomme ich ja bei zweiten Fall {{X,~Z}, {X,Z}, {~Z}} -> dann kommt da {{X}} raus und das ist doch weder True . Warum macht es einen Unterschied, was ich wähle, bei dir kommt da False raus
Hm, also durch das logische Oder sollte sich das doch wieder ausgleichen oder?
zu 28:30, wäre es für die Menge {{},{X}} auch false?
Ja weil die leere Menge durch nichts erfüllt werden kann. Und zwei Mengen werden mit UND verknüpft
Dieser Anfang..... wird das ein Porno.....
Aber klar 😏
Was ist der Unterschied zu Davis Putnam Algorithmus ? DP und DPLL ist ja nicht dasselbe
DPLL verfeinert den DP Algorithmus. Genaueres sprengt jetzt hier ein bisschen den Rahmen von nem Kommentar :D
Prog2?
Ich steig aus wenn du plötlich K schreibst und es nichtmal irgentwo definierst aber nur sagst das ist jetzt das.
Dieser ganze Logik Kram ist halt so lächerlich. Es ist so einfach, aber so viel kompliziertes drumrum gemacht. Der DPLL-Algorithmus ist einfach nur ein Programm, was nicht sonderlich schwer ist. Ich verstehe nicht wieso man das Programm mit irgendwelchen Fachbegriffen erklärt bekommt und warum man es quasi auswendig kennen soll. Das ist genauso sinnlos wie irgendwelche Gedichte von früheren Künstlern auswendig zu lernen.
Eigentlich recht simpel. Damit man auch andere Probleme und Anwendungen lösen kann, für die der dpll nichts nützt
@@TheMorpheusTutorials Ganz genau. Einen Algorithmus abspielen kann jeder. Einen Algorithmus entwickeln nur wenige. Und erst recht kann kaum jemand zeigen, dass ein Algorithmus auch wirklich das tut, was er tun soll. Dazu bedarf es mathematischer Grundlagen, die häufig nicht immer so einfach oder Anwendungsbezogen sind.
Wenn man jedoch die mathematische Grundlagen verinnerlicht hat, kann man den Algorithmus so verändern, dass er andere Probleme lösen kann oder das Problem effizienter lösen kann. SAT oder die Verallgemeinerung Satisfiability Modulo Theory (SMT) klingt zunächst nach reiner Spielerei. Aber wenn man SAT/SMT mit k-Induktion Verknüpft, erhält man k-Bounded Model Checker, die man bei der Verifikation von reaktiven Systemen verwenden kann. Damit kann man einen automatisierten mathematischen Beweis führen, dass böse Dinge innerhalb von k Berechnungszyklen nie eintreten werden (Sicherheitsanforderungen). Und sowas wird in Domänen wie Luft- und Raumfahrt auch tatsächlich gemacht! Auf sowas muss man nur erstmal kommen!
ERSTER ;)
+RocketlauncherLP Das ging schnell :D