Rozhodovací procedury a verifikace Pavel Surynek, KTIML

6 Rozhodovací procedury a verifikace Pavel Surynek, KTIML http://ktiml.mff.cuni.cz/~surynek/nail094 Matematicko-fyzikální fakulta Univerzita Karlova v Praze

1

Lineární aritmetika 

Budeme zabývat rozhodovacími procedurami pro konjunkce lineárních podmínek. 

Definice 11.1 (formule lineární aritmetiky). Nechť Var je množina symbolů pro proměnné, Cons nechť je množina symbolů pro konstanty (VarCons=). Formule lineární aritmetiky je slovo dané následující gramatikou:      



Počáteční neterminál I, další neterminály T, A, S Množina terminálů = VarCons {,=,<,≤,+,(,)} I  II |(I) | I  A AS=S|S<S|S≤S ST|SS+T T  v | c | cv pro vVar, cCons

I … odpovídá formuli, A … odpovídá atomu, S … odpovídá součtu, T … odpovídá termu.

2 / Rozhodovací procedury a verifikace, 11. přednáška

Pavel Surynek, 2016

Lineární aritmetika - poznámky 



Z formálního hlediska je lineární aritmetika teorie obsahující axiomy pro binární relace =, <, ≤, binární funkci + a unární funkce c pro cCons (násobení konstantou). Jako doménu uvažujeme buď racionální nebo celá čísla: 



Rozhodování o splnitelnosti je v prvním případě polynomiální, v druhém NPúplný problém.

Příklad formule lineární aritmetiky:

3y1 + 2y2 ≤ 5y3 ∧ 2y1 - 2 y2 = 0 Tělo smyčky  Motivační příklad: for (i = 1; i <= 10; i++) R4 ← mem[a+R2] { R5 ← R2 + R1 a[j+i] = a[j] mem*a+R5+ ← R4 } R1 ← R1 + 1 



R4 ← mem[a+R2] Mimo tělo smyčky

Tělo smyčky R5 ← R2 + R1 mem*a+R5+ ← R4 R1 ← R1 + 1

a[j] se nesmí měnit, tj. formule (i≥1 ∧ i≤10 ∧ j+i=j) musí být nesplnitelná.


Pavel Surynek, 2016

Rozhodování lineární aritmetiky 

Lineární programování (LP)  



Celočíselné lineární programování (ILP)  



Zadání: konjunkce lineárních nerovností a lineární objektivní funkce (=lineární program). Hledáme ohodnocení proměnných racionálními čísly, které splňuje nerovnosti a maximalizuje (minimalizuje) objektivní funkci. Zadání: opět lineární program (nerovnosti a objektivní funkce) Hledáme celočíselné ohodnocení proměnných, které splňuje stejné podmínky.

Rozhodování lineární aritmetiky  

Zadání: konjunkce lineárních nerovností, tj. formule lineární aritmetiky. Chceme odpověď, zda existuje ohodnocení proměnných racionálními čísly splňující danou formuli.


Pavel Surynek, 2016

Obecný simplex (1)  

Obecný simplex je metoda pro rozhodování lineární aritmetiky s rovnostmi a neostrými nerovnostmi. Lineární nerovnosti tvořící formuli lineární aritmetiky jsou požadovány ve speciálním tvaru, tzv. obecný tvar: 

Rovnosti tvaru: 



a1x1 + a2x2+ … + anxn = 0, kde x1, x2, … , xn jsou racionální proměnné a a1, a2, … , an racionální konstanty.

Dolní a horní mez pro proměnné:  li ≤ xi ≤ ui pro i = 1,2, …,n, kde li a ui jsou racionální konstanty nebo -∞ 



resp. +∞. Poznámka: V klasickém simplexovém algoritmu požadujeme proměnné nezáporné.

Převod na obecný tvar: 

Nechť se formule skládá z m lineárních podmínek ve tvaru Li Δ Ri, kde Δ  ,=, ≤, ≥-, pro I = 1,2,…,m.


