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. Therefo...

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Javier Álvez, Paqui Lucio
• Keywords: ENTCS 2008, Most Well-known Algorithms, Normal Form, Quantifier Elimination