Arrow Research search

Author name cluster

Mark Weyer

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

CSL Conference 2009 Conference Paper

Decidable Relationships between Consistency Notions for Constraint Satisfaction Problems

  • Albert Atserias
  • Mark Weyer

Abstract We define an abstract pebble game that provides game interpretations for essentially all known consistency algorithms for constraint satisfaction problems including arc-consistency, ( j, k )-consistency, k -consistency, k -minimality, and refinements of arc-consistency such as peek arc-consistency and singleton arc-consistency. Our main result is that for any two instances of the abstract pebble game where the first satisfies the additional condition of being stacked, there exists an algorithm to decide whether consistency with respect to the first implies consistency with respect to the second. In particular, there is a decidable criterion to tell whether singleton arc-consistency with respect to a given constraint language implies k -consistency with respect to the same constraint language, for any fixed k. We also offer a new decidable criterion to tell whether arc-consistency implies satisfiability which pulls from methods in Ramsey theory and looks more amenable to generalization.

Details

CSL Conference 2009 Conference Paper

Tree-Width for First Order Formulae

  • Isolde Adler
  • Mark Weyer

Abstract We introduce tree-width for first order formulae ϕ, fotw( ϕ ). We show that computing fotw is fixed-parameter tractable with parameter fotw. Moreover, we show that on classes of formulae of bounded fotw, model checking is fixed parameter tractable, with parameter the length of the formula. This is done by translating a formula ϕ with fotw( ϕ ) < k into a formula of the k -variable fragment \({\mathcal L^k}\) of first order logic. For fixed k, the question whether a given first order formula is equivalent to an \({\mathcal L^k}\) formula is undecidable. In contrast, the classes of first order formulae with bounded fotw are fragments of first order logic for which the equivalence is decidable. Our notion of tree-width generalises tree-width of conjunctive queries to arbitrary formulae of first order logic by taking into account the quantifier interaction in a formula. Moreover, it is more powerful than the notion of elimination-width of quantified constraint formulae, defined by Chen and Dalmau (CSL 2005): For quantified constraint formulae, both bounded elimination-width and bounded fotw allow for model checking in polynomial time. We prove that fotw of a quantified constraint formula φ is bounded by the elimination-width of φ, and we exhibit a class of quantified constraint formulae with bounded fotw, that has unbounded elimination-width. A similar comparison holds for strict tree-width of non-recursive stratified datalog as defined by Flum, Frick, and Grohe (JACM 49, 2002). Finally, we show that fotw has a characterization in terms of a robber and cops game without monotonicity cost.

Details