Z3 SAT 솔버의 랜덤 시드

Question

CNF/DIMACS 형식으로 인코딩 된 까다로운 적합성 문제에 대해 Z3을 SAT solver으로 사용하고 있습니다.

이 해결책 찾을 수있는 기회를 높이기 위해 입력을 랜덤 나을 :

• 가 CNF 조항의 순서를 섞어서
• 정렬/입력의 번호 셔플 변수를

에 대한 측정 (솔버와 정렬 모드 당 100 번 테스트) Z3, Cryptominisat 및 Clasp :

Z3를 들어, 아마 대표하지 않습니다 내 예를 들어 약속 보이지 않는/무작위 분류.

Z3의 SAT 모듈에 영향을 미치는 임의 시드 커맨드 라인 매개 변수를 찾지 못했습니다. "random_seed"매개 변수 만 SMT 해석기를 제어하는 ​​것처럼 보입니다.

Answer 1

당신은 훌륭한 지적을합니다 : sat 솔버가 사용하는 임의의 시드는 다른 모듈과 같은 방식으로 노출되지 않습니다. sat 솔버의 매개 변수를 업데이트하여 불안정한 분기를 업데이트했습니다. 이제 sat 매개 변수의 일부로 명령 줄에서 무작위 시드를 설정할 수 있습니다. 이게 도움이 되길 바란다.