변수에 많은 제약이 있으며이 제한된 공간을 효율적으로 샘플링 할 방법을 찾고 있습니다. 나는 Z3을 시험해 보았다. 그리고 그것이 공간이 사소한 지 (즉, 제약이 만족 스럽다면) 말할 수있을 것 같다. 그러나 나는 공간에서 예제를 얻는 방법을 보지 않는다. 내가 최소화하거나 최대화하지 않는 한. .제한된 공간에서 샘플링하기 위해 Z3 사용하기
나는 뭔가를 놓치고 있습니까, 아니면 Z3이 아닌 것입니까?
Z3은 모델을 제공 할 수 있습니다. 즉, 제약 조건을 충족하는 변수에 대한 할당의 한 예입니다 (.NET API의 SMT2 또는 Solver.Model (및 다른 API의 이름이 비슷한 것과 비슷 함) (get-model) 명령을 사용하십시오) . 그런 다음 모델의 부정을 선언하여 해석자가 다음 쿼리에 대해 다른 할당을 생성하도록 할 수 있습니다. 이러한 종류의 구성표는 많은 응용 프로그램에서 사용되지만 반드시 "효율적"이라고는 할 수 없지만 실제로 어떤 종류의 샘플링을 수행 할 것인가에 달려 있습니다 (예 : Z3 모델이 검색 공간에 임의로 배포되지 않음).
예, 무작위 샘플링을 찾고있었습니다. 나는 다른 것을 사용해야 할 것이다. 어떤 제안? – syzygy
유클리드 거리 (euclidean distance)에 관한 전략을 사용하려고 생각했습니다. 첫 번째 점을 생성 한 후 상수와 기존 솔루션 간의 거리를 최대화하기위한 최적화를 시작하십시오. 나는 자바 스택에 https://www.github.com/groostav/sojourn-cvg에서 이것을하기를 바라고있다. 문제는 말입니다 : SMT2 리스프와 같은 것이 자바 API보다 훨씬 좋네요. 탐색하는데 문제가 있습니다. 그 결과는 느릴 수 있지만 실현 가능한 지역 주변에 일종의 완전한 요인 테두리 상자를 만들 수 있기를 바랄뿐입니다. 균일 분포는 아니지만 나에게 충분합니다. – Groostav