Linear Arithmetic Satisfiability Game Strategies

quantified linear arithmetic satisfiability n.w
1 / 72
Embed
Share

Delve into the world of linear arithmetic satisfiability game strategies, exploring the concepts of quantified linear arithmetic, first-order logic terms, and rational arithmetic. Uncover the dynamics of SAT vs. UNSAT scenarios and the interplay of demonic and angelic choices in the realm of satisfiability.

  • Linear Arithmetic
  • Satisfiability Game
  • Logic Strategies
  • Quantified Arithmetic
  • SAT-UNSAT
rayaanacharya
ibr_kus Follow

Uploaded on | 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. 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.

Download 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.

E N D

Presentation Transcript

  1. Quantified Linear Arithmetic Satisfiability via Fine-Grained Strategy Improvement Charlie Murphy University of Wisconsin-Madison Zachary Kincaid Princeton University July 24, 2024

  2. First Order Logic Terms ? ? | ? ?1, ,??? ? ?,? ? ?1, ,??? ? | ? ?1, ,??? ? Formulas ?:?.? ? ? | ? ? | ?:?.? Negation Normal Form

  3. Linear Rational Arithmetic Terms ? ? | ? ?1+ ?2 ? ? ?,? t1< t2 ?: .? ? ? | ?1 ?2| ?: .? Formulas | ? ? Negation Normal Form

  4. Satisfiability ? ? Formula with free variables X Model of free variables ? ??? ?

  5. Satisfiability Game SAT UNSAT Controls Demonic Choice Universal Quantifiers, Conjunction Controls Angelic Choice Existential Quantifiers, Disjunction

  6. Satisfiability Game SAT UNSAT ? ?

  7. Satisfiability Game SAT UNSAT ?(?,?) State of the game

  8. Satisfiability Game ?,?. ? < ? ?. ? < ? < ? SAT UNSAT Density Property of Rationals

  9. Satisfiability Game ?( , ?,?. ? < ? ?. ? < ? < ?) SAT UNSAT

  10. Satisfiability Game ?( , ?,?. ? ? ?. ? < ? ? < ? SAT UNSAT Rewrite to negation normal form

  11. Satisfiability Game ?( , ?,?. ? ? ?. ? < ? ? < ? SAT UNSAT Controlled by SAT

  12. Satisfiability Game ?( , ?,?. ? ? ?. ? < ? ? < ? SAT UNSAT Controlled by UNSAT

  13. Satisfiability Game ?,?. ? , SAT UNSAT ? ? ? ? < ? ? < ? Represent formula as abstract syntax tree (AST)

  14. Satisfiability Game UNSAT s choice ?,?. SAT UNSAT Choose: ? 0 ? 1 ? ? ? ? < ? ? < ? Sequence of actions played so far (by either player). Play: 0 1

  15. Satisfiability Game SAT s choice SAT Choose right UNSAT ? 0 ? 1 ? ? ? ? < ? ? < ? Play: 0 1 R Play: 0 1

  16. Satisfiability Game SAT s choice ? SAT Choose: ? 1 UNSAT ? 0 ? 1 ? < ? ? < ? 2 Play: 0 1 R 1 Play: 0 1 R 2

  17. Satisfiability Game UNSAT s choice ? 0 ? 1 SAT UNSAT Choose left ? 1 2 ? < ? ? < ? Play: 0 1 R 1 Play: 0 1 R 1 2 L 2

  18. Satisfiability Game ? 0 ? 1 SAT UNSAT ? 1 2 ? < ? The chosen model satisfies the chosen atom. SATwins. Play: 0 1 R 1 2 L

  19. Strategies maps from states of the game thatSAT controls to SAT s next move: L or R for disjunctions a rational value to instantiate an existential quantifier. ?SAT :

  20. Strategies ?SATM,z x ?. ? < ? ? < ? if ? ? ? ? then ? else ? ? ? + ? ? 2 ?SATM, ?. ? < ? ? < ? The formula must be satisfiable ?SAT is a winning strategy: If SATplays according to ?SAT, then SAT will win any play regardless of the choices made by UNSAT.

  21. How do we compute a winning strategy?

  22. Strategy Skeletons SAT Skeleton ? ?: ?: ?,?. ? ? ? ? ? ? ? ? ? ?+? 2 ? ? < ? ? < ? ? ? ? < ? ? < ? Represents a non-deterministic collection of SAT Strategies whose structure closely follows ?

  23. Strategy Improvement SAT Skeleton ?0 ?: ?: Start with an arbitrary SAT skeleton ?,?. ? ? Is it winning? ? ? ? ? ? ? ? < ? ? < ?

  24. Winning Formula Winning formula of ?0 ? ? ?: ?: ?,?. ?. ?.? ? ? ? ? Herbandize ?.? ? ? ? ? ? ? ? ? ? ? Valid if and only if ?0is winning ? < ? ? < ?

  25. Winning Formula Winning formula of ?0 ? 0 ? 1 ?: ?: ?0 ?,?. ? < ? ? ? ? Satisfiable if and only if ?? is losing ? < ? ? < ?

  26. Strategy Improvement SAT Skeleton ?0 ?: ?: ?,?. ? ? ? ? ? ? ? ? ?? has a counter-strategy ?? is not winning ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0)

  27. Computing a Counter-Strategy

  28. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ?: ?,?. ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0)

  29. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ?: ?,?. ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0)

  30. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0)

  31. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0)

  32. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0)

  33. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) Keeps track of what conditions under which?? beats?? ? ? < ?

  34. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) ? ? < ?

  35. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) ?0has no strategy for this branch ? ? < ?

  36. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) ? ? < ? Choose any strategy ?0has no strategy for this branch ? ? < ? ????

  37. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) ? ? < ? Combine Sub-strategies ? ? < ? ????

  38. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) ? ? < ? ? ? < ?

  39. Model-based Term Selection

  40. Term Selection UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: Need to find a term to substitute for? ?,?. ? ? ? ? At least by model ? ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) ? ? < ? That ensures ? Is satisfied ? ? < ?

  41. Term Selection ? ?????? ?,?,? Find a ? such that: FV ? ?? ? ? If ? ? then ? ?[? ?]

  42. LRA Term Selection Pick ? such that M ? = ? and ? = ? is a sub-formula of G ?? ?,?,? 1 2??? ?,?,? +???(?,?,?) ??? ?,?,? + 1 ??? ?,?,? 1 0 ?????? ?,?,?

  43. LRA Term Selection ?? ?,?,? 1 2??? ?,?,? +???(?,?,?) ??? ?,?,? + 1 ??? ?,?,? 1 0 Pick ? such that M ? < ? ? < ? is a sub-formula of G There is no ? such that M ? < ? ? < ? is a sub-formula of G ? ? < ? ?????? ?,?,?

  44. LRA Term Selection ?? ?,?,? 1 2??? ?,?,? +???(?,?,?) ??? ?,?,? + 1 ??? ?,?,? 1 0 Pick ? such that M ? < ? ? < ? is a sub-formula of G There is no ? such that M ? < ? ? < ? is a sub-formula of G ? ? < ? ?????? ?,?,?

  45. LRA Term Selection ?? ?,?,? 1 2??? ?,?,? +???(?,?,?) ??? ?,?,? + 1 ??? ?,?,? 1 0 ?????? ?,?,? ? does not appear in G

  46. LRA Term Selection ?????? ?,? 0 ? 1,? < ? ? + 1

  47. Computing a Counter Strategy

  48. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ? 1 ?: ?,?. ? ? ? ? + 1 ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) ? ? < ? ? ? < ?

  49. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ? 0 ?: ?,?. ? ? ? ? ? ? + 1 ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) ? ? < ? ? ? < ? + 1

  50. Counter Strategy UNSAT Skeleton ?0 SAT Skeleton ?0 ?: ?: ?,?. 0 ? ? ? ? ? + 1 ? ? ? ? ? ? ? ? ? ? ? ? < ? ? < ? ? 0 ? 1 ?0 ????(?,?0) ? ? < ? ? ????

Related


No related presentations.

More Related Content