2
z3에서 random-seed 옵션을 사용하는 것은 무엇입니까? 임의의 모델을 생성하는 데 사용할 수 있습니까? 이 게시물 Z3: Offering random solutions in solving에서 LIA는 임의 모델을 가질 수 없다고 언급합니다. 그렇다면 우리는 왜 무작위로 씨앗이 필요한가?Z3에서 무작위 시드 사용
A
답변
2
임의 시드를 사용하여 SMT 코어에서 명제 변수 선택 추론을 제어 할 수 있습니다. SAT 검색 구성 요소의 성능이 수식의 작성 순서와 관계없이 안정적인지 여부를 확인하기 위해 임의의 시드를 사용할 수 있습니다.
관련 문제
- 1. 파이썬 : 무작위 시드 문제
- 2. 시드 무작위 플로팅 2d 그리드
- 3. C# 무작위 인스턴스의 시드 결정
- 4. Z3에서 정렬 사용
- 5. 100M 행 관계 테이블 대신 시드 된 무작위 시퀀스 사용
- 6. C++ 무작위 시드, 전역 개체 및 SDL_Threads
- 7. Shuffle 함수의 SystemVerilog 배열 무작위 시드
- 8. Pickadate 시드 시드 다른 시드
- 9. Z3에서 Skolemization
- 10. Z3에서 대체
- 11. MiniTest : 테스트 내부의 시드 사용
- 12. `RANDOM_NUMBER` 알고리즘에서 특정 시드 사용
- 13. 외래 키 시드 시드
- 14. PHPUnit에서 별도의 시드 시드
- 15. Laravel 4의 패키지 테이블 시드 시드
- 16. 시드 문자열
- 17. 레일 시드 데이터 시드 위치
- 18. Java에서 보안 난수 시드 시드
- 19. Z3에서 참조 카운팅 유지
- 20. z3에서 멤버십 관계 설정
- 21. Z3에서 배열 선언
- 22. Z3에서 귀납적 사실 증명
- 23. Z3에서`simplify` 전술 조정하기
- 24. Z3에서 나누기위한 버그입니까?
- 25. Z3에서 최적화 : 엡실론 제거
- 26. Z3에서 주입 함수 정의하기
- 27. Z3에서 Craig 보간 지원
- 28. Z3에서 모델링 배열 지정
- 29. for all의 z3에서 Simplex
- 30. Java의 난수 생성기에 특정 시드 사용
답변 감사합니다 Nikolaj. 한가지 확실한 것은, 우리가 랜덤 모델을 얻을 수 없다는 것입니다. 그러나 비트 벡터의 경우 위상 선택이 어떻게 작동하며 서로 다른 임의의 시드를 사용하여 실행할 때마다 서로 다른 모델을 얻을 수 있습니다. 또한 Z3이 수용 할 수있는 임의의 시드 값의 범위는 무엇입니까? – Shambo