Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization

Slide Note
Embed
Share

Weighted MaxSAT is a optimization problem where targets are assigned weights and hard clauses must be satisfied. The goal is to find a model that maximizes the overall weight of satisfied target bits. The formulation involves unit clauses associated with integer weights, with a focus on improving polarity selection and using bit-vector optimization techniques to enhance efficiency. The output is a model that maximizes the weight of satisfied target bits. Real-world examples and models are provided to illustrate the concept.

agabr
agabr Follow

Uploaded on Nov 27, 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. Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization Alexander Nadel, Intel Israel FMCAD 19, San Jose California, USA October 25, 2019 11/27/2024 1 PEG PDS DDI

  2. Weighted MaxSAT Formulation Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal (unit clause), associated with an integer weight w(ti) > 0 Hard Clauses H - Satisfiable 11/27/2024 2 PEG PDS DDI

  3. Weighted MaxSAT Formulation Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal (unit clause), associated with an integer weight w(ti) > 0 Hard Clauses H - Satisfiable ? 1?(??) ?(??) Output: A model M to H which maximizesthe overall weight of the satisfied target bits ?=0 11/27/2024 3 PEG PDS DDI

  4. Weighted MaxSAT Formulation Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal (unit clause), associated with an integer weight w(ti) > 0 Hard Clauses H - Satisfiable ? 1?(??) ?(??) Output: A model M to H which maximizes the overall weight of the satisfied target bits ?=0 Example: H = ( a + b) ( a + c) (a + c); T = {a,b} H has 3 models: - M1={a=1, b=0, c=1} - M2={a=0, b=1, c=0} - M3={a=0, b=0, c=0} 11/27/2024 4 PEG PDS DDI

  5. Weighted MaxSAT Formulation Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal (unit clause), associated with an integer weight w(ti) > 0 Hard Clauses H - Satisfiable ? 1?(??) ?(??) Output: A model M to H which maximizes the overall weight of the satisfied target bits ?=0 Example: H = ( a + b) ( a + c) (a + c); T = {a,b} H has 3 models: - M1={a=1, b=0, c=1} - M2={a=0, b=1, c=0} - M3={a=0, b=0, c=0} Best model for w(a)=2; w(b)=1 11/27/2024 5 PEG PDS DDI

  6. Weighted MaxSAT Formulation Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal (unit clause), associated with an integer weight w(ti) > 0 Hard Clauses H - Satisfiable ? 1?(??) ?(??) Output: A model M to H which maximizes the overall weight of the satisfied target bits ?=0 Example: H = ( a + b) ( a + c) (a + c); T = {a,b} H has 3 models: - M1={a=1, b=0, c=1} - M2={a=0, b=1, c=0} - M3={a=0, b=0, c=0} Best model for w(a)=1; w(b)=2 11/27/2024 6 PEG PDS DDI

  7. Weighted MaxSAT Formulation Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal (unit clause), associated with an integer weight w(ti) > 0 Hard Clauses H - Satisfiable ? 1?(??) ?(??) Output: A model M to H which maximizes the overall weight of the satisfied target bits ?=0 Example: H = ( a + b) ( a + c) (a + c); T = {a,b} H has 3 models: - M1={a=1, b=0, c=1} - M2={a=0, b=1, c=0} - M3={a=0, b=0, c=0} Never the best, since the cost is 0 11/27/2024 7 PEG PDS DDI

  8. Why is MaxSAT Useful? Solves problems with SAT X. Si, X. Zhang, R. Grigore, and M. Naik. Maximum satisfiability in software analysis: Applications and techniques. CAV 2017 Plenty of applications in CAD and other areas (AI, Planning, Bio-informatics, ) 11/27/2024 8 PEG PDS DDI

  9. Why Is MaxSAT Useful to Intel? SMT in production for various tasks "PhysicalDesign" by Linear77 - Own work. Licensed under CC BY 3.0 via Wikimedia Commons - https://commons.wikimedia.org/wiki/File:PhysicalDesign.png#/media/File:PhysicalDesign.png 11/27/2024 9 PEG PDS DDI

  10. Fixer of an Existing Placement of Cells in a Fub Alexander Nadel and Vadim Ryvchin, Bit-Vector Optimization , TACAS 16. Basic Input: Grid of size (X, Y) n non-overlapping rect s (cells) placed on a grid Violation; Priority 3 Violations between pairs of cells touching top-to-bottom : Each violation has a uniquepriority Violation; Priority 1 Output and Additional Constraints: New cells placement while minimizing violations Movement along both axes is allowed, but restricted To meet backward compatibility req s Additional constraint (e.g., parity) Violation; Priority 2 10 PEG PDS DDI

  11. Example Solution Violation; Priority 3 Violation; Priority 1 Violation; Priority 2 11 PEG PDS DDI

  12. Fixer Problem Solution Alexander Nadel and Vadim Ryvchin, Bit-Vector Optimization , TACAS 16. Solved by reduction to Bit-vector Optimization(aka Optimization Modulo Bit-vectors or OBV) Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal Hard Clauses H - Satisfiable Output: A model M to H which maximizesthe value of T (interpreted as an unsigned number) Example: H = ( a + b) ( a + c) (a + c); T = {a,b} H has 3 models: - M1={a=1, b=0, c=1} - M2={a=0, b=1, c=0} - M3={a=0, b=0, c=0} Best model! The reduction to OBV worked because of the strict order between violations 11/27/2024 12 PEG PDS DDI

  13. New Requirements 1. Each violation can be associated with an integer weight Reflecting the actual cost in $$ of leaving that violation un-fixed Makes the problem reducible to MaxSAT, rather than OBV 11/27/2024 13 PEG PDS DDI

  14. New Requirements 1. Each violation can be associated with an integer weight Reflecting the actual cost in $$ of leaving that violation un-fixed Makes the problem reducible to MaxSAT, rather than OBV 2. Incrementality Incremental solving under different hard assumptions and targets Solving lexicographically ordered classes What-if analysis 11/27/2024 14 PEG PDS DDI

  15. New Requirements 1. Each violation can be associated with an integer weight Reflecting the actual cost in $$ of leaving that violation un-fixed Makes the problem reducible to MaxSAT, rather than OBV 2. Incrementality Incremental solving under different hard assumptions and targets Solving lexicographically ordered classes What-if analysis 3. Anytime-ness Generate an improving set of models M1, M2, M3, Critical for production, since we need an approximate solution for every instance 11/27/2024 15 PEG PDS DDI

  16. New Requirements 1. Each violation can be associated with an integer weight Reflecting the actual cost in $$ of leaving that violation un-fixed Makes the problem reducible to MaxSAT, rather than OBV 2. Incrementality Incremental solving under different hard assumptions and targets Solving lexicographically ordered classes What-if analysis 3. Anytime-ness Generate an improving set of models M1, M2, M3, Critical for production, since we need an approximate solution for every instance 11/27/2024 16 PEG PDS DDI

  17. Anytime Incremental MaxSAT: Solution Sketch WMB (Weighted Mrs. Beaver) algorithm Generalize Mrs. Beaver: an anytime incremental unweighted MaxSAT algorithm to weighted MaxSAT Alexander Nadel, Solving MaxSAT with Bit-Vector Optimization . SAT 18. No other incremental MaxSAT algorithm is described in literature Algorithm-independent polarity and variable heuristics for anytime MaxSAT Target-Optimal-Rest-Conservative (TORC) polarity selection Target-Score-Bump (TSB) variable heuristic Implementation and Impact Hazel: implemented WMB algorithm as well as TORC and TSB heuristics in Intel s proprietary solver Hazel Successfully productized @ Intel Would have won both (non-incremental!) Weighted Incomplete tracks of MaxSAT Evaluation 2018 TT-Open-WBO-Inc: implemented TORC & TSB only in the open-source solver Open-WBO-Inc Won both the Weighted Incomplete tracks of the latest MaxSAT Evaluation 2019 11/27/2024 17 PEG PDS DDI

  18. Agenda for the Rest of the Talk Polarity Heuristics Variable Heuristics WMB Algorithm Experimental Results 11/27/2024 18 PEG PDS DDI

  19. Agenda for the Rest of the Talk Polarity Heuristics Variable Heuristics WMB Algorithm Experimental Results 11/27/2024 19 PEG PDS DDI

  20. Polarity Selection in SAT Which value (0 or 1) to assign to a new decision variable? Phase saving: always choose the latest assigned value Frost D. and Dechter R., In search of the best constraint satisfaction search, AAAI 94. Refocus on the same space Strichman O., Tuning SAT checkers for bounded model checking, CAV 00. Pipatsrisawat, K. and Darwiche, A. A Lightweight Component Caching Scheme for Satisfiability Solvers. SAT'07. Doesn t perform well for anytime MaxSAT! 11/27/2024 20 PEG PDS DDI

  21. LSU: a Simple Anytime MaxSAT Algorithm Daniel Le Berre, Anne Parrain: The Sat4j library, release 2.2. JSAT 7(2-3): 59-6 (2010) 11/27/2024 21 PEG PDS DDI

  22. LSU: a Simple Anytime MaxSAT Algorithm Daniel Le Berre, Anne Parrain: The Sat4j library, release 2.2. JSAT 7(2-3): 59-6 (2010) Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal (unit clause), associated with an integer weight w(ti) > 0 Hard Clauses H - Satisfiable Output: A model M to H which maximizesthe overall weight of the satisfied target bits Linear SAT-UNSAT (LSU) F H Do SAT(F) If (Satisfiable with a model M) Block all the models of weight <= w(M) in F Using a Pseudo-Boolean constraint Else Return the best model so far 11/27/2024 22 PEG PDS DDI

  23. Polarity Selection for Anytime MaxSAT Look for a model near a certain assignment M Conservative: M is the best solution so far (Barcelogic; Roig 13) Optimistic: M is the ideal assignment (targets are assigned 1) (Sat4j; Le Berre and Parrain. JSAT 10) How: Fix the polarity of variables (Guide-k-SAT; Agbaria, Carmi, Cohen, Korchemny, Lifshits and Nadel. FMCAD 10) Fixing means always assigning a certain value first Assigning the value only once is also possible Why: Conservative: finds the next model much faster than the default Optimistic: biases the search towards the ideal 11/27/2024 23 PEG PDS DDI

  24. Target-Optimal-Rest-Conservative (TORC) Polarity Selection Leverage the best of both the conservative and the optimistic approaches 11/27/2024 24 PEG PDS DDI

  25. Target-Optimal-Rest-Conservative (TORC) Polarity Selection Leverage the best of both the conservative and the optimistic approaches TORC Algorithm: whenever the variable decision heuristic chooses: A non-target variable: TORC sets its polarity to its value in the best model so far Only after the initial SAT invocation is completed The conservative part to make the search faster! A target variable: TORC sets its polarity to 1 The optimistic part to bias the search towards the ideal! 11/27/2024 25 PEG PDS DDI

  26. Agenda for the Rest of the Talk Polarity Heuristics Variable Heuristics WMB Algorithm Experimental Results 11/27/2024 26 PEG PDS DDI

  27. Target-Score-Bump (TSB) Variable Heuristic Increase the likelihood of starting near the ideal assignment TSB algorithm Initially, bump up the scores of the target variables As if the targets participated in a conflict clause An anytime MaxSAT algorithm with TSB & TORC is likely to: Start looking near the ideal assignment, yet won t get stuck Continue to give preference to impactful targets TSB refinement Not in the paper, but in TT-Open-WBO-Inc solver description Make the score boost proportional to the weight 11/27/2024 27 PEG PDS DDI

  28. Agenda for the Rest of the Talk Polarity Heuristics Variable Heuristics WMB Algorithm Experimental Results 11/27/2024 28 PEG PDS DDI

  29. Mrs. Beaver for Unweighted MaxSAT (Simplified) Alexander Nadel, Solving MaxSAT with Bit-Vector Optimization . SAT 18. 11/27/2024 29 PEG PDS DDI

  30. Mrs. Beaver for Unweighted MaxSAT (Simplified) Alexander Nadel, Solving MaxSAT with Bit-Vector Optimization . SAT 18. Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal (unit clause) Hard Clauses H - Satisfiable Output: A model M to H which maximizesthe number of the satisfied target bits 11/27/2024 30 PEG PDS DDI

  31. Mrs. Beaver for Unweighted MaxSAT (Simplified) Alexander Nadel, Solving MaxSAT with Bit-Vector Optimization . SAT 18. Input: Optimization Target T = {tn-1, tn-2, , t0} - Each target bit ti is a literal (unit clause) Hard Clauses H - Satisfiable Output: A model M to H which maximizesthe number of the satisfied target bits An anytime incremental SAT-based Bit-vector Optimization algorithm Mrs. Beaver Do Incomplete part OBV-BS(F, T) Shuffle or Reverse T S := Sum of the satisfied bits in T in unary encoding Complete part OBV-BS(F, S) Incremental under different hard assumptions and targets 11/27/2024 31 PEG PDS DDI

  32. WMB: Generalizing Mrs. Beaver to Weighted MaxSAT Mrs. Beaver Do OBV-BS(F, T) Shuffle or Reverse T S := Sum of the satisfied bits in T in unary encoding OBV-BS(F, S) Next: Mrs. Beaver WMB transformations (see the paper for more) 11/27/2024 32 PEG PDS DDI

  33. WMB: Sum-up the Weights using The Generalized Totalizer (GT) Mrs. Beaver WMB Do OBV-BS(F, T) Shuffle or Reverse T S := Sum of the weights of the satisfied bits in T in unary encoding OBV-BS(F, S) 11/27/2024 33 PEG PDS DDI

  34. WMB: Sort T by weight Mrs. Beaver WMB Sort T by weight Do OBV-BS(F, T) Shuffle or Reverse T S := Sum of the weights of the satisfied bits in T in unary encoding OBV-BS(F, S) 11/27/2024 34 PEG PDS DDI

  35. WMB: Adapt Shuffling and Reversing Mrs. Beaver WMB Sort T by weight Do OBV-BS(F, T) Shuffle or Reverse T Use weighted random shuffling Weight-oriented reverse strategy S := Sum of the weights of the satisfied bits in T in unary encoding Using the Generalized Totalizer (GT) OBV-BS(F, S) 11/27/2024 35 PEG PDS DDI

  36. WMB: Size-based Switching to Complete Part When to switch to the complete part? Mrs. Beaver: After a user-given number of iterations Improved the performance only marginally WMB: Switch after gtI iterations gtI: user-given parameter But only if the number of clauses, expected to be generated by the GT <= gtThr gtThr: user-given parameter Otherwise, stick with the incomplete part Applicable to the original Mrs. Beaver 11/27/2024 36 PEG PDS DDI

  37. Agenda for the Rest of the Talk Polarity Heuristics Variable Heuristics WMB Algorithm Experimental Results 11/27/2024 37 PEG PDS DDI

  38. Experimental Results Implemented WMB, TORC (polarity heuristic) and TSB (decision heuristic) in Intel s solver Hazel MSE18 (MaxSAT Evaluation 2018) settings Based on average score: Score for one problem: how far the solution is from the optimum, normalized to [0,1] Optimum in the paper: the best result by 6 top-performing MSE18 solvers in 24 hours Experiments: Hazel vs. the top incomplete solvers in MSE18 Polarity selection: TORC vs. conservative vs. optimistic vs. default More data in the paper: TSB impact, parameters, TORC & TSB in BMO algorithm, weakening fixing Industrial placement instances TT-Open-WBO-Inc (not in the paper) Implemented TORC and TSB in the BMO-based algorithm in Open-WBO-Inc MSE19 results available 11/27/2024 38 PEG PDS DDI

  39. Experimental Results: MSE18 Settings Solver 60 sec.: Average Score 300 sec.: Average Score Hazel 0.8616 0.9041 LinSBPS 0.8303 0.8916 Open-WBO-Inc-BMO 0.8202 0.8391 maxroster 0.7885 0.8169 11/27/2024 39 PEG PDS DDI

  40. Experimental Results: Polarity Heuristics Polarity Heuristic 60 sec.: Average Score Polarity Heuristic 300 sec.: Average Score TORC 0.8616 TORC 0.9041 Optimistic 0.8240 Conservative 0.8700 Conservative 0.8226 Optimistic 0.8499 Phase saving 0.7734 Phase saving 0.8166 11/27/2024 40 PEG PDS DDI

  41. Experimental Results: Industrial Benchmarks: Intel s placement application Isolated 7 non-incremental benchmarks Solvers: Intel s Hazel with WMB The best performing anytime solver LinSBPS The two best complete (non-anytime) solvers in MSE18 RCB2 Maxino 11/27/2024 41 PEG PDS DDI

  42. Conclusions: Complete algorithms don t suit our needs No clear winner between WMB and LinSBPS We need WMB because of incrementality Future work: integrate weight descaling from LinSBPS into WMB 11/27/2024 42 PEG PDS DDI

  43. Experimental Results: MSE19 60 sec. 300 sec. Our solver The original solver (without TORC & TSB) 11/27/2024 43 PEG PDS DDI

  44. Conclusion and Future Work Contributions: A new efficient incremental anytime MaxSAT algorithm: Weighted Mrs. Beaver (WMB) Efficient algorithm-independent heuristics for anytime MaxSAT: Polarity selection: TORC Variable selection: TSB Future work: Apply the heuristics to other SAT-based optimization problems Combine WMB with other weighted MaxSAT algorithms 11/27/2024 44 PEG PDS DDI

  45. 11/27/2024 45 PEG PDS DDI

  46. Back-up 11/27/2024 46 PEG PDS DDI

  47. TORC in LSU: Example Example: H = ( a + b) ( a + c) (a + c); T = {a,b}; w(a) = 1, w(b) = 2;H has 3 models: M1={a=1, b=0, c=1}; w(M1) = 1 M2={a=0, b=1, c=0}; w(M2) = 2 M3={a=0, b=0, c=0}; w(M3) = 0 TORC: Fix a=1 and b=1 LSU: Run the SAT solver Likely to return M1 (since variable a has the most appearances in H) TORC: Fix c=1 (since c=1 in M1) LSU: Block all the solution of weight <= 1 LSU: Run the SAT solver Will return M2 TORC: Fix c=0 (since c=0 in M2) LSU: Block all the solution of weight <= 2 LSU: Run the SAT solver Will return UNSAT LSU: Return M2 11/27/2024 47 PEG PDS DDI

  48. TORC & TSB in LSU: Example Example: H = ( a + b) ( a + c) (a + c); T = {a,b}; w(a) = 1, w(b) = 2;H has 3 models: M1={a=1, b=0, c=1}; w(M1) = 1 M2={a=0, b=1, c=0}; w(M2) = 2 M3={a=0, b=0, c=0}; w(M3) = 0 TORC: Fix a=1 and b=1 TSB: Boost the scores of a and b, where b is given a slight preference LSU: Run the SAT solver Likely to return M2 (if b has a higher score than a) TORC: Fix c=0 (since c=0 in M2) LSB: Block all the solution of weight <= 2 LSB: Run the SAT solver Will return UNSAT LSB: Return M2 11/27/2024 48 PEG PDS DDI

  49. WMB: Global Stopping Condition for OBV-BS Mrs. Beaver WMB Sort T by weight Do OBV-BS(F, T) Stop OBV-BS, if the weight of unsatisfied target bits is too high to help WMB Stop when OBV-BS can t improve the absolutely best model M, maintained by WMB, although OBV-BS can still improve the model w.r.t to its own optimization goal Enhances the original unweighted Mrs. Beaver Shuffle or Reverse T Use weighted random shuffling Weight-oriented reverse strategy S := Sum of the weights of the satisfied bits in T in unary encoding OBV-BS(F, S) 11/27/2024 49 PEG PDS DDI

