Body: <p>I encountered a question about solving CNF SAT using reinforcement learning: A state is a partial substitution to the variables, and each action is choosing an empty variable and set its value (to <code>True</code> or <code>False</code>). If the formula is satisfied the reward is 2, and if it's not, the reward is 0. The discount factor is <span class="math-container">$\gamma \in (0, 1)$</span></p>
  <p>Does Q-Learning can solve the problem and converge to an optimal plan for any CNF formula? and what about other RL algorithms?</p>
  <p>I think it will converge, but I am not sure if I am right.</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2023-02-24T04:02:43.130Z
Comments.Text: So long as this can be modeled as a MDP process with finite state and action spaces, by TD based Q-learning's convergence theorem based upon stochastic approximation theory it's provably convergent albeit may be very slow since its combinatoric state space could be huge while reward is extremely sparse (need some heuristic search help such as A* or SAT solver or add some intermediate reward shape) and SAT is the first known NP-complete problem. But what makes you doubt it cannot be modeled as model-free RL?
Comments.UserDisplayName: cinch
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2024-08-02T21:18:53.507Z
Comments.Text: I've seen machine learning used for "Automated Configuration and Selection of SAT Solvers", ch. 12 of [_Handbook of Satisfiability_](https://isidore.co/calibre/#panel=book_details&book_id=6907).
Comments.UserDisplayName: Geremia
Tags: <reinforcement-learning><convergence><satisfiability><conjunctive-normal-form>
Title: Can Q-learning and other RL algorithms solve CNF SAT?
UserDisplayName: Dani
ThreadText: # Can Q-learning and other RL algorithms solve CNF SAT?
  
  (Asked by: username_0 on 2023-02-19)
  
  I encountered a question about solving CNF SAT using reinforcement learning: A state is a partial substitution to the variables, and each action is choosing an empty variable and set its value (to `True` or `False`). If the formula is satisfied the reward is 2, and if it's not, the reward is 0. The discount factor is $\gamma \in (0, 1)$
  
  Does Q-Learning can solve the problem and converge to an optimal plan for any CNF formula? and what about other RL algorithms?
  
  I think it will converge, but I am not sure if I am right.
  
  **Tags:** reinforcement-learning, convergence, satisfiability, conjunctive-normal-form
  
  > **Comments:**
  > **username_1**: So long as this can be modeled as a MDP process with finite state and action spaces, by TD based Q-learning's convergence theorem based upon stochastic approximation theory it's provably convergent albeit may be very slow since its combinatoric state space could be huge while reward is extremely sparse (need some heuristic search help such as A* or SAT solver or add some intermediate reward shape) and SAT is the first known NP-complete problem. But what makes you doubt it cannot be modeled as model-free RL?  
  > **username_2**: I've seen machine learning used for "Automated Configuration and Selection of SAT Solvers", ch. 12 of [_Handbook of Satisfiability_](https://isidore.co/calibre/#panel=book_details&book_id=6907).  
  
  ---
  
  ## 0 answers
  
  