Analysis of Branching Heuristics in SAT Solvers

 
Tie break
 
University of Tokyo
Seongsoo Moon
 
Lists of solvers
 
Sequential solvers
CHBR_GLUCOSE
CHBR_GLUCOSE_TUNED
TB_GLUCOSE
TC_GLUCOSE
 (bug exist?)
 
Parallel solver
ParaGlueminisat
 
}
 
Glucose + CHB [Liang+, 16]
 
Glucose + TBVSIDS
 
Glucose + CHB + TBVSIDS
 
Session 4A (12:00 – 12:30)
 
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
 
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
 
VSIDS
 
VSIDS
 
Is this reasonable?
TBVSIDS [MOON+, CP-DP 2016]
VSIDS
TBVSIDS
 
×
Compare first by activity
If activitys are equal, 
compare activityQ
 
TBVSIDS [MOON+, CP-DP 2016]
VSIDS
TBVSIDS
 
×
 
Priority
 
In VSIDS,
 
In TBVSIDS,
 
TBVSIDS [MOON+, CP-DP 2016]
VSIDS
TBVSIDS
 
×
 
Priority
 
In VSIDS,
 
In TBVSIDS,
 
TBVSIDS [MOON+, CP-DP 2016]
 
Clause learning
 
Conflict
 
TBVSIDS1 [MOON+, CP-DP 2016]
 
TBVSIDS2 [MOON+, CP-DP 2016]
 
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
 
Hybrid CHB + TBVSIDS
 
Why Hybrid?
 
Benchmarks: 300 instances from SAT Competition 2014 application track
Timeout: 3,600 s
 
Results
 
Benchmarks: 900 instances from 2014Crafted, 2014App and 2015App
Slide Note

Hi. My name is seong soo Moon from Univ of Tokyo.

I will introduce our solvers briefly.

Embed
Share

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

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.

E N D

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

More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#