Conjunctive query evaluation is NP-complete
Lax420092.EvaluationNPComplete · concepts/Lax420092/EvaluationNPComplete.lean · lax-420092
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Boolean conjunctive query evaluation, in combined complexity, is NP-complete in the sense of the NP core: it is definable in existential second-order logic, guessing the valuation, and 3-colorability reduces to it by a quantifier-free first-order reduction, the query of a graph being evaluated in the triangle. This is the evaluation half of Chandra and Merlin (1977).
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax904597.Problems |
| 2 | import Lax904597.Interpretations |
| 3 | import Lax904597.Classes |
| 4 | import Lax799700.Problems |
| 5 | import Lax420092.QueryDatabases |
| 6 | import Lax420092.Evaluation |
| 7 | import Lax420092.QueryPairs |
| 8 | import Lax420092.PackagedInstances |
| 9 | |
| 10 | /-! |
| 11 | --- |
| 12 | title: Conjunctive query evaluation is NP-complete |
| 13 | type: theorem |
| 14 | --- |
| 15 | Boolean conjunctive query evaluation, in combined complexity, is NP-complete |
| 16 | in the sense of the NP core: it is definable in existential second-order |
| 17 | logic, guessing the valuation, and 3-colorability reduces to it by a |
| 18 | quantifier-free first-order reduction, the query of a graph being evaluated |
| 19 | in the triangle. This is the evaluation half of Chandra and Merlin (1977). |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax420092.EvaluationNPComplete |
| 23 | |
| 24 | open FirstOrder FirstOrder.Language |
| 25 | open Lax904597.Problems Lax904597.Interpretations Lax904597.Classes Lax799700.Problems |
| 26 | open Lax420092.QueryDatabases Lax420092.Evaluation Lax420092.QueryPairs Lax420092.PackagedInstances |
| 27 | |
| 28 | /-- CQEval is NP-complete. -/ |
| 29 | axiom cqEval_NP_complete : NP.Complete CQEval |
| 30 | |
| 31 | end Lax420092.EvaluationNPComplete |
| 32 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments