Symmetry and Satisfiability Update: An Insightful Study
This updated work by Hadi Katebi, Karem A. Sakallah, and Igor L. Markov delves into the interplay between symmetry and satisfiability, offering a fresh perspective on the subject. The presentation by Chien-Yen Kuo sheds light on new findings and potential implications in the field. This insightful examination combines theory with practical applications, making it a valuable resource for researchers, academics, and enthusiasts seeking a comprehensive understanding of the topic. Tags: Symmetry, Satisfiability, Study, Research, Insightful
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Symmetry and Satisfiability: An Update Author: Hadi Katebi, Karem A. Sakallah, Igor L. Markov Presenter: Chien-Yen Kuo
Symmetry Structures in SAT For a typical SAT, there are some symmetry structures = (a'+b+c)(a+b'+c')(b'+c) (a'+b+c) (a+b'+c') (b'+c) (a'+b+c) (a+b'+c') (b'+c) (a,a')(b,c')(b',c) 000 001 101 111 000 001 101 111
Symmetry Breaking To reduce search space Break it! Symmetry-breaking predicates (SBPs) Sorted variables, ex: ?,?,? For all truth assignments of ?, SBPs agree with exactly one in each equivalent class defined by symmetry = (a'+b+c)(a+b'+c')(b'+c)(a') = (a'+b+c)(a+b'+c')(b'+c) SBPs: ? ? ? = ? ? ? ? = ? ? = ? (?,? )(?,? )(? ,?) ? ?
Calculate SBPs Shatter Encode CNF formula as colored graph Determine symmetries on the graph nauty: for small, dense graph saucy: for large, sparse graph Convert to SBPs Append SBPs to the original formula Resulting formula is often much faster to solve We then focus on graph symmetry, a structure remaining unchanged under certain mapping
Notations ? = {0,1, ? 1} Permutation of ? Bijection from ? to ? ?: identity permutation Automorphism Group Set of permutations that preserve edge relations
Permutation Representation Ordered partition ? of ? ? = ?1?2 |??, where ??refers to cell Ordered partition pair, OPP Isomorphic: ? = ?, ?? = ??for all ? Matching: corresponding non-singleton cells are identical
Determine Graph Symmetry Baseline Pick a non-singleton cell ??from top partition Pick a vertex ? from ?? Map ? to a vertex ? from ?? Similar to backtracking SAT solving Assumption Vertex mapping Propagation Partition refinement
Automorphism Group ?: automorphism group An action of ? is a map :? ? ? ? ? = ? for all ? ? ?? ? = ? ? ? for all ? ? and all ?,? ? Equivalence relation ~ on ? ?~? iff ? ? = ? for some ? ? ??: equivalent class, or orbit, of ?
Coset Pruning Stabilizer subgroup ??= ? ?|? ? = ? Coset of ?? ???= {??|? ??}, for ? ? but ? ?? Any element in coset ???generates ???by composing with elements in ?? Thus representative for ???
Coset Pruning Solving (representative of) each coset is a subproblem ?? ??(solution ?? ??) Note that ?1, ?2, ,?? ??
Orbit Pruning If ?? ???and ? > ?, skip ??? Must necessarily contain redundant generators
Other Pruning Skills Matching OPP Pruning Quick discover of candidate coset representative Non-isomorphic OPP pruning
Experimental Results About 93% cases are finished in one second
Conclusions A scalable symmetry-detection algorithm But some CNF instances may not benefit from static symmetry breaking Dynamic detection in SAT solving May uncover hidden/conditional symmetries
