Fundamenta Informaticae - Volume 109, issue 1

Authors: Caron, Pascal | Flouret, Marianne

Article Type: Research Article

Abstract: We take an active interest in the problem of conversion of a Weighted Finite Automaton (WFA) into a \mathbb{K}-expression. The known algorithms give an exponential size expression in the number of states of the given automaton. We study the McNaughton-Yamada algorithm in the case of multiplicities and then we show that the resulting \mathbb{K}-expression is in the Star Normal Form (SNF) defined by Brüggemann-Klein [3]. The Glushkov algorithm computes an (n + 1)-state automaton from an expression having n occurrences of letters even in the multiplicity case [5]. We reverse this procedure and get a linear size \mathbb{K}-expression from a …Glushkov WFA. A characterization of Glushkov WFAs which are not in SNF is given. This characterization allows us to emphasize a normal form for \mathbb{K}-expressions. As for SNF in the boolean case, we show that every \mathbb{K}-expression has an equivalent one in normal form having the same Glushkov WFA. We end with an algorithm giving a small normal form \mathbb{K}-expression from a Glushkov WFA. Show more

DOI: 10.3233/FI-2011-427

Citation: Fundamenta Informaticae, vol. 109, no. 1, pp. 1-25, 2011

Authors: Kullmann, Oliver

Article Type: Research Article

Abstract: We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals are the wellknown “signed literals”, corresponding to unary constraints in CSP. However we argue that only the restricted form of “negative monosigned literals” and the resulting generalised clause-sets, corresponding to “sets of no-goods” in the AI literature, maintain the essential properties of boolean conjunctive normal forms. In this first part of a mini-series of two articles, we build up a solid foundation …for (generalised) clause-sets, including the notion of autarky systems, the interplay between autarkies and resolution, and basic notions of (DP-)reductions. As a basic combinatorial parameter of generalised clause-sets we introduce the (generalised) notion of deficiency, which in the boolean case is the difference between the number of clauses and the number of variables. Autarky theory plays a fundamental role here, and we concentrate especially on matching autarkies (based on matching theory). A natural task is to determine the structure of (matching) lean clause-sets, which do not admit non-trivial (matching) autarkies. A central result is the computation of the lean kernel (the largest lean subset) of a (generalised) clause-set in polynomial time for bounded maximal deficiency. Show more

Keywords: autarkies, deficiency, satisfiability problem, constraint satisfaction problem, generalized clause-sets, signed formulas, non-boolean variables, polynomial time, matching autarkies, lean clause-sets

DOI: 10.3233/FI-2011-428

Citation: Fundamenta Informaticae, vol. 109, no. 1, pp. 27-81, 2011

Authors: Kullmann, Oliver

Article Type: Research Article

Abstract: Concluding this mini-series of 2 articles on the foundations of generalised clause-sets, we study the combinatorial properties of non-boolean conjunctive normal forms (clause-sets), allowing arbitrary (but finite) sets of values for variables, while literals express that some variable shall not get some (given) value. First we study the properties of the direct translation (or “encoding”) of generalised clause-sets into boolean clause-sets. Many combinatorial properties are preserved, and as a result we can lift fixed-parameter tractability of satisfiability in the maximal deficiency from the boolean case to the general case. Then we turn to irredundant clause-sets, which generalise minimally unsatisfiable clause-sets, …and we prove basic properties. The simplest irredundant clause-sets are hitting clause-sets, and we provide characterisations and generalisations. Unsatisfiable irredundant clause-sets are the minimally unsatisfiable clause-sets, and we provide basic tools. These tools allow us to characterise the minimally unsatisfiable clause-sets of minimal deficiency. Finally we provide a new translation of generalised boolean clause-sets into boolean clause-sets, the nested translation, which preserves the conflict structure. As an application, we can generalise results for boolean clause-sets regarding the hermitian rank/defect, especially the characterisation of unsatisfiable hitting clause-sets where between every two clauses we have exactly one conflict. We conclude with a list of open problems, and a discussion of the “generic translation scheme”. Show more

Keywords: generalised clause-sets, satisfiability, non-boolean variables, boolean translations, direct encoding, irredundant clause-sets, minimally unsatisfiable clause-sets. deficiency, hitting clause-sets, disjoint DNF, hermitian defect, nested translation

DOI: 10.3233/FI-2011-429

Citation: Fundamenta Informaticae, vol. 109, no. 1, pp. 83-119, 2011