Commits

Alexandru Moșoi committed 60630bb

bcp: choose better literal reason.

  • Participants
  • Parent commits 75c26a1

Comments (0)

Files changed (1)

 	alive  bool    // true if literal was assigned
 	seen   bool    // used by analyze
 	level  int     // level at which literal was assigned
+	trail  int     // position in trail
 	clause *Clause // reason for this literal
 }
 
 	bcp.reasons[literal].alive = true
 	bcp.reasons[literal].level = bcp.Level
 	bcp.reasons[literal].clause = clause
+	bcp.reasons[literal].trail = len(bcp.Trail)
 	bcp.Trail = append(bcp.Trail, literal)
 }
 
 
 			// Moves the watched clause to this non-false literal.
 			// It is possible that literal is already Trail,
-			// but it doesn't matter.
+			// but it does not matter.
 			watches[i].literals[0] = other
 			bcp.watches[other] = append(bcp.watches[other], watches[i])
 			numWatches--
 		// Found a propagation.
 		forced := watches[i].literals[1]
 		if bcp.reasons[forced].alive {
+			// Replaces reason clause if forced not propagated yet.
+			if bcp.reasons[forced].trail > bcp.tail && bcp.Level > 0 {
+				bcp.reasons[forced].clause = watches[i].clause
+			}
 			continue
 		}