일반적으로 술어를 결합하고 최적화하는 방법은 무엇입니까?

복잡한 이벤트 처리 시스템에서 일부 작업을하고 있습니다. 쿼리 언어를 사용하여 해당 레코드의 멤버를 기반으로 레코드 집합을 필터링 할 수 있습니다. 이 언어는 임의 구성원에 대한 논리 연산자, 산술 연산자 및 사용자 정의 연산자를 지원합니다.일반적으로 술어를 결합하고 최적화하는 방법은 무엇입니까?

다음은 지원되는 쿼리의 예 :

(MemberA > MemberB) && 
(@in MemberC { "str1", "str2" }) && 
(com.foo.Bar.myPred(MemberD, MemberE))

내 문제는 내가 한 슈퍼 쿼리에 쿼리를 결합하려는 것입니다, 그리고 나는 해고, tautologies와 모순을 제거하는 슈퍼 쿼리를 최적화 할 수 있습니다. 예 : 나는 아주 쉽게되는

A > 0

을 가지고

A > 1

와 결합 할 :

A > 0 || A > 1

하지만 나는 그것이

A > 0

을 줄일 수 있도록 최적화 할

디스크가있는 URL이나 책이있는 경우 우리는이 일반적인 주제에 대해 알고있을 것입니다.

출처

2009-09-21 Anonymous

도서? 나는 약간이 있다고 생각한다; 이 영역에서 기사를 찾아보아야 할 가능성이 큽니다.

귀하의 도메인은 귀하의 도메인에서 작동 할 수있는 SMT solvers입니다. 표현식 언어의 수학적 정의, 당신이 지원하는 관계의 공리를 제공합니다. 그렇다면 예를 들어, 하나의 술어가 다른 술어를 암시하는지 여부 (예, 2 개의 등가 결합)가 동질화 문제 (tautology)인지 여부를 판단 할 수 있습니다.

이 작업에 대한 자동화 된 솔루션은 모호하며 때로는 튜링 기계 (컴퓨터)의 이론적 기능을 뛰어 넘을 수도 있습니다. 문제에 대한 유일한 해결책은 없습니다.

출처

2009-09-21 15:56:53

감사 파벨. 필자의 생각은 완전히 최적의 솔루션은 다루기 힘들지만 한정된 기간에 적절한 최적화를 수행 할 수 있어야한다는 것입니다. SMT는 그 (것)들을 지적을위한 감사합니다, 그러나 나는 당신의 응답에서이 문장을 이해하는 데 어려움을 겪고 있습니다. "예를 들어, 하나의 술어가 다른 것을 의미하는지 (예, 2 개의 등가 결합)가 동어 반복 ", 분명히 할 수 있니? –

@Bill : 명확하게. 당신의 예제에서, 당신은'A> 0 '에 의해 함축되어 있기 때문에 술어'A> 1'을 버려야합니다. 나는. 'A> 1 '이 참인 모든 경우에'A> 0'도 참입니다 (함축적이라고 함). SMT 솔버가 공식 산술적 공리를 업로드했다고 가정하면, 공식 (A> 0)이 의미하는 바는 (A> 1)은 동어 반복이다. 이 추론을 한 후에는 표현식에서'A> 0'을 철회 할 수 있습니다. 그러나 이것은 SMT 솔버의 많은 어플리케이션 중 하나 일 뿐이며, 당신이 당신의 질문에 그것을 사용했기 때문에 그것을 요약했습니다. –

좋아, 그 말이 맞는, 파벨 고마워. –

일반적으로 술어를 결합하고 최적화하는 방법은 무엇입니까?

답변

관련 문제