Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
6. Propositional Logic: SAT Solvers
verfasst von : Prof. Mordechai Ben-Ari
Erschienen in: Mathematical Logic for Computer Science
Verlag: Springer London
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Abstract
Although it is believed that there is no efficient algorithm for the decidability of satisfiability in propositional logic, many algorithms are efficient in practice. This is particularly true when a formula is satisfiable; for example, when you build a truth table for an unsatisfiable formula of size n you will have to generate all 2
n
rows, but if the formula is satisfiable you might get lucky and find a model after generating only a few rows. Even an incomplete algorithm—one that can find a model if one exists but may not be able to detect if a formula is unsatisfiable—can be useful in practice.