MAX-SAT 용 Z3 활용 관련 문제

Question

MAX-SAT에 관심이 있으며 Z3에 내장 기능이 포함되기를 기대하고있었습니다. 가까운 장래에이 일을 할 계획이 있습니까?

위의 내용이 없으면 명령 줄에서 예제 maxsat 응용 프로그램을 사용해 보았습니다. 불행히도 exec.sh "filename.z3"을 수행 할 때마다 항상 다음과 같은 응답을 얻습니다. "하드 제한 조건이 만족 스러운지 확인하는 중 ... 결과 : 0". 내가 도대체 ​​뭘 잘못하고있는 겁니까? 이 응답은 파일의 실제 내용과는 완전히 독립적 인 것으로 보입니다.

마지막으로 maxsat 예제의 주석은 제약 조건을 하드 또는 소프트로 표시하는 방법을 명확하게 지정하지 않았습니다. 하드 제약은 수식과 소프트 제약으로 앞에 오는 수식으로 가정됩니다 : 가정. 그러므로 "(assert (> x 0))"을 부드럽게 표시하려면 정확히 ": assumption"을 어디에 두어야할까요? (하드 및 소프트 제약 조건에 대한 질문을 읽었지 만 만족할 수없는 수식의 "최대 만족 코어"와 달리 만족할만한 코어를 찾는 맥락에서 질문/응답이 더 많은 것처럼 보였습니다.)

Answer 1

MaxSAT 예제 Z3 배포판에서 Z3 API를 사용하여 두 개의 MaxSAT 알고리즘을 구현하는 방법을 보여줍니다. 이 예에서는 구속 조건을 유지하는 데 이전 API (사용되지 않음)를 계속 사용하지만 새 solver API를 사용하도록 쉽게 수정할 수 있습니다. 예제 응용 프로그램은 SMT 1.0 파일을 읽습니다. 그러나 C API를 사용하여 작성된 수식에는 MaxSAT 함수를 사용할 수 있습니다. 이 스크립트에서는 :assumption 필드가 소프트 제약 조건이고 :formula 필드는 어려운 조건이라고 가정합니다. 여기에 작은 예제가 있습니다. (> x 0), (> y 0), (< x y) 및 (> x (- y 1))은 소프트 제한이고 (> (+ x y) 0)과 (< (- x y) 100)은 어려운 것입니다. 예제 응용 프로그램은 3을 반환합니다. 즉, 최대 3 개의 소프트 제약 조건이 충족 될 수 있습니다.

(benchmark ex 
    :extrafuns ((x Int)) 
    :extrafuns ((y Int)) 
    ;; Soft Constraints 
    :assumption (> x 0) 
    :assumption (> y 0) 
    :assumption (< x y) 
    :assumption (> x (- y 1)) 
    :formula 
    (and 
    ;; Hard Constraints 
    (> (+ x y) 0) 
    (< (- x y) 100) 
)) 

그렇다면 MaxSAT를 Z3 API에서 직접 지원할 계획이 없습니다. 이후 버전에서는 MaxSAT 예제를 다른 API (.NET, Python 및 C++)로 이식 할 수 있습니다.