@@ -238,7 +238,7 @@ def pl_true(exp, model={}):
238238    and False if it is false. If the model does not specify the value for 
239239    every proposition, this may return None to indicate 'not obvious'; 
240240    this may happen even when the expression is tautological.""" 
241-     if  exp  ==   True   or   exp   ==   False :
241+     if  exp  in  ( True ,  False ) :
242242        return  exp 
243243    op , args  =  exp .op , exp .args 
244244    if  is_prop_symbol (op ):
@@ -639,7 +639,7 @@ def inspect_literal(literal):
639639def  WalkSAT (clauses , p = 0.5 , max_flips = 10000 ):
640640    """Checks for satisfiability of all clauses by randomly flipping values of variables 
641641    """ 
642-     # set  of all symbols in all clauses 
642+     # Set  of all symbols in all clauses 
643643    symbols  =  set (sym  for  clause  in  clauses  for  sym  in  prop_symbols (clause ))
644644    # model is a random assignment of true/false to the symbols in clauses 
645645    model  =  {s : random .choice ([True , False ]) for  s  in  symbols }
@@ -655,14 +655,14 @@ def WalkSAT(clauses, p=0.5, max_flips=10000):
655655        else :
656656            # Flip the symbol in clause that maximizes number of sat. clauses 
657657            def  sat_count (sym ):
658-                 #returns  the the number of clauses satisfied after flipping the symbol 
658+                 # Return  the the number of clauses satisfied after flipping the symbol.  
659659                model [sym ] =  not  model [sym ]
660660                count  =  len ([clause  for  clause  in  clauses  if  pl_true (clause , model )])
661661                model [sym ] =  not  model [sym ]
662662                return  count 
663663            sym  =  argmax (prop_symbols (clause ), key = sat_count )
664664        model [sym ] =  not  model [sym ]
665-     #If no solution is found within the flip limit, we return failure 
665+     #  If no solution is found within the flip limit, we return failure 
666666    return  None 
667667
668668# ______________________________________________________________________________ 
@@ -686,71 +686,71 @@ def SAT_plan(init, transition, goal, t_max, SAT_solver=dpll_satisfiable):
686686    """Converts a planning problem to Satisfaction problem by translating it to a cnf sentence. 
687687    [Figure 7.22]""" 
688688
689-     #Functions used by SAT_plan 
689+     #  Functions used by SAT_plan 
690690    def  translate_to_SAT (init , transition , goal , time ):
691691        clauses  =  []
692692        states  =  [state  for  state  in  transition ]
693693
694-         #Symbol claiming state s at time t 
694+         #  Symbol claiming state s at time t 
695695        state_counter  =  itertools .count ()
696696        for  s  in  states :
697697            for  t  in  range (time + 1 ):
698-                 state_sym [( s , t ) ] =  Expr ("State_{}" .format (next (state_counter )))
698+                 state_sym [s , t ] =  Expr ("State_{}" .format (next (state_counter )))
699699
700-         #Add initial state axiom 
700+         #  Add initial state axiom 
701701        clauses .append (state_sym [init , 0 ])
702702
703-         #Add goal state axiom 
703+         #  Add goal state axiom 
704704        clauses .append (state_sym [goal , time ])
705705
706-         #All possible transitions 
706+         #  All possible transitions 
707707        transition_counter  =  itertools .count ()
708708        for  s  in  states :
709709            for  action  in  transition [s ]:
710710                s_  =  transition [s ][action ]
711711                for  t  in  range (time ):
712-                     #Action 'action' taken from state 's' at time 't' to reach 's_' 
713-                     action_sym [( s , action , t ) ] =  Expr ("Transition_{}" .format (next (transition_counter )))
712+                     #  Action 'action' taken from state 's' at time 't' to reach 's_' 
713+                     action_sym [s , action , t ] =  Expr ("Transition_{}" .format (next (transition_counter )))
714714
715715                    # Change the state from s to s_ 
716716                    clauses .append (action_sym [s , action , t ] | '==>' |  state_sym [s , t ])
717717                    clauses .append (action_sym [s , action , t ] | '==>' |  state_sym [s_ , t  +  1 ])
718718
719-         #Allow only one state at any time 
719+         #  Allow only one state at any time 
720720        for  t  in  range (time + 1 ):
721-             #must be a state at any time 
722-             clauses .append (associate ('|' , [  state_sym [s , t ] for  s  in  states   ]))
721+             #  must be a state at any time 
722+             clauses .append (associate ('|' , [state_sym [s , t ] for  s  in  states ]))
723723
724724            for  s  in  states :
725725                for  s_  in  states [states .index (s )+ 1 :]:
726-                     #for each pair of states s, s_ only one is possible at time t 
726+                     #  for each pair of states s, s_ only one is possible at time t 
727727                    clauses .append ((~ state_sym [s , t ]) |  (~ state_sym [s_ , t ]))
728728
729-         #Restrict to one transition per timestep 
729+         #  Restrict to one transition per timestep 
730730        for  t  in  range (time ):
731-             #list of possible transitions at time t 
731+             #  list of possible transitions at time t 
732732            transitions_t  =  [tr  for  tr  in  action_sym  if  tr [2 ] ==  t ]
733733
734-             #make sure atleast  one of the transition  happens 
735-             clauses .append (associate ('|' , [  action_sym [tr ] for  tr  in  transitions_t   ]))
734+             #  make sure at least  one of the transitions  happens 
735+             clauses .append (associate ('|' , [action_sym [tr ] for  tr  in  transitions_t ]))
736736
737737            for  tr  in  transitions_t :
738738                for  tr_  in  transitions_t [transitions_t .index (tr ) +  1  :]:
739-                     #there cannot be two transitions tr and tr_ at time t 
740-                     clauses .append (( ~ action_sym [tr ])  |  ( ~ action_sym [tr_ ]) )
739+                     #  there cannot be two transitions tr and tr_ at time t 
740+                     clauses .append (~ action_sym [tr ] |  ~ action_sym [tr_ ])
741741
742-         #Combine the clauses to form the cnf 
742+         #  Combine the clauses to form the cnf 
743743        return  associate ('&' , clauses )
744744
745745    def  extract_solution (model ):
746-         true_transitions  =  [  t  for  t  in  action_sym  if  model [action_sym [t ]]]
747-         #Sort transitions based on time which is the 3rd element of the tuple 
746+         true_transitions  =  [t  for  t  in  action_sym  if  model [action_sym [t ]]]
747+         #  Sort transitions based on time,  which is the 3rd element of the tuple 
748748        true_transitions .sort (key  =  lambda  x : x [2 ])
749-         return  [  action  for  s , action , time  in  true_transitions   ]
749+         return  [action  for  s , action , time  in  true_transitions ]
750750
751-     #Body of SAT_plan algorithm 
751+     #  Body of SAT_plan algorithm 
752752    for  t  in  range (t_max ):
753-         #dcitionaries  to help extract the solution from model 
753+         # dictionaries  to help extract the solution from model 
754754        state_sym  =  {}
755755        action_sym  =  {}
756756
@@ -1062,5 +1062,3 @@ def simp(x):
10621062def  d (y , x ):
10631063    "Differentiate and then simplify." 
10641064    return  simp (diff (y , x ))
1065- 
1066- 
0 commit comments