Computer Science – Artificial Intelligence
Scientific paper
2011-09-09
Presented at 8th International Workshop on Local Search Techniques in Constraint Satisfaction (LSCS 2011)
Computer Science
Artificial Intelligence
15 pages
Scientific paper
This work focuses on improving state-of-the-art in stochastic local search (SLS) for solving Boolean satisfiability (SAT) instances arising from real-world industrial SAT application domains. The recently introduced SLS method CRSat has been shown to noticeably improve on previously suggested SLS techniques in solving such real-world instances by combining justification-based local search with limited Boolean constraint propagation on the non-clausal formula representation form of Boolean circuits. In this work, we study possibilities of further improving the performance of CRSat by exploiting circuit-level structural knowledge for developing new search heuristics for CRSat. To this end, we introduce and experimentally evaluate a variety of search heuristics, many of which are motivated by circuit-level heuristics originally developed in completely different contexts, e.g., for electronic design automation applications. To the best of our knowledge, most of the heuristics are novel in the context of SLS for SAT and, more generally, SLS for constraint satisfaction problems.
Belov Anton
Järvisalo Matti
No associations
LandOfFree
Structure-Based Local Search Heuristics for Circuit-Level Boolean Satisfiability does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Structure-Based Local Search Heuristics for Circuit-Level Boolean Satisfiability, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Structure-Based Local Search Heuristics for Circuit-Level Boolean Satisfiability will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-414031