1
는 의사 부울 문제에 대한 솔루션 (또는 할당)을 찾을 솔버 효율적 SMT 수 사용될 수있다 Int 유형의 가중치입니다.은 SMT/Z3 optimazation
사용자의 편의를 위해 페이지 1과 3의 내용을 강조하여 의사 불리언 문제 을 지정하기에 충분합니다.
A
답변
3
SMT 솔버는 대개 이론적 인 공식을 사용합니다. 선택적으로 기본 이론의 함수와 술어 (예 : 산술 이론, 비트 벡터 이론, 배열)를 사용하면 수식이 만족 스러운지 아닌지를 알 수 있습니다. 그들은 대개 객관적인 기능을 지정하기위한 방법을 공개하지 않습니다. 일반적으로 기본 제공 최적화 절차가 없습니다.
특수한 경우 중 일부는 부울을 사용하거나 부울 및 비트 벡터 또는 정수 중 하나만 사용하는 수식입니다. 의사 부울 제약 조건은 비트 벡터를 사용하여 정수로 인코딩되거나 인코딩 (오버 플로우 의미를 고려하여 일부주의)하거나 SAT로 직접 인코딩 할 수 있습니다. psuedo-boolean 문제의 클래스에 속하는 제한된 정수를 사용하는 일부 수식의 경우 Z3은 비트 벡터로 자동 축소를 시도합니다. 이것은 QF_LIA로 태그 지정된 SMT-LIB2 형식의 benchmkars에만 적용되거나 명시 적으로이 축소를 수행하는 전술 ("qflia"전술 적용)이 적용되는 경우에 적용됩니다.
Z3은 객관적인 기능을 직접 노출시키지 않지만 객관적인 기능을 가진 SMT 해결자를 늘리는 질문은 연구 커뮤니티에서 적극적으로 추구됩니다. SAT 2006에서 Nieuwenhuis와 Oliveras가 제안한 한 가지 접근 방식은 사용자 지정 이론 인 "가중치 최대 SMT"문제를 해결하기 위해 을 구축하는 것이 었습니다. Yices에는 가중치가 적용된 SMT에 대한 기능이 내장되어 있지만 Z3에는 포함되지 않지만 가중치가 적용된 최대 SMT 솔버의 역 추적 검색을 수행하는 사용자 정의 이론을 작성할 수는 있지만 나중에는 을 사용하지 않아도됩니다.
때때로 사람들은 정량화 된 수식을 사용하여 목적 함수를 지정하려고합니다. 이론에서는 수량 한정자 제거 절차가 을 객관식으로 해결할 수 있기를 기대할 수 있습니다. 성능에 있어서는 일반적으로 상당히 나쁩니다. 한정어 제거 은 과장이며 루틴은 효율적이지 않습니다.
관련 문제