Related


Daily current affairs 2024(presentation)

Daily current affairs 2024(presentation)

KD
SSC CHSL CPO 2024 (presentation)

SSC CHSL CPO 2024 (presentation)

KD
Understanding Vector Operations in Linear Algebra

Understanding Vector Operations in Linear Algebra

adira
Understanding Normed Vector Spaces for Nanotechnology Engineering

Understanding Normed Vector Spaces for Nanotechnology Engineering

reverie
Understanding Your GPA: Weighted vs. Unweighted, College Admission, and Scholarships

Understanding Your GPA: Weighted vs. Unweighted, College Admission, and Scholarships

grover
DNN Inference Optimization Challenge Overview

DNN Inference Optimization Challenge Overview

buddy
Understanding Vector Algebra and Its Applications

Understanding Vector Algebra and Its Applications

elspeth
Understanding Discrete Optimization in Mathematical Modeling

Understanding Discrete Optimization in Mathematical Modeling

heloise
Understanding Weighted Moving Average Charts for Process Monitoring

Understanding Weighted Moving Average Charts for Process Monitoring

viviana
Understanding Weighted Price Indices in Economics

Understanding Weighted Price Indices in Economics

maisie
Understanding Parallelism and Vector Instructions in CMPT 295

Understanding Parallelism and Vector Instructions in CMPT 295