Pavel Surynek, 2016

Obecný simplex (2) 

Převod na obecný tvar: 

Případ Li ≤ Ri (resp. Li ≥ Ri)  



Případ Li = Ri: 







Podmínku Li ≤ Ri, převedeme na tvar Li’ ≤ bi, kde bi je racionální konstanta. Zavedeme novou proměnnou si, původní podmínku nahradíme podmínkami Li’ - si = 0 a si ≤ bi. Podmínku Li = Ri, převedeme na tvar Li’ = bi, kde bi je racionální konstanta. Zavedeme novou proměnnou si, původní podmínku nahradíme podmínkami Li’ - si = 0, si ≤ bi a si ≥ bi.

Původní proměnné y1, y2, … , yn se nazývají problémové proměnné, proměnné s1, s2, … , sm se nazývají dodatečné. Příklad:  

y1 + y2 ≥ 2 ∧ 2y1 – y2 ≥ 0 ∧ -y1 + 2y2 ≥ 1 y1 + y2 – s1 = 0 ∧ 2y1 – x2 – s2 = 0 ∧ -y1 + 2y2 – s3 = 0 ∧ s1 ≥ 2 ∧ s2 ≥ 0 ∧ s3 ≥ 1.


Pavel Surynek, 2016


Úlohu nalezení splňujícího ohodnocení proměnných je možné nahlížet geometricky:   

Každá proměnná představuje dimenzi, podmínky představují nadroviny (rovnosti) a poloprostory (nerovnosti). Uzavřený podprostor splňujících ohodnocení je průnikem nadrovin a poloprostorů, jedná se o konvexní polytop. y1 + y2 ≥ 2 ∧ 2y1 – y2 ≥ 0 ∧ -y1 + 2y2 ≥ 1 y2

2y1 - y2 ≥ 0

4 3

-y1 + 2y2 ≥ 0

2 1

y1 + y2 ≥ 2 0

1


2

3

4

y1 Pavel Surynek, 2016




Koeficienty v zadání úlohy reprezentujeme jako matici A typu m × (n + m), proměnné y1, y2, … , yn, s1, s2, … ,sm reprezentujeme jako vektor x (prvky matice značíme aij pro i=1,2,…,m a j=1,2,…,n+m). Lze použít ekvivalentní formulaci: 

Ax = 0 a ∧i=1n+m li ≤ xi ≤ ui 

y1 + y2 – s1 = 0 ∧ 2y1 – y2 – s2 = 0 ∧ -y1 + 2y2 – s3 = 0 ∧ s1 ≥ 2 ∧ s2 ≥ 0 ∧ s3 ≥ 1

1 1 -1 0 0 A = 2 -1 0 -1 0 -1 2 0 0 -1 

2 ≤ s1 (≤ +∞) (-∞ ≤ y1 ≤ +∞) 0 ≤ s2 (≤ +∞) (-∞ ≤ y2 ≤ +∞) 1 ≤ s3 (≤ +∞)

Nebo se používá tabulková reprezentace (matice A bez diagonální podmatice s -1).


A je pro pořadí proměnných: x = (y1, y2, s1, s2 , s3)

y1

y2

s1

1

1

s2

2

-1

s3

-1 2

2 ≤ s1 (≤ +∞) 0 ≤ s2 (≤ +∞) 1 ≤ s3 (≤ +∞) (-∞ ≤ y1 ≤ +∞) (-∞ ≤ y2 ≤ +∞) Pavel Surynek, 2016


V průběhu obecného simplexu se bude matice A (tabulka) měnit, ovšem sloupce odpovídající diagonální podmatici s -1 budou stále přítomné (permutovaně). 

 

Definice 11.2 (bázické, nebázické proměnné). Množina proměnných odpovídající sloupcům diagonální podmatice s -1 se nazývá množina bázických proměnných, značí se B. Ostatní proměnné se nazývají nebázické a značí se N.

