1
전적으로 Z3 전용 시스템을 설정하고 싶습니다. 4 개의 코어가 있고 머신의 모든 힘을 사용하고 싶다고합시다.멀티 코어 서버에서 Z3 사용
약 1000 개의 증분 어설 션이있는 큰 수식을 해결할 것입니다.
나는이 수식을 병렬 방식으로 풀고 싶습니다. this question을 읽었으며 수식 문제를 해결할 때마다 고유 한 Context을 만들어야합니다.
그럼 내 질문에 전체 시스템 리소스 (4 코어)를 사용하고 점진적 어설 션을 사용하여 수식을 해결하는 가장 좋은 방법은 무엇입니까? 코어 당 컨텍스트를 만들어야하고 수식을 점진적으로 해결하기 위해 푸시와 팝을 동기화해야합니다. 하나의 컨텍스트를 통해 생성
감사
"최적의"방법이 없다고 생각합니다. 문제를 해결하는 데 정말로 달려 있습니다. API를 사용하는 경우 모든 스레드/프로세스에 별도의 컨텍스트를 사용해야합니다. 스레드/프로세스 당 둘 이상의 컨텍스트가있는 좋은 이유가 있다고 생각하지 않습니다. –
그러면 코어 당 컨텍스트를 만들 수 있습니까? 각 컨텍스트가 다른 코어를 사용합니까? 4 개의 컨텍스트가 중복 된 정보를 4 번 (코어 당 1 개) 갖는 것을 의미하는 점진적으로 해결 될 1000 개의 어설트가 있기 때문에. 그게 맞습니까? 모든 컨텍스트에서 모든 주장을하는 것보다 더 나은 방법이 있습니까? 고마워요 @ChristophWintersteiger – user1618465