A New Proposal Of Quasi-Solved Form For Equality Constraint Solving

Most well-known algorithms for equational solving are based on quantifier elimination. This technique iteratively eliminates the innermost block of existential/universal quantifiers from prenex formulas whose matrices are in some normal form (mostly DNF). Traditionally used notions of normal form satisfy that every constraint (in normal form) different from false is trivially satisfiable. Hence, they are called solved forms. However, the manipulation of such constraints require hard transformations, especially due to the use of the distributive and the explosion rules, which increase the number of constraints at intermediate stages of the solving process. On the contrary, quasi-solved forms allow for simpler transformations by means of a more compact representation of solutions, but their satisfiability test is not so trivial. Nevertheless, the total cost of checking satisfiability and manipulating constrains using quasi-solved forms is cheaper than using simpler solved forms. Therefore, they are suitable for improving the efficiency of constraint solving procedures. In this paper, we present a notion of quasi-solved form that provides a good trade-off between the cost of checking satisfiability and the effort required to manipulate constraints. In particular, our new quasi-solved form has been carefully designed for efficiently handling conjunction and negation, which are the main Boolean operations necessary to keep matrices of formulas in normal form