Containment, Equivalence and Coreness from CSP to QCSP and beyond
This work addresses theoretical complexity problems in logic and computer science for researchers in constraint satisfaction and quantified logic, but it is incremental as it extends prior results.
The paper investigates containment, equivalence, and coreness in constraint satisfaction problems (CSP) and their quantified extensions (QCSP and QCSP_or), characterizing cores for QCSP in certain structures and finding them more elusive than for CSP.
The constraint satisfaction problem (CSP) and its quantified extensions, whether without (QCSP) or with disjunction (QCSP_or), correspond naturally to the model checking problem for three increasingly stronger fragments of positive first-order logic. Their complexity is often studied when parameterised by a fixed model, the so-called template. It is a natural question to ask when two templates are equivalent, or more generally when one "contain" another, in the sense that a satisfied instance of the first will be necessarily satisfied in the second. One can also ask for a smallest possible equivalent template: this is known as the core for CSP. We recall and extend previous results on containment, equivalence and "coreness" for QCSP_or before initiating a preliminary study of cores for QCSP which we characterise for certain structures and which turns out to be more elusive.