<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>7715</REFNUM><AUTHORS><AUTHOR>Donaldson,A.</AUTHOR><AUTHOR>Miller,A.</AUTHOR><AUTHOR>Calder,M.</AUTHOR></AUTHORS><YEAR>2004</YEAR><TITLE>Comparing the use of symmetry in constraint processing and model checking</TITLE><PLACE_PUBLISHED> Proceedings of the the 4th International Workshop on Symmetry and Constraint Satisfaction Problems (SymCon'04) </PLACE_PUBLISHED><PUBLISHER>N/A</PUBLISHER><PAGES>18-25</PAGES><LABEL>Donaldson:2004:7715</LABEL><KEYWORDS><KEYWORD>symmetry reduction</KEYWORD></KEYWORDS<ABSTRACT>Both model checking and constraint processing involve the searching of graphs: in model checking to establish the truth of a temporal logic formula; in constraint processing to determine whether or not solutions to a problem exist which satisfy a set of constraints. In both fields, the presence of symmetry in the model or problem can result in redundant search over equivalent areas of the graph or search space. Recently there has been much interest in symmetry reduction in model checking, and symmetry breaking in constraint satisfaction problems (CSPs). The n-queens problem is a CSP to which symmetry breaking has been applied. To illustrate the approaches to exploiting symmetry in both model checking and CSPs we show how the n-queens problem can be solved using model checking, and how symmetry reduction can be used to make larger instances of the problem tractable. Through this example we haghlight the similarities and diferences between the approaches. </ABSTRACT></RECORD></RECORDS></XML>