RecycleUnits - RecycleUnits

v matematická logika, důkaz komprese pomocí RecycleUnits^[1] je metoda pro kompresi výroková logika rozlišení důkazů Jeho hlavní myšlenkou je využít průběžné (např. Nezadané) výsledky důkazu jako jednotky doložky, tj. klauzule obsahující pouze jeden literál. Určité uzly důkazu lze nahradit uzly představujícími tyto klauzule jednotek. Po této operaci se získaný graf transformuje na platný důkaz. Výstupní důkaz je kratší než originál, přičemž je ekvivalentní nebo silnější.

Algoritmy

Algoritmy považují důkazy rozlišení za směrované acyklické grafy, kde je každý uzel označen klauzulí a každý uzel má jednoho nebo dva předchůdce zvané rodiče. Pokud má uzel dva rodiče, je také označen výrokovou proměnnou zvanou pivot, která byla použita k výpočtu klauzule uzlů pomocí rozlišení.
Následující algoritmus popisuje nahrazení uzlů.
Předpokládá se, že v důkazu rozlišení pro všechny nelistové uzly se dvěma nadřazenými uzly obsahuje levý nadřazený uzel kladnou a pravý nadřazený uzel zápornou proměnnou pivot. Algoritmus nejprve iteruje přes všechny klauzule nelistových jednotek a poté přes všechny předkové uzly důkazu. Pokud je otočným prvkem uzlu proměnná doslovného klauzule současné jednotky, jeden z nadřazených uzlů lze nahradit uzlem odpovídajícím klauzuli jednotky. Z výše uvedeného předpokladu, pokud se literál rovná pivot, levý rodič obsahuje literál a může být nahrazen uzlem klauzule jednotky. Pokud se literál rovná negaci pivot, nahradí se pravý rodič.

1  funkce RecycleUnits (Důkaz  ${ displaystyle P}$ ): 2 Let  ${ displaystyle U}$  být množinou nelistových uzlů představujících jednotkové klauze3 pro každý  ${ displaystyle u v U}$  dělat4 Označte předky u5 pro každý neoznačený  ${ displaystyle n v P}$  dělat6 let  ${ displaystyle p}$  být kontingenční proměnnou  ${ displaystyle n}$ 7 let  ${ displaystyle l}$  být doslovný obsažený v klauzuli  ${ displaystyle u}$ 8              -li  ${ displaystyle p == l}$  pak9 nahraďte levého rodiče  ${ displaystyle n}$  s  ${ displaystyle u}$ 10             jinak pokud  ${ displaystyle neg p == l}$  pak11 nahradit pravého rodiče  ${ displaystyle n}$  s  ${ displaystyle u}$

Obecně po provedení této funkce už důkaz nebude právním důkazem. Následující algoritmus vezme kořenový uzel důkazu a vytvoří z něj právní důkaz. Výpočet začíná rekurzivními voláními na podřízené uzly. Za účelem minimalizace volání algoritmu se sleduje, které uzly již byly navštíveny. Všimněte si, že důkaz rozlišení lze považovat za obecně zaměřený acyklický graf na rozdíl od stromu. Po rekurzivním volání se aktualizuje klauzule tohoto uzlu. Přitom mohou nastat čtyři různé případy. Současná proměnná proměnné se může vyskytnout v obou, vlevo, vpravo nebo v žádném z nadřazených uzlů. Pokud k tomu dojde v obou nadřazených uzlech, klauzule se vypočítá jako resolvent nadřazených klauzulí. Pokud není k dispozici v jednom z nadřazených uzlů, lze klauzuli tohoto nadřazeného uzlu zkopírovat. Pokud to chybí u obou rodičů, je třeba si vybrat heuristicky.

1  funkce ReconstructProof (uzel  ${ displaystyle n}$ ):3      -li  ${ displaystyle n}$  je navštíveno vrátit se4 značka  ${ displaystyle n}$  jak bylo navštíveno5 -li  ${ displaystyle n}$  nemá rodiče vrátit se6      jinak pokud  ${ displaystyle n}$  má pouze jednoho rodiče  ${ displaystyle x}$  pak7 ReconstructProof ( ${ displaystyle x}$ )8           ${ displaystyle n}$ . Klauzule =  ${ displaystyle x}$ . Klauzule9 jiný10 let  ${ displaystyle l}$  být vlevo a  ${ displaystyle r}$  pravý nadřazený uzel 11 let  ${ displaystyle p}$  být kontingenční proměnnou používanou k výpočtu  ${ displaystyle n}$ 12 ReconstructProof ( ${ displaystyle l}$ ) 13 ReconstructProof ( ${ displaystyle r}$ )14         -li  ${ displaystyle p in l.Clause}$  a  ${ displaystyle p in r.Clause}$ 15              ${ displaystyle n}$ .Clause = Vyřešit ( ${ displaystyle l}$ , ${ displaystyle r}$ , ${ displaystyle p}$ )16         jinak pokud  ${ displaystyle p in l.Clause}$  a  ${ displaystyle p notin r. klauzule}$ 17              ${ displaystyle n}$ . Klauzule =  ${ displaystyle r}$ .Clause18 smazat odkaz na  ${ displaystyle l}$ 19         jinak pokud  ${ displaystyle p in r.Clause}$  a  ${ displaystyle p notin l. klauzule}$ 20              ${ displaystyle n}$ . Klauzule =  ${ displaystyle l}$ .Clause21 smazat odkaz na  ${ displaystyle r}$ 22         jiný23 let  ${ displaystyle x in {l, r }}$  a  ${ displaystyle y in {l, r } setminus {x }}$  // vyberte x heuristicky24  ${ displaystyle n}$ . Klauzule =  ${ displaystyle x}$ .Clause25 smazat odkaz na  ${ displaystyle y}$

