Commits

Alexandru Moșoi  committed 5886cb4

bcp: implemented otf clause simplification.

  • Participants
  • Parent commits 8b8eb14

Comments (0)

Files changed (1)

 	alive  bool    // true if literal was assigned
 	seen   bool    // true if seen by analyzer
 	level  int     // level at which literal was assigned
-	trail  int     // position in trail
 	clause *Clause // reason for this literal
 }
 
 	watches      [][]*watch // list of watches for each literal
 	tail         int        // next to be propagated from Trail
 	numUndefined int        // number of variables
+	otfUnits     []Literal  // units discovered during otf
 }
 
-
 // A simple procedure to propagate all units.
 func PropagateUnits(formula *Formula) (bool, Reasoning) {
 	bcp := NewBCP(formula)
 	return bcp
 }
 
-func (bcp *BCP) VerifyLearned() {
-	if bcp.Level != 0 {
-		panic("verifying at non-zero level")
-	}
-
-	falsified := false
-	for _, lit := range bcp.Learned {
-		if !bcp.reasons[lit.Neg()].alive && bcp.PropagateLiteral(lit.Neg(), false) {
-			falsified = true
-			break
-		}
-	}
-
-	bcp.UndoAll()
-	if !falsified {
-		panic("not a conflict")
-	}
-}
-
 // Builds watch lists.
 func (bcp *BCP) buildWatchLists(formula *Formula) bool {
 	set := make(map[Variable]bool)
 			return true
 		}
 
-		// Deletes satisfied clauses.
-		for _, watch := range bcp.watches[unit] {
-			watch.clause.Deleted = true
-		}
-		bcp.watches[unit] = nil
-
-		// And enqueues the unit for propagation.
+		bcp.clearAssignedUnit(unit)
 		bcp.queueUnit(unit, nil)
 		return false
 	}
 	return false
 }
 
+// Deletes satisfied clauses by unit.
+func (bcp *BCP) clearAssignedUnit(unit Literal) {
+	for _, watch := range bcp.watches[unit] {
+		watch.clause.Deleted = true
+	}
+	bcp.watches[unit] = nil
+}
+
 // Queues a new unit for propagation.
 func (bcp *BCP) queueUnit(literal Literal, clause *Clause) {
 	if bcp.reasons[literal].alive {
 		panic("literal already in trail")
 	}
+	/*
+		if clause != nil && !clause.HasLiteral(literal) {
+			panic("literal not in reason")
+		}
+	*/
 
 	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)
 }
 
 
 		// Finds another, not-false, literal to watch the clause.
 		moved := false
+		hasForced := false
 		for _, other := range watches[i].clause.Literals {
-			if other == watches[i].literals[0] || other == watches[i].literals[1] {
+			if other == watches[i].literals[0] {
+				// NOTE: it is possible that literal is missing.
+				continue
+			}
+			if other == watches[i].literals[1] {
+				hasForced = true
 				continue
 			}
 			if bcp.reasons[other.Neg()].alive {
 			}
 
 			// Moves the watched clause to this non-false literal.
-			// It is possible that literal is already Trail,
+			// It is possible that literal is already in Trail,
 			// but it does not matter.
 			watches[i].literals[0] = other
 			bcp.watches[other] = append(bcp.watches[other], watches[i])
 		// Found a propagation.
 		forced := watches[i].literals[1]
 		if bcp.reasons[forced].alive {
-			// Replaces reason clause if forced not propagated yet.
-			/*
-			// TODO: this a bug
-			if bcp.reasons[forced].trail > bcp.tail && bcp.Level > 0 {
-				bcp.reasons[forced].clause = watches[i].clause
-			}
-			*/
 			continue
 		}
 
 		// Checks if a conflict was discovered.
-		if bcp.reasons[forced.Neg()].alive {
+		if bcp.reasons[forced.Neg()].alive || !hasForced {
 			if analyze {
 				bcp.analyze(watches[i].clause)
 			}
 // Analyzes a conflict clause.
 // For now stores the clause in bcp.Learned
 func (bcp *BCP) analyze(conflict *Clause) {
-	bcp.Learned = make([]Literal, 0, 16)
-	num := 0  // number of literals at current level
-	inside := 1 // number of literals in resolvent
+	bcp.Learned = make([]Literal, 0)
+	num := 0            // number of literals at current level
+	inside := 1         // number of literals in resolvent
+	simplified := false // true if clause was simplified
 	clause := conflict
 	tail := len(bcp.Trail)
 	expanded := Literal(0)
 	for clause != nil && (expanded == 0 || num != 0) {
 		inside--
 		seenInside := 0
+		simplified = false
 
 		for _, lit := range clause.Literals {
 			reason := &bcp.reasons[lit.Neg()]
 					size := len(clause.Literals) - 1
 					clause.Literals[i] = clause.Literals[size]
 					clause.Literals = clause.Literals[:size]
+					simplified = true
 					break
 				}
 			}
+
+			if !simplified {
+				panic("clause not simplified")
+			}
+
+			if len(clause.Literals) == 1 {
+				bcp.otfUnits = append(bcp.otfUnits, clause.Literals[0])
+			}
 		}
 
 		// Finds the next literal for expansion.
 	for _, lit := range bcp.Trail {
 		bcp.reasons[lit].seen = false
 	}
+
+	if simplified {
+		// if last clause was simplified, don't learn
+		// because resolvent is equal to that clause.
+		bcp.Learned = nil
+	}
 }
 
 // Performs all units propagations.
 	}
 }
 
+// Propagates all otf units discovered during clause simplification.
+func (bcp *BCP) PropagateOTFUnits() bool {
+	if bcp.Level != 0 {
+		panic("can propagete otf units only at top level")
+	}
+
+	for _, unit := range bcp.otfUnits {
+		if !bcp.reasons[unit].alive {
+			bcp.clearAssignedUnit(unit)
+			bcp.queueUnit(unit, nil)
+		}
+	}
+
+	bcp.otfUnits = bcp.otfUnits[:0]
+	return bcp.Propagate(false)
+}
+
 // Returns true if literal is Trail.
 func (bcp *BCP) IsAssigned(literal Literal) bool {
 	return bcp.reasons[literal].alive