Implikationsgraf

En implikationsgraf som representerar instansen $\scriptscriptstyle (x_{0}\lor x_{2})\land (x_{0}\lor \lnot x_{3})\land (x_{1}\lor \lnot x_{3})\ land (x_{1}\lor \lnot x_{4})\land (x_{2}\lor \lnot x_{4})\land {} \atop \quad \scriptstyle (x_{0}\lor \lnot x_{5})\land (x_{1}\lor \lnot x_{5})\land (x_{2}\lor \lnot x_{5})\land (x_{3}\lor x_{6} )\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6}).$ 2-tillfredsställelse

I matematisk logik och grafteori är en implikationsgraf en skevsymmetrisk , riktad graf G = ( V , E ) som består av vertexuppsättning V och riktad kantuppsättning E. Varje vertex i V representerar sanningsstatusen för en boolesk bokstavlig , och varje riktad kant från vertex u till vertex v representerar den materiella implikationen "Om det bokstavliga u är sant så är det bokstavliga v också sant". Implikationsgrafer användes ursprungligen för att analysera komplexa booleska uttryck .

Ansökningar

En instans med 2-tillfredsställelse i konjunktiv normalform kan omvandlas till en implikationsgraf genom att ersätta var och en av dess disjunktioner med ett par implikationer. Till exempel kan påståendet $(x_{0}\lor x_{1})$ skrivas om som paret ${\ displaystyle (\neg x_{0}\högerpil x_{1}),(\neg x_{1}\högerpil x_{0})}$ . En instans är tillfredsställbar om och endast om ingen bokstavlig och dess negation hör till samma starkt sammankopplade komponent i dess implikationsgraf; denna karakterisering kan användas för att lösa 2-tillfredsställande fall i linjär tid.

I CDCL SAT- lösare kan enhetsutbredning naturligt associeras med en implikationsgraf som fångar alla möjliga sätt att härleda alla implicita literaler från beslutsliteraler, som sedan används för satsinlärning.