avamingli commented on PR #1762: URL: https://github.com/apache/cloudberry/pull/1762#issuecomment-4818483941
> ### 1. CTE Predicate Pushdown via OR Collection and CNF Conversion > Checked the 1st commit [7f13fc4](https://github.com/apache/cloudberry/commit/7f13fc4fa537b7a96cbb156c74c719eb45092d5a) for correctness - all Ok, the code is correct. > > The only flaw is in example T10 we have (A OR NOT(A)) predicate - could exclude it, but I think it's not the current implementation task - exclude tautology. > > What I checked. The focus was on function `convert_expr_to_cnf_complete`. We transform logical expression to simplified form, lets check the original equation and transformed one. The only known for me method is https://en.wikipedia.org/wiki/Karnaugh_map So we have the original expression, lets create Karnaugh map for it, then transform expression, again create Karnaugh map, compare maps, and also check if the transformed equation the same we could generate using rules for Karnaugh map. > > To do so I generate python code based on `prepqual.c`, manually checked generated code for correctness, and then launch code and see the results. @leborchuk Thank you for the rigorous review and the Karnaugh-map verification! Really appreciate the depth here. The conversion is verified in 2-valued logic, which is exactly right. The reason I deliberately keep `(A OR NOT A)` instead of eliminating it as a tautology is SQL's 3-valued logic: `A OR NOT A` is **not** always TRUE — when `A` is NULL it evaluates to NULL. And here `A` is a general operator expression, not a single column, so I can't fall back on a column-level NOT NULL constraint to recover the law of excluded middle. Eliminating it would only be safe under a *proven* NOT NULL on `A`, which for a general expression I don't have. (PostgreSQL's own const-folding keeps it for the same reason.) A quick reproduction anyone can run: ```sql -- ============================================================ -- (A OR NOT A) is NOT always TRUE in SQL's 3-valued logic, -- so eliminating it as a tautology can change query results. -- ============================================================ -- Part 1: truth table of (A OR NOT A) for a boolean A, including NULL SELECT a, (a OR NOT a) AS "a OR NOT a", (a OR NOT a) IS TRUE AS "passes a WHERE?" FROM (VALUES (true), (false), (NULL::bool)) v(a); -- Part 2: effect on a real query result. -- A is a general operator expression (x > 5), NOT a bare nullable column. DROP TABLE IF EXISTS aornota_demo; CREATE TABLE aornota_demo (id int, x int, b bool); INSERT INTO aornota_demo VALUES (1, 10, true), -- A = (x>5) = TRUE (2, NULL, true), -- A = (x> (3, 3, true); -- A = (x>5) = FALSE -- (a) keep the tautology clause (what the CNF conversion produces): SELECT count(*) AS kept_A_OR_NOTA FROM aornota_demo WHERE ((x > 5) OR NOT (x > 5)) AND b; -- (b) drop it as a "tautology" (the suggested simplification) SELECT count(*) AS dropped FROM aornota_demo WHERE b; -- per-row view: row id=2 (x IS NULL) flips reject -> accept SELECT id, x, ((x > 5) OR NOT (x > 5)) AS "A OR NOT A", (((x>5) OR NOT (x>5)) AND b) IS TRUE AS kept_passes, (b) IS TRUE AS dropped_passes FROM aornota_demo ORDER BY id; DROP TABLE aornota_demo; ``` Output (standard SQL 3-valued logic): ``` a | a OR NOT a | passes a WHERE? ---+------------+----------------- t | t | t f | t | t | | f <- A IS NULL: (A OR NOT A) is NUL kept_a_or_nota -- WHERE ((x>5) OR NOT(x>5)) AND b ---------------- 2 dropped -- WHERE b (tautology eliminated) --------- 3 id | x | A OR NOT A | kept_passes | dropped_passes ----+----+------------+-------------+---------------- 1 | 10 | t | t | t 2 | | | f | t <- flips reject -> accept 3 | 3 | t | t | t ``` 2 rows vs 3 rows: the `x IS NULL` row flips from rejected to accepted once the clause is dropped. So that clause isn't redundant — it carries predicate's NULL-rejection into the CNF. Side note: I actually tried a Karnaugh-map based approach during development but dropped it — every nested step had to allocate a lot of space mostly discarded during dedup, so I went with the recursive distributive-law method instead. Your verification on top of it is a great cross-check. Thanks again! -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected] --------------------------------------------------------------------- To unsubscribe, e-mail: [email protected] For additional commands, e-mail: [email protected]
