명제변항이 n개면 interpretation은 2^n개고 그러면 명제함수의 종류는 2^2^n개가 되는데...압축해서 표현하면서도 논리적 관계사(not, and만 있으면 충분할 것 같음)를 적용하는 걸 각 표현에 직접할 수 있도록 하는 방법이 없을까요?

truth table을 나열해놓는 건 당연히 너무 크기가 커서 안 되겠고...CNF는 not을 적용할 때 크기가 폭발적으로 증가할 때가 있기도 하고 tseytin transformation을 쓴다고 해도 여전히 큰 것 같습니다. ANF는 명제함수가 복잡해질수록 크기가 커져서 나중에 논리적 관계사를 적용할 때 시간이 오래 걸려서 안 될 것 같습니다.

정 안 되면 그냥 부정확함을 감수하고 word embedding식으로 명제함수를 벡터공간에 놓을 생각입니다.

궁극적인 목적은 주어진 논리식을 참으로 만드는 해를 찾는 것입니다. 그렇게 하기 쉬운 표현법이 뭐가 있을지, 그리고 그 표현법상에서 논리적 관계사를 잘 적용할 수 있을지...

truth table로 표현했을 때 가장 메모리가 크겠지만 논리적 관계사를 적용하는 건 간단한 상태인데, 그러면 논리적 관계사 적용을 살짝 복잡하게 하더라도 메모리를 상당히 줄일 수 있는 방법은 없을지 고민을 하고 있습니다.