Lze psát: ∧xiB(xi=∑xjN aijxj), toto plyne přímo z Ax=0 a definice 11.2. Algoritmus bude udržovat následující: 



Ohodnocení α:BN  Q (racionální čísla) Invarianty (i) a (ii): (i): Axα = 0, kde xα = (α(x1), α(x2),…, α(xn+m)) (ii): (xjN) lj ≤ α(xj) ≤ uj


Pavel Surynek, 2016

Obecný simplex (6) - algoritmus 

Na vstupu nechť je formule L lineární aritmetiky s m rovnostmi a neostrými nerovnostmi.

function GENERAL-SIMPLEX(L): boolean Pořadí proměnných je pevné převeď formuli L na obecný tvar: Ax = 0 a ∧i=1m li ≤ si ≤ ui B ← {s1,s2, …, sm} s1,s2, …, sm jsou bázické proměnné N ← {y1,y2, …, yn} y1,y2, …, yn jsou nebázické proměnné for i=1,2,…,n+m do [y1,y2, …, yn, s1,s2, …, sm] = [x1,x2, …, xn+m ] α(xi) ← 0 while True do Satisfied ← True for i=1,2,…,n+m do if xiB and (li > α(xi) or α(xi) > ui ) then Satisfied ← False, Pivot ← False for j=1,2,…,n+m do if xjN and xi a xj lze pivotovat then Pivot ← True proveď pivotaci s xi a xj if not Pivot then return False Formule je nesplnitelná if Satisfied then return True Formule je splnitelná 10 / Rozhodovací procedury a verifikace, 11. přednáška

Pavel Surynek, 2016

Operace pivotace (1) 

Nechť xiB je taková, že α(xi) > ui (bez újmy na

obecnosti). 







 

Je tedy třeba snížit hodnotu α(xi). Platí, že xi=∑xjN aijxj , tedy hodnota α(xi) může být redukována snížením hodnoty xjN, kde aij > 0 a lj<α(xj), nebo zvýšením hodnoty xkN, kde aik < 0 a α(xk)

Pavel Surynek, 2016

Operace pivotace (2) 

Chceme tedy přehodit xi a xj. 



Definice 11.3 (pivot, pivotový sloupec, pivotový řádek). Pro proměnné xi a xj se koeficient aij tabulky nazývá pivot. Sloupec s proměnnou xj se nazývá pivotový sloupec (xj nebázická, nebázické odpovídají sloupcům), řádek s proměnnou xi se nazývá pivotový řádek (xi bázická, bázické odpovídají řádkům).

Platí, že aij≠0: 

Vyřešíme řádek i pro xj. 

 



tj. z rovnosti xi = ∑xlN ailxl obdržíme rovnost xj = ∑xlN l≠j (-ail/aij)xl + (1/aij)xi

Ve všech ostatních řádcích k≠i eliminujeme proměnnou xj pomocí získané rovnosti. Vypočteme novou hodnotu ohodnocení pro bázické proměnné.

V algoritmu postupujeme při výběru pivota podle pevného pořadí proměnných (Blandovo pravidlo), žádní množina bázických proměnných se nezopakuje, algoritmus vždy skončí (bez důkazu).


Pavel Surynek, 2016

Obecný simplex – příklad (1) 

Uvažujme formuli:  



y1 + y2 ≥ 2 ∧ 2y1 – y2 ≥ 0 ∧ -y1 + 2y2 ≥ 1 y1 + y2 – s1 = 0 ∧ 2y1 – x2 – s2 = 0 ∧ -y1 + 2y2 – s3 = 0 ∧ s1 ≥ 2 ∧ s2 ≥ 0 ∧ s3 ≥ 1. y1

y2

s1

1

1

s2

2

-1

s3

-1 2

2 ≤ s1 (≤ +∞) 0 ≤ s2 (≤ +∞) 1 ≤ s3 (≤ +∞) (-∞ ≤ y1 ≤ +∞) (-∞ ≤ y2 ≤ +∞)

