Analysis of Branching Heuristics in SAT Solvers

This content delves into various branching heuristics used in SAT solvers, such as Exponential Recency Weighted Average, Conflict History-Based, and Tie-break of VSIDS. It discusses the decision-making processes of solvers and compares different approaches to handle ties and improve solver performance.

• Branching heuristics
• SAT solvers
• Tie-break
• VSIDS
• Conflict history-based

mur_b Follow

Uploaded on Oct 02, 2024 | 0 Views

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. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Tie break University of Tokyo Seongsoo Moon

2. Lists of solvers Sequential solvers CHBR_GLUCOSE CHBR_GLUCOSE_TUNED TB_GLUCOSE TC_GLUCOSE (bug exist?) } Glucose + CHB [Liang+, 16] Glucose + TBVSIDS Glucose + CHB + TBVSIDS Parallel solver ParaGlueminisat Session 4A (12:00 12:30)

3. CHB [Liang+, AAAI 16] Conflict history-based branching heuristic Introduced in AAAI 2016 Title: Exponential Recency Weighted Average Branching Heuristic for SAT Solvers Solve significantly more instances than VSIDS

4. TBVSIDS [MOON+, CP-DP 2016] Tie break of VSIDS Tie occurs frequently and broken randomly in VSIDS Ties are broken randomly by default, although this is configurable [Moskewicz+, 2001] VSIDS in many SAT solvers uses heap array for VSIDS Proposal of meaningful selection from ties

5. VSIDS 2v Variables = { , , , , , } v v v v v v 1 2 3 4 5 6 3v 5v = ( ) 2 activity v 1 = ( ) 100 activity v 1v 4v 6v 2 = ( ) 19 activity v 3 = ( ) 25 activity v Pick 2 v reconstruc , t 4 = ( ) 36 activity v 5 = ( ) 3 activity v 5v 6 3v 4v 1v 6v

6. VSIDS 2v Variables = { , , , , , } v v v v v v 1 2 3 4 5 6 3v 5v = ( ) 2 activity v 1 = ( ) 100 activity v 1v 6v 4v 2 = ( ) 100 activity v 3 = ( ) 25 activity v Is this reasonable? Pick 2 v reconstruc , t 4 = ( ) 36 activity v 5 = ( ) 100 activity v 5v 6 3v 4v 1v 6v

7. TBVSIDS [MOON+, CP-DP 2016] 2v Variables = { , , , , , } v v v v v v 1 2 3 4 5 6 3v 5v = = ( ) , 2 ( ) 1 activity v activityQ v 1 1 = = ( ) 100 , ( ) 15 activity v activityQ v 1v 6v 4v 2 2 = = ( ) 100 , ( ) 10 activity v activityQ v 3 3 = = ( ) 25 , ( ) 10 activity v activityQ v VSIDS TBVSIDS 4 4 = = ( ) 36 , ( ) 5 activity v activityQ v 5 5 6v = = ( ) 100 , ( ) 20 activity v activityQ v 6 6 5v 2v Compare first by activity If activitys are equal, compare activityQ 1v 3v 4v

8. TBVSIDS [MOON+, CP-DP 2016] 2v Variables = { , , , , , } v v v v v v 1 2 3 4 5 6 3v 5v = = ( ) , 2 ( ) 1 activity v activityQ v 1 1 = = ( ) 100 , ( ) 15 activity v activityQ v 1v 6v 4v 2 2 = = ( ) 100 , ( ) 10 activity v activityQ v 3 3 = = ( ) 25 , ( ) 10 activity v activityQ v VSIDS TBVSIDS 4 4 = = ( ) 36 , ( ) 5 activity v activityQ v 5 5 6v = = ( ) 100 , ( ) 20 activity v activityQ v 6 6 Priority 5v 2v = = In VSIDS, In TBVSIDS, v v v 3 2 6 1v 3v 4v v v v 3 2 6

9. TBVSIDS [MOON+, CP-DP 2016] 2v Variables = { , , , , , } v v v v v v 1 2 3 4 5 6 3v 5v = = ( ) , 2 ( ) 1 activity v activityQ v 1 1 = = ( ) 100 , ( ) 20 activity v activityQ v 1v 6v 4v 2 2 = = ( ) 100 , ( ) 10 activity v activityQ v 3 3 = = ( ) 25 , ( ) 10 activity v activityQ v VSIDS TBVSIDS 4 4 = = ( ) 36 , ( ) 5 activity v activityQ v 5 5 6v = = ( ) 100 , ( ) 20 activity v activityQ v 6 6 Priority 5v 2v = = In VSIDS, In TBVSIDS, v v v 3 2 6 1v 3v 4v = v v v 3 2 6

10. TBVSIDS [MOON+, CP-DP 2016] Conflict v { , } 6v v { , } v 8 7 8 v v { , } { , , } v v v Update each varia ble`s activity 6 7 2 5 6 relevant t resolution o v { , , } { , , } v v v v v 2 5 7 3 5 7 { , , } v v v 2 3 5 Clause learning Update each varia ble`s activityQ { , , } v v v learned a in clause 2 3 5

11. TBVSIDS1 [MOON+, CP-DP 2016]

12. TBVSIDS2 [MOON+, CP-DP 2016]

13. Tie occurences Benchmarks: 300 instances from SAT Competition 2014 application track Timeout: 1,000 s 96 / 145 (66.2 %) reduced 110 / 151 (72.8 %) reduced

14. Hybrid CHB + TBVSIDS

15. Why Hybrid? Benchmarks: 300 instances from SAT Competition 2014 application track Timeout: 3,600 s

16. Results Benchmarks: 900 instances from 2014Crafted, 2014App and 2015App