julissa
Understanding Subspaces and Span of Vector Sets

Understanding Subspaces and Span of Vector Sets

zipporah
Unveiling Polarity with Polarity-Inducing Latent Semantic Analysis

Unveiling Polarity with Polarity-Inducing Latent Semantic Analysis

jwans
Effect of Weighted Sled Towing and Weighted Vest on Sprinter Acceleration Performance

Effect of Weighted Sled Towing and Weighted Vest on Sprinter Acceleration Performance

christoph
Understanding Molecular Polarity and Electronegativity in Chemistry

Understanding Molecular Polarity and Electronegativity in Chemistry

daeshawna
Understanding Polarity in Covalent Bonds

Understanding Polarity in Covalent Bonds

jord_936
Understanding Smells Through Molecular Structure: A Lesson in Polarity

Understanding Smells Through Molecular Structure: A Lesson in Polarity

goak
Choosing Between Money-Weighted Return & Time-Weighted Return in CFA Level 1 Exam

Choosing Between Money-Weighted Return & Time-Weighted Return in CFA Level 1 Exam

kierste
Understanding Cost Variants in Healthy Diets: Least Cost vs Preference Weighted

Understanding Cost Variants in Healthy Diets: Least Cost vs Preference Weighted

tabith
Fundamental Concepts in Vector Spaces and Inner Product Spaces

Fundamental Concepts in Vector Spaces and Inner Product Spaces

toee564
Understanding Vectors in AP Physics C: Mechanics

Understanding Vectors in AP Physics C: Mechanics

toms_ene
Understanding Vector Graphics in Computer Graphics

Understanding Vector Graphics in Computer Graphics

pkai

More Related Content