α(s1)=0 α(s2)=0 α(s3)=0 α(y1)=0 α(y2)=0

Dolní mez pro s1 je porušená, protože α(s1) < 2. Zvýšíme proměnnou y1 o θ = (2 - 0)/1 (první, se kterou lze pivotovat, shora neomezená). 

Vyřešíme rovnost pro y1: s1 = y1 + y2  y1 = s1 – y2


N={y1, y2} B={s1, s2, s3} pořadí: y1, y2, s1, s2, s3 y2

2y1 - y2 ≥ 0

4 3 2

-y1 + 2y2 ≥ 0

1

y1 + y2 ≥ 2 0

1

2

3

4

y1

Pavel Surynek, 2016


 

Nahradíme (eliminujeme) y1 v ostatních rovnostech pravou stranou s1 – y2: s2 = 2(s1 - y2) – y2  s2 = 2s1 – 3y2 s3 = -(s1 - y2) – 2y2  s3 = -s1 + 3y2 s1

y2

y1

1

-1

s2

2

-3

s3

-1 3

2 ≤ s1 (≤ +∞) 0 ≤ s2 (≤ +∞) 1 ≤ s3 (≤ +∞) (-∞ ≤ y1 ≤ +∞) (-∞ ≤ y2 ≤ +∞)

α(s1)=2 α(s2)=4 α(s3)=-2 α(y1)=2 α(y2)=0

Dolní mez pro s3 je porušená, protože α(s3) < 1. Zvýšíme proměnnou y2 o θ = (1 – (-2))/3=1 (jediná, se kterou lze pivotovat, shora neomezená (s1 bychom museli snižovat, což nejde)). 

Vyřešíme rovnost pro y2 a eliminujeme y2


N={s1, y2} B={y1, s2, s3}

y2

2y1 - y2 ≥ 0

4 3 2

-y1 + 2y2 ≥ 0

1

y1 + y2 ≥ 2 0

1

2

3

4

y1

Pavel Surynek, 2016


Algoritmus končí, získáme splňující ohodnocení: 

y1  1, y2  1 s1

s3

y1

2/3

-1/3

s2

1

-1

y2

1/3

1/3

2 ≤ s1 (≤ +∞) 0 ≤ s2 (≤ +∞) 1 ≤ s3 (≤ +∞) (-∞ ≤ y1 ≤ +∞) (-∞ ≤ y2 ≤ +∞)

α(s1)=1 α(s2)=1 α(s3)=2 α(y1)=1 α(y2)=1

N={s1, s3} B={y1, s2, y2}

y2

2y1 - y2 ≥ 0

4 3 2

-y1 + 2y2 ≥ 0

1

y1 + y2 ≥ 2 0


1

2

3

4

y1

Pavel Surynek, 2016

Metoda větví a mezí (1) 



Metoda pro řešení celočíselného lineárního programování (ILP). Zde nás zajímá rozhodovací varianta, čili nebudeme mít objektivní funkci. Zadání stejné jako pro obecný simplex (tedy formule lineární aritmetiky), pouze vyžadujeme, aby ohodnocení proměnných byla celá čísla. 





Poznámka: lze snadno podporovat ostré nerovnosti, stačí přičíst či odečíst 1 od konstanty na pravé straně nerovnosti. Definice 11.4 (problém, relaxovaný problém). Mějme systém systém lineárních nerovností S, problém nalezení celočíselného ohodnocení proměnných, které splňuje nerovnosti, nechť je problém. Relaxovaný problém potom je tatáž úloha, ale bez požadavku na celočíselnost ohodnocení, značíme relaxed(S).

Předpokládejme existenci funkce LPfeasible, která rozhoduje splnitelnost pro formuli lineární aritmetiky (vrací dvojici - indikátor splnitelnosti, případně splňující ohodnocení). Lze použít například obecný simplex.


Pavel Surynek, 2016

Metoda větví a mezí (2) 

Na vstupu je formule lineární aritmetiky s celočíselnými proměnnými S.

