Search

We first define a mapping from CSP to many-valued SAT which allows to solve CSP instances with many-valued SAT solvers. Second, we define a new many-valued resolution rule and prove that it is refutation complete for many-valued CNF formulas and, moreover, enforces CSP (i,j)-consistency when applied to a many-valued SAT encoding of a CSP. Instances of our rule enforce well-known local consistency properties such as arc consistency and path consistency. [ABSTRACT FROM AUTHOR]

Sequence variables play an interesting role in unification and matching when dealing with terms in an unranked signature. Sequence Unification generalizes Word Unification and seems to be appealing for information extraction in XML documents, program transformation, and rule-based programming. In this work we study a relation between Sequence Unification and another generalization of Word Unification: Context Unification. We introduce a variant of Context Unification, called Left-Hole Context Unification that serves us to reduce Sequence Unification to it: We define a partial currying procedure to translate sequence unification problems into left-hole context unification problems, and prove soundness of the translation. Furthermore, a precise characterization of the shape of the unifiers allows us to easily reduce Left-Hole Context Unification to (the decidable problem of) Word Unification with Regular Constraints, obtaining then a decidability proof for an extension of Sequence Unification. [ABSTRACT FROM AUTHOR]

Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses of a given CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound. [ABSTRACT FROM AUTHOR]

Context Unification is the problem to decide for a given set of second-order equations E where all second-order variables are unary, whether there exists a unifier, such that for every second-order variable X, the abstraction λx. r instantiated for X has exactly one occurrence of the bound variable x in r. Stratified Context Unification is a specialization where the nesting of second-order variables in E is restricted. It is already known that Stratified Context Unification is decidable, NP-hard, and in PSPACE, whereas the decidability and the complexity of Context Unification is unknown. We prove that Stratified Context Unification is in NP by proving that a size-minimal solution can be represented in a singleton tree grammar of polynomial size, and then applying a generalization of Plandowski's polynomial algorithm that compares compacted terms in polynomial time. This also demonstrates the high potential of singleton tree grammars for optimizing programs maintaining large terms. A corollary of our result is that solvability of rewrite constraints is NP-complete. [ABSTRACT FROM AUTHOR]

Bounded Second-Order Unification is the problem of deciding, for a given second-order equation ${t {\stackrel{_?}=} u}$ and a positive integer m, whether there exists a unifier σ such that, for every second-order variable F, the terms instantiated for F have at most m occurrences of every bound variable. It is already known that Bounded Second-Order Unification is decidable and NP-hard, whereas general Second-Order Unification is undecidable. We prove that Bounded Second-Order Unification is NP-complete, provided that m is given in unary encoding, by proving that a size-minimal solution can be represented in polynomial space, and then applying a generalization of Plandowski's polynomial algorithm that compares compacted terms in polynomial time. [ABSTRACT FROM AUTHOR]

Context unification (CU) is the open problem of solving context equations for trees. We distinguish a new decidable variant of CU-well-nested CU - and present a new unification algorithm that solves well-nested context equations in non-deterministic polynomial time. We show that minimal well-nested solutions of context equations can be composed from the material present in the equation (see Theorem[1]). This property is wishful when modeling natural language ellipsis in CU. [ABSTRACT FROM AUTHOR]

Linear Second-Order Unification and Context Unification are closely related problems. However, their equivalence was never formally proved. Context unification is a restriction of linear second-order unification. Here we prove that linear second-order unification can be reduced to context unification with tree-regular constraints. Decidability of context unification is still an open question. We comment on the possibility that linear second-order unification is decidable, if context unification is, and how to get rid of the tree-regular constraints. This is done by reducing rank-bound tree-regular constraints to word-regular constraints. [ABSTRACT FROM AUTHOR]

There is a close relationship between word unification and second-order unification. This similarity has been exploited for instance for proving decidability of monadic second-order unification. Word unification. can be easily decided by transformation rules (similar to the ones applied in higher-order unification procedures) when variables are restricted to occur at most twice. Hence a well-known open question was the decidability of second-order unification under this same restriction. Here we answer this question negatively by reducing simultaneous rigid E-unification to second-order unification. This reduction, together with an inverse reduction found by Degtyarev and Voronkov, states an equivalence relationship between both unification problems. Our reduction is in some sense reversible, providing decidability results for cases when simultaneous rigid E-unification is decidable. This happens, for example, for one-variable problems where the variable occurs at most twice (because rigid E-unification is decidable for just one equation). We also prove decidability when no variable occurs more than once, hence significantly narrowing the gap between decidable and undecidable second-order unification problems with variable occurrence restrictions. [ABSTRACT FROM AUTHOR]