임의의 명제식에서 변수의 상한/하한 결정

Question

임의의 명제식 PHI (일부 변수의 선형 제약)가 주어지면 각 변수의 (대략적인) 상한 및 하한을 결정하는 가장 좋은 방법은 무엇입니까?

일부 변수는 제한되지 않을 수 있습니다. 이 경우 알고리즘은 해당 변수에 대한 상한/하한이 없음을 결정해야합니다.

예 : PHI = (x = 3 AND y> = 1). x의 상한과 하한은 모두 3입니다. y의 하한은 1이고 y는 상한을 갖지 않습니다.

이것은 매우 간단한 예이지만 일반적으로 (아마도 SMT 해결사를 사용하는) 해결책이 있습니까?

Answer 1

각 변수의 SAT/UNSAT 도메인이 연속적이라고 가정합니다.

1. 수식에 대한 솔루션을 확인하려면 SMT 솔버를 사용하십시오. 솔루션이 없다면 상한선이나 하한선을 의미하지 않으므로 중지하십시오.
2. 수식의 각 변수에 대해 변수 도메인에서 두 개의 이진 검색을 수행합니다. 하나는 하한을 검색하고 다른 하나는 상한을 검색합니다. 각 변수를 검색 할 때의 시작 값은 1 단계에서 찾은 해의 변수 값입니다. SMT 솔버를 사용하여 각 검색 값의 적합성을 조사하고 각 변수의 경계를 체계적으로 괄호로 묶습니다.

검색 기능을위한 의사 코드를 가정 정수 도메인 변수 :

lower_bound(variable, start, formula) 
{ 
    lo = -inf; 
    hi = start; 
    last_sat = start; 
    incr = 1; 
    do { 
     variable = (lo + hi)/2; 
     if (SMT(formula) == UNSAT) { 
      lo = variable + incr; 
     } else { 
      last_sat = variable; 
      hi = variable - incr; 
     } 
    } while (lo <= hi); 
    return last_sat; 
} 

및

upper_bound(variable, start, formula) 
{ 
    lo = start; 
    hi = +inf; 
    last_sat = start; 
    do { 
     variable = (lo + hi)/2; 
     if (SMT(formula) == SAT) { 
      last_sat = variable; 
      lo = variable + incr; 
     } else { 
      hi = variable - incr; 
     } 
    } while (lo <= hi); 
    return last_sat; 
} 

-INF/+ INF는 최소/최대 값은 각각의 영역에서 표현할 수있다 변하기 쉬운. lower_bound가 -inf를 리턴하면 변수는 하한을 갖지 않습니다. upper_bound가 + inf를 반환하면 변수는 상한을 갖지 않습니다.

Answer 2

실제로 대부분의 최적화 문제는 SMT 솔버 상단에 일종의 반복/최대/최소 종류의 외부 드라이버가 필요합니다. SMT 솔버의 특정 기능을 활용할 수있는 정량화 된 접근법도 가능하지만 실제로 이러한 제약은 근원적 인 솔버에게는 너무 어려워집니다. 특히이 토론을 참조하십시오 : How to optimize a piece of code in Z3? (PI_NON_NESTED_ARITH_WEIGHT related)

대부분의 고수준 언어 바인딩에는 삶을 단순화하는 데 필요한 기계가 포함되어 있습니다. 당신이 스크립트 Z3에 하스켈 SBV 라이브러리를 사용하는 경우 예를 들어, 당신은 할 수 있습니다 :

Prelude> import Data.SBV 
Prelude Data.SBV> maximize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1] 
Prelude Data.SBV> maximize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Nothing 
Prelude Data.SBV> minimize Quantified head 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1] 
Prelude Data.SBV> minimize Quantified (head . tail) 2 (\[x, y] -> x.==3 &&& y.>=1) 
Just [3,1] 

첫 번째 결과 상태 X = 3, y는 술어의 X == 3 & & Y에 대한 1 극대화의 X를 = > = 1. 두 번째 결과는 같은 술어와 관련하여 y를 최대화하는 값이 없음을 나타냅니다. 세 번째 호출은 x = 3, y = 1은 x에 대한 술어를 최소화합니다. 네 번째 호출에서 x = 3, y = 1이라고하면 y에 대한 조건부가 최소화됩니다. (자세한 내용은 http://hackage.haskell.org/packages/archive/sbv/0.9.24/doc/html/Data-SBV.html#g:34을 참조하십시오.)

한정 기호 대신 반복 옵션을 사용하여 라이브러리에서 반복 최적화를 수행 할 수도 있습니다 (Quantified 대신).이 두 기법은 이 아니고,은 로컬 minima/maxima에서 달라 붙을 수 있지만, 반복적 접근법은 정량화 된 버전이 SMT 해석기에서 처리하기에는 너무 많은 문제를 해결할 수 있습니다.