function FEASIBILITY-BRANCH-AND-BOUND(S): boolean SEARCH-INTEGRAL-SOLUTION(S) Snadno lze dovolit některé proměnné racionální a jiné celočíselné (MIP – smíšení return False celočíselné programování)

procedure SEARCH-INTEGRAL-SOLUTION(S) (satisfiable, α) ← LPfeasible(relaxed(S)) V aktuální větvi není přípustné ohodnocení, tedy ani celočíselné if not satisfiable then return else Celočíselné přípustné ohodnocení if α je celočíselné then abort(True) nalezeno, formule splnitelná, konec. else Proměnná x je ohodnocením let x je proměnní, že α(x)=rZ SEARCH-INTEGRAL-SOLUTION(S ∧ (x ≤ r)) α ohodnocena neceločíselně SEARCH-INTEGRAL-SOLUTION(S ∧ (x ≥ r)) V aktuální větvi není celočíselné řešení 17 / Rozhodovací procedury a verifikace, 11. přednáška

Pavel Surynek, 2016

Metoda větví a mezí – příklad a poznámky 

Příklad: Nechť x1, x2, x3, x4 jsou proměnné formule lineární aritmetiky.   

Předpokládejme, že funkce LPfeasible vrátila řešení (1, 0.7, 2.5, 3) Dále je možno vybrat neceločíselně ohodnocenou proměnnou, v tomto případě buď x2, nebo x3. Nechť byla vybrána x2:  



Algoritmus není úplný, nemusí zastavit.  



Přidá se podmínka x2 ≤ 0 a rekurzivně se pokračuje v řešení, nechť není nalezeno přípustné ohodnocení v této větvi. Přidá se tedy podmínka x2 ≥ 1 a opět se rekurzivně pokračuje v řešení.

Pro formuli lineární aritmetiky: 1 ≤ 3x – 3y ≤ 2 nezastaví (úloha nemá celočíselné přípustné řešení). Lze vyřešit odhadem na velikost domény proměnných:

Tvrzení 11.1 (odhad proměnných): Nechť koeficienty formule φ tvoří matici A typu m × n a vektor b (pravé strany), x1, x2, …, xn nechť jsou proměnné a nechť μ je největší z abs. hodnot koeficientů a abs. hodnot konstant. Potom je-li φ celočíselně splnitelná, existuje celočíselné ohodnocení α, že |α(xj)|≤((m+n)*n*μ)n pro j=1,2,…,n. Bez důkazu.


Pavel Surynek, 2016

Ořezávání pomocí nadrovin (1) 



Ořezávací nadrovina je podmínka, která když se přidá k formuli lineární aritmetiky, nezmění množinu přípustných celočíselných řešení. Ořezávací nadroviny mohou pomoci zmenšit prohledávaný prostor přípustných (neceločíselných) ohodnocení.


Pavel Surynek, 2016


Popíšeme ořezávací nadroviny nazývané Gomoryho řezy, nejdříve příklad: 

Nechť x1, x2, x3 jsou proměnné a nechť dolní meze jsou 1 ≤ x1 a 0.5 ≤ x2, předpokládáme, že konečná tabulka v obecném simplexu obsahuje rovnost: 



Konečné přípustné ohodnocení nechť je: 



α: {x1  1, x2  0.5, x3  1.75}.

Odečteme přípustné ohodnocení od rovnosti:   



x3 = 0.5x1+2.5x2.

x3 – 1.75 = 0.5(x1 – 1) +2.5(x2 – 0.5) x3 – 1 = 0.75 + 0.5(x1 – 1) +2.5(x2 – 0.5) 0.75 + 0.5(x1 – 1) +2.5(x2 – 0.5) ≥ 1

Poslední nerovnost přidáme jako novou podmínku, aktuální ohodnocení α ji nesplňuje, α bude oříznuto.


Pavel Surynek, 2016


Budeme odvozovat řez z rovnosti, ta musí splňovat dvě podmínky:   