Příklad

Zvažte následující důkaz rozlišení.
Jedním z mezivýsledků je ${ displaystyle C_ {8}}$ což představuje jednotkovou klauzuli (-1).

${ displaystyle (1) { cfrac {(2) { cfrac {(1) { cfrac {C_ {1} (1,3) qquad C_ {2} (- 1,2,5)} {C_ {3} (2,3,5)}} qquad C_ {4} (1, -2)} {C_ {7} (1,3,5)}} qquad (4) { cfrac {C_ { 5} (- 1,4) qquad C_ {6} (- 1, -4)} { color {red} C_ {8} (- 1)}}} {C_ {9} (3,5)} }}$

Existuje jeden uzel, který není předkem a používá proměnnou 1 jako otočný prvek: ${ displaystyle C_ {3}}$ .

${ displaystyle (1) { cfrac {(2) { cfrac {{ color {red} (1)} { cfrac {C_ {1} (1,3) qquad C_ {2} (- 1, 2,5)} {C_ {3} (2,3,5)}} qquad C_ {4} (1, -2)} {C_ {7} (1,3,5)}} qquad (4 ) { cfrac {C_ {5} (- 1,4) qquad C_ {6} (- 1, -4)} {C_ {8} (- 1)}}} {C_ {9} (3,5 )}}}$

Doslovný -1 je obsažen v pravém rodiči tohoto uzlu, a proto je tento rodič nahrazen znakem ${ displaystyle C_ {8}}$ . Řetězec ${ displaystyle {C_ {8}} ^ {*}}$ označuje odkaz na klauzuli ${ displaystyle C_ {8}}$ (struktura je nyní spíše namířeným acyklickým grafem než stromem).

${ displaystyle (1) { cfrac {(2) { cfrac {(1) { cfrac {C_ {1} (1,3) qquad { color {red} {C_ {8}} ^ {* }}} {C_ {3} (2,3,5)}} qquad C_ {4} (1, -2)} {C_ {7} (1,3,5)}} qquad (4) { cfrac {C_ {5} (- 1,4) qquad C_ {6} (- 1, -4)} {C_ {8} (- 1)}}} {C_ {9} (3,5)} }}$

Tato struktura již není právním důkazem, protože ${ displaystyle C_ {3}}$ není rezolventem společnosti ${ displaystyle C_ {1}}$ a ${ displaystyle C_ {8}}$ . Proto se musí znovu transformovat do jednoho.
Prvním krokem je aktualizace ${ displaystyle C_ {3}}$ . Protože se kontingenční proměnná 1 objevuje v obou nadřazených uzlech, ${ displaystyle C_ {3}}$ se počítá jako jejich rozpouštědlo.

${ displaystyle (1) { cfrac {(2) { cfrac {(1) { cfrac {C_ {1} (1,3) qquad {C_ {8}} ^ {*}} {C_ {3 } { color {red} (3)}}} qquad C_ {4} (1, -2)} {C_ {7} (1,3,5)}} qquad (4) { cfrac {C_ {5} (- 1,4) qquad C_ {6} (- 1, -4)} {C_ {8} (- 1)}}} {C_ {9} (3,5)}}}$

Levý nadřazený uzel ${ displaystyle C_ {7}}$ neobsahuje proměnnou pivot a proto je klauzule tohoto rodiče zkopírována do klauzule ${ displaystyle C_ {7}}$ . Souvislost mezi ${ displaystyle C_ {7}}$ a ${ displaystyle C_ {4}}$ je odstraněn a protože na něj neexistují žádné další odkazy ${ displaystyle C_ {4}}$ tento uzel lze smazat.

${ displaystyle (1) { cfrac {{ cfrac {(1) { cfrac {C_ {1} (1,3) qquad {C_ {8}} ^ {*}} {C_ {3} (3 )}}} {C_ {7} { color {red} (3)}}} qquad (4) { cfrac {C_ {5} (- 1,4) qquad C_ {6} (- 1, -4)} {C_ {8} (- 1)}}} {C_ {9} (3,5)}}}$

Opět levý rodič ${ displaystyle C_ {9}}$ neobsahuje proměnnou pivot a provádí se stejná operace jako dříve.

${ displaystyle { cfrac { cfrac {(1) { cfrac {C_ {1} (1,3) qquad (4) { cfrac {C_ {5} (- 1,4) qquad C_ {6 } (- 1, -4)} {C_ {8} (- 1)}}} {C_ {3} (3)}}} {C_ {7} (3)}} {C_ {9} { barva {red} (3)}}}}$

Poznámka: reference ${ displaystyle {C_ {8}} ^ {*}}$ byl nahrazen skutečným kontrolním uzlem ${ displaystyle C_ {8}}$ .
Výsledkem tohoto důkazu je jednotková klauzule (3), která je silnějším výsledkem než klauzule (3,5) původního důkazu.

Poznámky

^ Bar-Ilan, O .; Fuhrmann, O .; Hoory, S.; Shacham, O.; Strichman, O. Lineární redukce důkazů o rozlišení. Hardware a software: Verifikace a testování, s. 114–128, Springer, 2011.

[1] Bar-Ilan, O .; Fuhrmann, O .; Hoory, S.; Shacham, O.; Strichman, O. Lineární redukce důkazů o rozlišení. Hardware a software: Verifikace a testování, s. 114–128, Springer, 2011.

[1]