Enhetsutbredning

Unit propagation ( UP ) eller Boolean Constraint propagation ( BCP ) eller en-literal rule ( OLR ) är en procedur för automatiserad teorembevisande som kan förenkla en uppsättning (vanligtvis propositionella ) satser .

Definition

Förfarandet bygger på enhetssatser , dvs satser som är sammansatta av en enda bokstavlig , i konjunktiv normalform. Eftersom varje klausul måste vara uppfylld, vet vi att detta bokstavliga måste vara sant. Om en uppsättning satser innehåller enhetssatsen $l$ , förenklas de andra satserna genom tillämpningen av de två följande reglerna:

1. varje sats (förutom själva enhetssatsen) som innehåller $l$ tas bort (satsen är uppfylld om $l$ är);
2. i varje sats som innehåller $\neg l$ raderas den här bokstaven ( $\neg l$ kan inte bidra till att den är uppfylld).

Tillämpningen av dessa två regler leder till en ny uppsättning klausuler som är likvärdig med den gamla.

Till exempel kan följande uppsättning satser förenklas genom enhetsutbredning eftersom den innehåller enhetssatsen $a$ .

$\{a\vee b,\neg a\vee c,\neg c\vee d,a\}$

Eftersom $a\vee b$ innehåller bokstaven $a$ , kan denna sats tas bort helt och hållet. Eftersom $\neg a\vee c$ innehåller negationen av literalen i enhetssatsen, kan denna literal tas bort från satsen. Enhetssatsen $a$ tas inte bort; detta skulle göra att den resulterande uppsättningen inte är likvärdig med den ursprungliga; denna klausul kan tas bort om den redan har lagrats i någon annan form (se avsnittet "Använda en delmodell"). Effekten av enhetsutbredning kan sammanfattas enligt följande.

$\{$	$a\vee b,$	$\neg a\vee c,$	$\neg c\vee d,$	$a$	$\}$
	(tog bort)	( $\neg a$ raderad)	(oförändrad)	(oförändrad)
$\{$		$c,$	$\neg c\vee d,$	$a$	$\}$

Den resulterande uppsättningen av satser $\{c,\neg c\vee d,a\}$ är ekvivalent med ovanstående. Den nya enhetssatsen $c$ som är resultatet av enhetsutbredning kan användas för en ytterligare tillämpning av enhetsutbredning, vilket skulle omvandla $\neg c\vee d$ till $d$ .

Enhetsutbredning och upplösning

Den andra regeln för enhetsutbredning kan ses som en begränsad form av upplösning , där en av de två upplösningsmedlen alltid måste vara en enhetsklausul. När det gäller upplösning är enhetsutbredning en korrekt slutledningsregel, eftersom den aldrig producerar en ny klausul som inte innebar av de gamla. Skillnaderna mellan enhetsutbredning och upplösning är:

1. upplösning är en fullständig vederläggningsprocedur medan enhetsutbredning inte är det; med andra ord, även om en uppsättning satser är motsägelsefulla, kan enhetsutbredning inte generera en inkonsekvens;
2. de två satserna som är lösta kan i allmänhet inte tas bort efter att den genererade klausulen har lagts till i uppsättningen; tvärtom, icke-enhetsklausulen som är involverad i en enhetsutbredning kan tas bort när dess förenkling läggs till i uppsättningen;
3. upplösning inkluderar i allmänhet inte den första regeln som används vid enhetsförökning.

Upplösningskalkyler som inkluderar subsumtion kan modellera regel ett genom subsumtion och regel två genom ett enhetsupplösningssteg, följt av subsumtion.

Enhetsutbredning, som tillämpas upprepade gånger när nya enhetssatser genereras, är en fullständig tillfredsställelsealgoritm för uppsättningar av propositionella Horn-satser ; den genererar också en minimal modell för uppsättningen om den är tillfredsställande: se Horn-satisfiability .

Använder en delmodell

De enhetssatser som finns i en uppsättning klausuler eller kan härledas från den kan lagras i form av en delmodell (denna delmodell kan också innehålla andra bokstaver, beroende på applikation). I det här fallet utförs enhetsutbredning baserat på den partiella modellens literaler och enhetssatser tas bort om deras literal finns i modellen. I exemplet ovan skulle enhetssatsen $a$ läggas till i den partiella modellen; förenklingen av uppsättningen satser skulle då fortsätta som ovan med skillnaden att enhetssatsen $a$ nu tas bort från mängden. Den resulterande uppsättningen av klausuler är ekvivalent med den ursprungliga under antagandet om giltigheten av bokstaverna i den partiella modellen.

Komplexitet

Den direkta implementeringen av enhetsutbredning tar tid kvadratiskt i den totala storleken på uppsättningen att kontrollera, vilket definieras som summan av storleken på alla satser, där storleken på varje sats är antalet bokstaver som den innehåller.

Enhetsutbredning kan dock göras i linjär tid genom att lagra, för varje variabel, listan över satser där varje bokstav finns. Till exempel kan uppsättningen ovan representeras genom att numrera varje sats enligt följande:

$\{1:a\vee b,2:\neg a\vee c,3:\neg c\vee d,4:a\}$

och sedan lagra, för varje variabel, listan med satser som innehåller variabeln eller dess negation:

$a:1\ 2\ 4$

$b:1$

$c:2\ 3$

$d:3$

Denna enkla datastruktur kan byggas i tid linjär i storleken på uppsättningen, och gör det möjligt att hitta alla satser som innehåller en variabel mycket enkelt. Enhetsutbredning av en literal kan utföras effektivt genom att endast skanna listan av satser som innehåller variabeln för literalen. Mer exakt är den totala körtiden för att utföra enhetsutbredning för alla enhetssatser linjär i storleken på uppsättningen av satser.

Se även

• Horn tillfredsställelse
• Hornklausul
• Automatiserad teorembevisande
• DPLL-algoritm

•   Dowling, William F.; Gallier, Jean H. (1984), "Linear-time algorithms for testing the satisfiability of propositional Horn formulae", Journal of Logic Programming , 1 (3): 267–284, doi : 10.1016/0743-1066(84)90014- 1 , MR 0770156 .
• H. Zhang och M. Stickel (1996). En effektiv algoritm för enhetsutbredning. I Proceedings of the Fourth International Symposium on Artificiell Intelligens och Matematik .