(i) Ohodnocení bázických proměnných musí být zlomkové. (ii) Ohodnocení všech nebázických proměnných musí odpovídat jedné z jejích mezí (hodní nebo dolní). Uvažme rovnost: 



(1)

α nechť je ohodnocení nalezené obecným simplexem, tedy: 



xi=∑xjN aijxj, kde xi je bázická proměnná α(xi)=∑xjN aijα(xj)

(2)

Rozdělíme nebázické proměnné podle toho, zda mají přiřazenou hodní nebo dolní mez:  

J = {j| xjN ∧ α(xj) = lj} K = {j|xjN ∧ α(xj) = uj}


Pavel Surynek, 2016


Provedeme odečtení (2) od (1): 



Nechť f0= α(xi) - α(xi), jelikož předpokládáme, že α(xi) není celé číslo, platí, že 0 < f0 < 1, můžeme tedy psát: 

 

xi - α(xi)=∑jJ aij(xj – lj) - ∑jK aij(uj - xj)

xi - α(xi) = f0 +∑jJ aij(xj – lj) - ∑jK aij(uj - xj)

Všimněme si, že levá strana je celé číslo. Nyní rozlišíme dva případy: (a) Když ∑jJ aij(xj – lj) - ∑jK aij(uj - xj) > 0, pak jelikož pravá strana je celé číslo, platí: 

f0 +∑jJ aij(xj – lj) - ∑jK aij(uj - xj) ≥ 1, provedeme rozdělení indexů: J+ = { j |jJ ∧ aij > 0} J- = { j |jJ ∧ aij < 0} K+ = { j |jK ∧ aij > 0} K- = { j |jK ∧ aij < 0}


Pavel Surynek, 2016


Na levou stranu shromáždíme pozitivní členy: 





(b) Když ∑jJ aij(xj – lj) - ∑jK aij(uj - xj) ≤ 0, pak jelikož pravá strana je celé číslo, platí: 





∑jJ- aij(xj – lj) - ∑jK+ aij(uj - xj) ≤ - f0, ekvivalentně také -∑jJ- (aij/f0)(xj – lj) + ∑jK+ (aij/f0)(uj - xj) ≥ 1

Celkem dostáváme, že: 



f0 +∑jJ aij(xj – lj) - ∑jK aij(uj - xj) ≤ 0

Podobně jako v předchozím obdržíme: 



∑jJ+ aij(xj – lj) - ∑jK- aij(uj - xj) ≥ 1 - f0, ekvivalentně také ∑jJ+ (aij/(1- f0))(xj – lj) - ∑jK- (aij /(1- f0))(uj - xj) ≥ 1

∑jJ+ (aij/(1- f0))(xj – lj) -∑jJ- (aij/f0)(xj – lj) + ∑jK+ (aij/f0)(uj - xj) - ∑jK- (aij /(1- f0))(uj - xj) ≥ 1

Nová podmínka zakáže ohodnocení α, jelikož při něm jsou členy na levé straně nulové.


Pavel Surynek, 2016

Diferenční logika (1) 

Rozhodovací procedura pro konjunkci diferenčních podmínek, jedná se o fragment lineární aritmetiky. 

Definice 11.5 (formule diferenční logiky). Nechť Var je množina symbolů pro proměnné, Cons nechť je množina symbolů pro konstanty (VarCons=). Formule diferenční logiky je slovo dané následující gramatikou:    





Počáteční neterminál I, další neterminál A, T Množina terminálů = VarCons {,<,≤,(,)} I  II |(I)| I  A A  T – T < c | T – T ≤ c pro cCons T  v pro vVar

I … odpovídá formuli, A … odpovídá atomu, T … odpovídá termu, který v tomto případě je proměnná.


Pavel Surynek, 2016


Lze modelovat i další podmínky podle následujících pravidel:     



Uvažujme formuli: 



