1. Alexandru Moșoi
  2. gasca

Commits

Alexandru Moșoi  committed bad654c

bcp: performs otf sss.

Additionally PropagateLiteral takes a bool to perform analysis.

  • Participants
  • Parent commits e0b0806
  • Branches default

Comments (0)

Files changed (4)

File lib/bcp.go

View file
  • Ignore whitespace
 // Reason a literal was propagated.
 type reason struct {
 	alive  bool    // true if literal was assigned
-	seen   bool    // used by analyze
+	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
 	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)
 		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
 		}
 
 	return false
 }
 
+func (bcp *BCP) checkConflict(ignore Literal, clause *Clause) {
+	if ignore != 0 && !bcp.reasons[ignore].alive {
+		panic("literal not assigned")
+	}
+
+	if clause != nil {
+		return
+	}
+
+	for _, lit := range clause.Literals {
+		if lit != ignore.Neg() {
+			bcp.checkConflict(lit, bcp.reasons[lit].clause)
+		}
+	}
+}
+
 // Analyzes a conflict clause.
 // For now stores the clause in bcp.Learned
 func (bcp *BCP) analyze(conflict *Clause) {
-	num := 0
+	bcp.Learned = make([]Literal, 0, 16)
+	num := 0  // number of literals at current level
+	inside := 1 // number of literals in resolvent
 	clause := conflict
-	learned := make([]Literal, 0, 16)
 	tail := len(bcp.Trail)
 	expanded := Literal(0)
 
 	for clause != nil && (expanded == 0 || num != 0) {
+		inside--
+		seenInside := 0
+
 		for _, lit := range clause.Literals {
 			reason := &bcp.reasons[lit.Neg()]
-			if lit != expanded && !reason.seen && reason.level > 0 {
+			if lit == expanded || reason.level == 0 {
+				continue
+			}
+
+			if reason.seen {
+				seenInside++
+			} else {
 				reason.seen = true
+				inside++
+
 				if reason.level == bcp.Level {
 					num++
 				} else {
-					learned = append(learned, lit)
+					bcp.Learned = append(bcp.Learned, lit)
+				}
+			}
+		}
+
+		if seenInside == inside {
+			// Performs on-the-fly-self-subsumption
+			for i, lit := range clause.Literals {
+				if lit == expanded {
+					size := len(clause.Literals) - 1
+					clause.Literals[i] = clause.Literals[size]
+					clause.Literals = clause.Literals[:size]
+					break
 				}
 			}
 		}
 		clause = bcp.reasons[expanded].clause
 		num--
 	}
-
-	learned = append(learned, bcp.Trail[tail].Neg())
-	bcp.Learned = learned
+	bcp.Learned = append(bcp.Learned, bcp.Trail[tail].Neg())
 
 	// Resets seen flags.
 	for _, lit := range bcp.Trail {
 
 // Propagates one literal.
 // Literal must not be already assigned.
-func (bcp *BCP) PropagateLiteral(literal Literal) bool {
+func (bcp *BCP) PropagateLiteral(literal Literal, analyze bool) bool {
 	if bcp.tail != len(bcp.Trail) {
 		panic("not all literals were propagated")
 	}
 	}
 
 	bcp.Level++
-	bcp.Learned = nil
 	bcp.queueUnit(literal, nil)
-	return bcp.Propagate(true)
+	return bcp.Propagate(analyze)
 }
 
 // Undoes last PropagateLiteral().

File lib/bcp_test.go

View file
  • Ignore whitespace
 			}
 
 			count++
-			if bcp.PropagateLiteral(FromDIMACS(lit)) {
+			if bcp.PropagateLiteral(FromDIMACS(lit), false) {
 				t.Error("Formula is not a contradiction:", f)
 			}
 		}
 			for j := 0; j < 2; j++ {
 				lit = lit.Neg()
 				if !bcp.IsAssigned(lit) {
-					bcp.PropagateLiteral(lit)
+					bcp.PropagateLiteral(lit, false)
 					bcp.Undo()
 				}
 			}

File lib/flp.go

View file
  • Ignore whitespace
 		}
 
 		// Negative polarity.
-		neg := bcp.PropagateLiteral(var_.Neg())
+		neg := bcp.PropagateLiteral(var_.Neg(), false)
 		for _, lit := range bcp.Trail[start:] {
 			paint[lit] = i
 		}
 		}
 
 		// Positive polarity.
-		pos := bcp.PropagateLiteral(var_.Pos())
+		pos := bcp.PropagateLiteral(var_.Pos(), false)
 		for _, lit := range bcp.Trail[start:] {
 			if paint[lit] == i {
 				extra = append(extra, lit)

File lib/search.go

View file
  • Ignore whitespace
 
 		// Propagates.
 		numProps++
-		conflict = srch.bcp.PropagateLiteral(branch)
+		conflict = srch.bcp.PropagateLiteral(branch, true)
 	}
 
 	// Returns a solution if found.
 
 	// Otherwise learns.
 	srch.bcp.UndoAll()
+	// srch.bcp.VerifyLearned()
 	if learned := srch.simplifyLearned(assignment); learned != nil {
 		srch.decider.Conflict(learned)
 		if srch.bcp.AddClause(NewClause(learned)) {