앉은 문제를 줄이기위한 알고리즘이 있습니까?만족도를 줄이기위한 알고리즘
만족 성은 주어진 부울 수식의 변수가 수식을 TRUE로 만드는 방식으로 할당 될 수 있는지를 결정하는 문제입니다. 똑같이 중요한 것은 그러한 할당이 존재하지 않는지를 결정하는 것인데, 이는 공식에 의해 표현 된 함수가 가능한 모든 변수 할당에 대해 똑같이 거짓임을 암시합니다. 후자의 경우 우리는 그 기능이 만족스럽지 않다고 말할 것이다. 그렇지 않으면 만족할 만하다. 이 문제의 이진 특성을 강조하기 위해 종종 불리언 또는 명제적 만족 가능성이라고합니다. 속기 "SAT"는 또한 함수 및 변수가 모두 2 진 값이라는 암묵적인 이해와 함께이를 나타 내기 위해 일반적으로 사용됩니다.
나는 이것을 해결하기 위해 유전 알고리즘을 사용했지만, 먼저 감소시키는 것이 더 쉽습니다.
당신은 아마 "경로"를 식별하는 공식에 깊이 우선 경로 트리 검색을 할 수있는Reduced Order Binary Decision Diagrams (ROBDD)을 살펴보십시오. 부울 식을 축소 된 표준 형식으로 압축하는 방법을 제공합니다. BDD 축소를 수행하는 데는 많은 소프트웨어가 있습니다. ROBDD에 대한 위키피디아 링크에는 기사 하단의 다른 관련 패키지에 대한 외부 링크 목록이 포함되어 있습니다.
- 즉, (ICanEat & & (IHaveSandwich || IHaveBanana))에 대한 "ICanEat"는 값, 거짓이면 대괄호는 중요하지 않으며 무시할 수 있습니다. 그래서, 바로 가장자리와 노드를 버릴 수 있습니다.
이 깊이 우선 검색을 생성하는 동안 현재 노드가 참으로 확인되면 솔루션을 찾았습니다.
정확하게 "축소"란 무엇을 의미합니까? 사전에 일종의 사전 처리를 의미한다고 가정하고, 일부 변수 나 절을 먼저 없애거나 단순화 할 것입니다.
모두 작업량에 따라 다릅니다. 완료 될 때까지 unit propagation을해야합니다. 당신이 할 수있는 다른 비싼 것들이 있습니다. 몇 가지 예는 march_dl 페이지의 사전 처리 섹션을 참조하십시오.