x – y = c lze zapsat jako x – y ≤ c  y – x ≤ -c x – y ≥ c lze zapsat jako y – x ≤ -c x – y > c lze zapsat jako y – x < -c Podmínka s jednou proměnnou jako například x < 5 lze napsat jako x-x0 < 5, kde x0 je nová proměnná (tzv. nulová proměnná). Vyžaduje se, aby hodnota nulové proměnné byla 0. x
Tuto formuli lze přepsat jako formuli diferenční logiky: 

x – y < 5  y – x0 ≤ 4  x – z ≤ -1  z – x ≤ 1


Pavel Surynek, 2016


Podívejme se na rozhodovací proceduru pro diferenční logiku. 



Definice 11.6 (graf nerovností). Nechť δ je formule diferenční logiky ve formě konjunkce nerovností. Potom orientovaný graf s váhami G=(V,E,c) je graf nerovností, jestliže vrcholy odpovídají proměnným a je přítomna hrana e=(x,y) s váhou c(e) pro každou nerovnost x-y≤c(e) ve formuli .

Tvrzení 11.2 (splňování diferenční logiky): Nechť δ je formule diferenční logiky ve formě konjunkce nerovností a nechť G je odpovídající graf nerovností. Potom δ je splnitelná, právě když G neobsahuje negativní cyklus. 

Důkaz: Použijeme Bellman-Fordův algoritmus pro nalezení nejkratších cest grafu.


Pavel Surynek, 2016

Předzpracování pro neceločíselné formule 

Dva jednoduché způsoby předzpracování vstupní formule (konjunkce podmínek): 

1. Uvažujme formuli lineární aritmetiky:  





x1 + x2 ≤ 2 ∧ x1 ≤ 1 ∧ x2 ≤ 1, zde vidíme, že první podmínka je redundantní. Obecně: ve formuli a0x0 + ∑j=1n ajxj ≤ b ∧ ∧j=0n(lj ≤ xj ≤ uj) je podmínka a0x0 + ∑j=1n ajxj ≤ b redundantní, jestliže: ∑j|aj>0 ajuj + ∑j|aj<0 ajlj ≤ b. Jinými slovy, když při dosazení extrémních hodnot proměnným součet nepřevýší konstantu b, pak ani pro jiné přípustné ohodnocení proměnných nepřevýší konstantu b.

2. Uvažujme formuli lineární aritmetiky:  

2x1 + x2 ≤ 2 ∧ x2 ≥ 4 ∧ x1 ≤ 3, zde je vidět, že z první a druhé nerovnosti plyne x1 ≤ -1. Obecně: když a0 > 0, pak x0 ≤ (b - ∑j|j>0 ∧ aj>0 ajlj - ∑j|aj<0 ajuj) / a0, podobně, když a0 < 0, pak x0 ≥ (b - ∑j|aj>0 ajlj - ∑j|j>0 ∧ aj<0 ajuj) / a0


Pavel Surynek, 2016

Předzpracování pro celočíselné formule 

Používají se dvě jednoduché úpravy: 

V každé podmínce vstupní formule nejprve vynásobíme všechny koeficienty a konstanty podmínky nejmenším společným násobkem jmenovatelů všech koeficientů a konstant podmínky. 



Poté je možné zavést neostré nerovnosti místo ostrých: 



Obdržíme formuli, kde všechny konstanty a koeficienty jsou celočíselné (předpokládá racionální konstanty a koeficienty ve vstupním zadání). Podmínka ∑i=1n aixi < b může být nahrazena podmínkou ∑i=1n aixi ≤ b – 1.

Speciální případ představují 0-1 formule (proměnné mohou nabývat hodnoty 0 nebo 1):  

Uvažujme formuli: 5x1 – 3x2 ≤ 4, z této podmínky lze odvodit, že x1=1  x2=1, tedy můžeme přidat podmínku x1≤ x2. Uvažujme formuli: x1 + x2 ≤ 1 ∧ x2 ≥ 1, z podmínek lze odvodit x1=0.


Pavel Surynek, 2016

Rozhodovací procedury a verifikace Pavel Surynek, KTIML

Recommend Documents