Wikiszótár

Boole-függvények kielégíthetőségének problémája

Magyar

Kiejtés

  • IPA: [ ˈboolɛfyɡveːɲɛk ˈkijɛleːɡiːthɛtøːʃeːɡeːnɛk ˈprobleːmaːjɒ]

Főnév

Boole-függvények kielégíthetőségének problémája

  1. (matematika, algoritmusok)

Boolean Satisfiability Problem (SAT)

Definíció

A **Boolean satisfiability problem (SAT)** a logikai algebra egy alapvető problémája. A SAT problémában azt kell eldönteni, hogy egy adott logikai formula kielégíthető-e, azaz létezik-e olyan változóérték-beállítás (True/False), amely a formulát igazságra (True) értékeli.

Példa: Adott a következő logikai formula:   A kérdés: létezik-e olyan értékadás  -ra, amely igazságra értékeli a formulát?

SAT Probléma Típusai

  1. Általános SAT probléma:
    Tetszőleges logikai formulák, például:  
  2. 3-SAT probléma:
    A formulát három literálból álló zárójeles kifejezések konjunkciójaként írjuk fel (pl.  ).
  3. Horn-SAT:
    Minden zárójeles kifejezés legfeljebb egy pozitív literált tartalmaz.

SAT Probléma Nehézsége

  • A SAT probléma az első ismert NP-teljes probléma, ami azt jelenti, hogy ha hatékony megoldási algoritmust találunk a SAT problémára, az minden NP-problémára is hatékony megoldást nyújtana.
  • A SAT probléma megoldása exponenciális időigényű lehet a változók számától függően.

Megoldási Módszerek

  1. Brute Force:
    Vizsgáljuk meg az összes lehetséges változóérték-beállítást ( , ahol   a változók száma). Nagyon lassú nagy méretű formulák esetén.
  2. DPLL Algoritmus (Davis-Putnam-Logemann-Loveland):
    Rekurzív keresési algoritmus, amely a változók értékeinek próbálgatásával dolgozik.
    • Kulcsfontosságú technikák:
      • Egyliterálos zárás (Unit Propagation): Ha egy klózban csak egy literál van, annak értéke meghatározott.
      • Pusztító lépés (Pure Literal Elimination): Ha egy literál csak egyfajta (pozitív/negatív) formában fordul elő, akkor annak értéke meghatározott.
  3. Modern SAT Solverek:
    • Olyan fejlett algoritmusok, mint a CDCL (Conflict-Driven Clause Learning), amelyek a konfliktusok tanulásával optimalizálják a keresést.
  4. Heurisztikus és Metaheurisztikus Módszerek:
    • Például Genetikus algoritmusok, szimulált lehűlés.

Python Implementáció Egyszerű SAT Solverhez

def is_satisfiable(formula):
    """
    SAT Solver a DPLL algoritmus alapján.
    
    Args:
        formula: A SAT formula klózok listájaként, ahol minden klóz literálok listája.
                 Literálok pozitív vagy negatív egész számok (pozitív = True, negatív = False).
    Returns:
        kielégíthető-e a formula (True/False).
    """
    if not formula:
        return True  # Üres formula kielégíthető
    if any([len(clause) == 0 for clause in formula]):
        return False  # Üres klóz, tehát nem kielégíthető

    # Egyliterálos zárás
    for clause in formula:
        if len(clause) == 1:
            literal = clause[0]
            return is_satisfiable(assign(formula, literal))

    # Válassz egy literált és próbálkozz
    literal = formula[0][0]
    return is_satisfiable(assign(formula, literal)) or is_satisfiable(assign(formula, -literal))

def assign(formula, literal):
    """
    A formula egyszerűsítése egy literál értékadásával.
    """
    new_formula = []
    for clause in formula:
        if literal in clause:
            continue  # Ez a klóz kielégíthető
        new_clause = [x for x in clause if x != -literal]
        new_formula.append(new_clause)
    return new_formula

# Példa formula: (x1 ∨ ¬x2) ∧ (x2 ∨ x3)
formula = [[1, -2], [2, 3]]  # x1: 1, ¬x2: -2, x2: 2, x3: 3

result = is_satisfiable(formula)
print("Kielégíthető a formula:", result)

Példa Kimenet

Adott formula:  

Kimenet: 

Kielégíthető a formula: True

Alkalmazások

  1. Hardver és szoftver ellenőrzés:
  Hibák és logikai következetlenségek detektálása.
  1. Mesterséges intelligencia:
  Problémamegoldás és tervezés.
  1. Optimalizálási problémák:
  Lineáris programozás és egészértékű programozás fordítása SAT problémává.
  1. Kriptográfia:
  Kriptoanalízis, például rejtjelek törése.

Előnyök és Kihívások

Előnyök

  • Az SAT egy általános probléma, amely számos egyéb optimalizálási problémára visszavezethető.
  • Hatékony modern SAT solverek elérhetők, például MiniSAT, Z3 Solver.

Kihívások

  • A probléma NP-teljes, ezért a legrosszabb esetben exponenciális időt igényel.
  • Nagy méretű formulák kezelése memória- és időigényes.

Összegzés

A **SAT probléma** a logikai és kombinatorikai optimalizáció alapvető építőköve. Bár NP-teljes, a modern solverek képesek hatékonyan kezelni a valós alkalmazásokban felmerülő SAT problémák nagy részét. Pythonban a DPLL algoritmus vagy egy modern SAT solver, például a PySAT vagy Z3, egyszerűen alkalmazható.

Fordítások

Tartalom

További információk

A lap eredeti címe: „https://hu.wiktionary.org/w/index.php?title=Boole-függvények_kielégíthetőségének_problémája&oldid=3479789”