sat

    0

    1답변

    일부 저널에 WSAT (Walking SAT) 알고리즘은 SAT 문제 해결에 Simulated Annealing 알고리즘보다 우수한 성능을 제공합니다. 제 질문은 누군가가 친절하게 왜 우리가이 결과를 얻었는지 설명 할 수 있습니까? SA가 범용 알고리즘과 비슷하기 때문일 수 있습니까? 편집 : Here 어쩌면 내가 읽어 가장 관련 문서.

    1

    1답변

    내가 근무하는 회사에서 여러 SAT 솔버에 액세스 할 수 있습니다. 각 SAT 솔버가 Z3 SMT 솔버의 성능에 어떤 영향을 주는지 분석하고 싶습니다. Z3에서 외부 SAT 솔버를 호출 할 수 있습니까? 그렇지 않은 경우 외부 솔버를 호출하도록 Z3을 수정해야합니까?

    1

    1답변

    이 문제에 대해 많은 상충되는 정보가 있습니다. 일부 말하기 사이트에서는 NP 완성형이며 다른 사람들은 그것이 공동 NP 완료 형이라고 말합니다. 내가 찾을 수있는 진정한 일관성있는 정보는 확실히 NP 하드입니다. 무엇 이니? 그리고 왜?

    1

    1답변

    정의 SAT2016 = {\ phi | \ phi는 최대 2016 개의 절이있는 CNF 공식}입니다. P \ neq NP라고 가정하면 SAT2016 NP가 완성 되었습니까? 각 절의 리터럴 수는 한정되어 있지 않으므로 절 수에 상수가있는 수식의 적합성을 검사하는 다항 시간 알고리즘이 있는지 여부가 즉시 명확하지 않습니다. 귀하의 아이디어를 환영합니다.

    1

    2답변

    숫자가 포함 된 .cnf 파일에 Conjunctive Normal Form이 있습니다. 색인으로 작업 할 수 있도록 데이터 구조 (행렬 또는 목록)에 읽고 저장해야합니다. (3-SAT 문제를 해결하려면이 코드가 필요합니다.) 어떻게하면 Java로 읽고 저장할 수 있습니까? 새들 - 뷰 관점에서 c This Formular is generated by mcn

    0

    1답변

    어쩌면이 사이트의 범위를 벗어난 것일 수도 있지만, 여기에 충분한 사람들이 이것을 알게되어서 내가 그 장면을 제공하고 있다고 생각했습니다. 내가 3-CNF 조항 의 집합을 말해봐 S = {Clause1, Clause2} = {<x1 or x2 or not x3>, <x4 or x5 or x6>} {0,1} S를 위해 얼마나 많은 만족스러운 과제가 이상