가장 작은 독립 세트

집합이 주어진 경우, 최소 수식 s'이 s이고 모든 수식이 s임을 의미합니다. 나는 s을 가장 작은 독립 세트라고 부르며, 모든 쌍의 경우 a,b은 s'이고, a은 b을 의미하지 않으며 그 반대의 경우도 마찬가지입니다.가장 작은 독립 세트

순진한 접근 방식은 복잡하다고 생각합니다. O(2^|s|)입니다. 더 효율적인 방법이 있습니까? 이 문제는 현재 smt/sat 솔버 (예 : unsat 코어)를 활용하는 방법으로 인코딩 될 수 있습니까?

출처

2012-10-07 Vu Nguyen

저는 Z3을 사용할 수 있다고 생각합니다. [Array and Bags] (http://rise4fun.com/z3/tutorialcontent/guide#h26)의 유스 케이스처럼 보입니다. 그러나 Z3은 런타임 복잡성에 대한 정보를 제공하지 않습니다. 또한, 문제가 있기 때문에, 주어진 상황 (그리고 일반적인 경우가 아니라)에 대해서만 문제를 해결할 수 있습니다. 개인적으로 Z3보다 [합금] (http://alloy.mit.edu/alloy/)에 문제를 적어 두는 것이 더 쉽습니다. –

어쩌면 너무 늦었을 수도 있습니다. 그러나 당신은 1 루프에 의해 그러한 세트를 계산할 수 있습니다.

IS = F1 // first formula in s 
for each formula Fi in {F2,..Fn} in s 
    if ((not IS) AND Fi) is UNSAT 
    IS = IS AND Fi

세트 IS에는 독립 세트가 들어 있습니다.

출처

2014-06-09 05:54:50 qsp

이것은 독립적 인 집합을 계산하지만 반드시 가장 작은 집합을 계산하지는 않습니다. – CliffordVienna

답변

관련 문제