KR2020Proceedings of the 17th International Conference on Principles of Knowledge Representation and ReasoningProceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning

Rhodes, Greece. September 12-18, 2020.

Edited by

ISSN: 2334-1033
ISBN: 978-0-9992411-7-2

Sponsored by
Published by

Copyright © 2020 International Joint Conferences on Artificial Intelligence Organization

Symbolic Solutions for Symbolic Constraint Satisfaction Problems

  1. Alexsander Andrade de Melo(Federal University of Rio de Janeiro)
  2. Mateus De Oliveira Oliveira(University of Bergen)


  1. Computational aspects of knowledge representation-General


A fundamental drawback that arises when one is faced with the task of deterministically certifying solutions to computational problems in PSPACE is the fact that witnesses may have superpolynomial size, assuming that NP is not equal to PSPACE. Therefore, the complexity of such a deterministic verifier may already be super-polynomially lower-bounded by the size of a witness. In this work, we introduce a new symbolic framework to address this drawback. More precisely, we introduce a PSPACE-hard notion of symbolic constraint satisfaction problem where both instances and solutions for these instances are implicitly represented by ordered decision diagrams (i.e. read-once, oblivious, branching programs). Our main result states that given an ordered decision diagram D of length k and width w specifying a CSP instance, one can determine in time f(w,w')*k whether there is an ODD of width at most w' encoding a solution for this instance. Intuitively, while the parameter w quantifies the complexity of the instance, the parameter w' quantifies the complexity of a prospective solution. We show that CSPs of constant width can be used to formalize natural PSPACE hard problems, such as reachability of configurations for Turing machines working in nondeterministic linear space. For such problems, our main result immediately yields an algorithm that determines the existence of solutions of width w in time g(w)*n, where g:N->N is a suitable computable function, and n is the size of the input.