On the Satisfiability of Complex Constraints

On the Satisfiability of Complex Constraints Luis Damas Universidade do Porto, Rua do Campo Alegre 823, 4000 Porto, Portugal Giovanni B. Varile CEC , 2920 Luxembourg, Luxembourg Abstract The main problem arising from the use of com- plex constraints in Computational Linguists is due to the NP-hardness of checking whether a given set of constraints is satisfiable and, in the affirmative case, of generating the set of min- imal models which satisfy the constraints. In this "paper we show how the CLG approach to rewriting constraints while constructing a par- tial model can greatly reduce the size of the original constraints and thus contribute to re- duce the computational problem. 1 Introduction Most of the more recent formalisms in Com- putational Linguistics involve complex con- straints, i.e. involving either disjunction or and negation of equality constraints [Kay85, KB82, PS87]. From a practical point of view, the main problem arising from the introduction of com- plex constraints is due to the NP-hardness of checking whether a given set of constraints is satisfiable and, in the affirmative case, of gen- erating tile set of minimal models which satisfy thc constraints. Since the NP-hardness of the problem tends to manifest in practical applications in a dra~ matic way there were several proposals of algo- rithms to minimize this problem [Kas87, ED88, MK91]. However, in our opinion, any practical ap- proach to the problem should rely on apply- ing an exponential satisfaction algorithm as sel- dom as possible and also, when that cannot be avoided, to reduce as much as possible the size of tile input formulae to which the algorithm is applied. A classical way in which one can reduce the size of input formulae is by factoring, i.e. ex- pressing it as a conjunction of smaller formulae which do not have variables in common. As a matter of fact if instead of checking the sat- isfiability of a formula of length nk we check the satisfiability of n formulae of size k we are gaining an exponential reduction in time. This strategy is also explored in [MK91]. Another way of reducing the size of input for- mulae which has been used in CLG implemen- tations [DV89, BDMVg0, DMVglb], and which can be combined with the previous approaches, is to build a partial model of the input formula and to apply the algorithm to the remaining constraints. Since in many cases this is able to do away with all the constraints this also achieves the goal of using the exponential satis- faction algorithm as seldom as possible. This method can also be seen as a generalization of steps 1 and 2 of the algorithm described in [Kas87], while avoiding some of its pitfalls. In this paper we start by showing, by trans- lating to the feature logics context the methods for first order terms introduced in [DMV91a, DMV91b], how the CLG approach to rewriting constraints while constructing a partial model can greatly reduce the size of the original con- straints and thus contribute …

Content truncated to 500 words