Assume() should return SAT in the case of a Propagation-complete problem.

[Mystelven]

Hello GopherSAT team.

I have either found a bug or I need an explanation on why this is not the expected behaviour.

Here is a unit test generating my strange case:

//
// ***************************************************************************************************
// @date 10/09/2020.
// @author Valentin Montmirail
//
// Here we want to test the behaviour of selectors in the following case:
//
// SUM( -sel + a + b + c +d ) <= 1
// && (sel v -a)
// && (sel v -b)
// && (sel v -c)
// && (sel v -d)
//
// In such a problem, we have two cases for our assumption: either sel is true, or it is false.
//
// [SEL is assumed to be true].
//
// 		The set of clauses ((sel v -a) && (sel v -b) && (sel v -c) && (sel v -d)) can be removed.
// 		Since they are tautological under our assumption.
// 		The problem thus becomes: SUM( a + b + c + d) <= 1. 
// 		Which is INDETERMINATE until we decided one of the truth values
// 		of either 'a', 'b', 'c' or 'd'.
//
//
// [SEL is assumed to be false].
//
// 		Then in such case, the set of clauses ((sel v -a) && (sel v -b) && (sel v -c) && (sel v -d)) becomes
// 		a set of unit clauses: (-a), (-b), (-c) and (-d). So the truth values of a,b,c and d are assigned.
//		The other constraint,  [SUM( -sel + a + b + c +d ) <= 1] becomes tautological since (-sel) equals 1.
// 		In such case, just assuming that SEL is false should already solve the problem by Unit Propagation.
//
// ***************************************************************************************************
func TestAssumptionInCardinalityConstraint(t *testing.T) {

	// Constraint will store all the constraints of our toy problem.
	constraints := make([]solver.CardConstr, 0)

	// For now, the problem is assumed to be INDETERMINATE.
	status := solver.Indet

	// We have the following variables in our problem.
	a := 1
	b := 2
	c := 3
	d := 4
	sel := 5

	sum := make([]int, 0)
	sum = append(sum, -sel)
	sum = append(sum, a)
	sum = append(sum, b)
	sum = append(sum, c)
	sum = append(sum, d)

	// constraints is thus containing: SUM( -sel + a + b + c +d ) <= 1
	constraints = append(constraints, solver.AtMost1(sum...))

	// We add the other binary clauses
	// We add (sel v -a)
	constraints = append(constraints, solver.AtLeast1(sel, -a))

	// We add (sel v -b)
	constraints = append(constraints, solver.AtLeast1(sel, -b))

	// We add (sel v -c)
	constraints = append(constraints, solver.AtLeast1(sel, -c))

	// We add (sel v -d)
	constraints = append(constraints, solver.AtLeast1(sel, -d))

	// We create the problem as a SAT problem (so we convert the cardinality constraints into clauses)
	problem := solver.ParseCardConstrs(constraints)

	// We create our solver from this set of clauses.
	solv := solver.New(problem)

	// ---------------------------------------------------------------------------------------------------
	// First case:  [SEL is assumed to be true].

	selectors := make([]solver.Lit, 1)
	selectors = append(selectors, solver.IntToLit(int32(sel)))

	// We ask the solver to assume that sel is true.
	status = solv.Assume(selectors)

	// As expected, the status should be INDETERMINATE since we still need to find a value for a, b, c and d.
	if status != solver.Indet {
		t.Error("We still need to decide the ExactlyOne constraint.")
	}

	// Obviously if we solve the problem, 
	// the solver will find a truth value for each variable and the problem becomes satisfiable.
	status = solv.Solve()
	if status != solver.Sat {
		t.Error("The ExactlyOne constraint must be satisfiable.")
	}

	// we can check the truth values of each variables.
	model := solv.Model()

	if len(model) != 5 {
		t.Error("Model: ", model)
		t.Fatal("We have a problem, we do not have a truth value for each variable.")
	}

	truthA := model[0]
	truthB := model[1]
	truthC := model[2]
	truthD := model[3]
	truthSel := model[4]

	if truthSel != true {
		t.Error("We have a problem, we have assumed sel to be true, so it must be true in the final model.")
	}

	if truthA == true {
		if (truthB || truthC || truthD) != false {
			t.Error("We have two different variables in the SUM, assigned to true.")
		}
	} else if truthB == true {
		if (truthA || truthC || truthD) != false {
			t.Error("We have two different variables in the SUM, assigned to true.")
		}
	} else if truthC == true {
		if (truthA || truthB || truthD) != false {
			t.Error("We have two different variables in the SUM, assigned to true.")
		}
	} else if truthD == true {
		if (truthA || truthB || truthC) != false {
			t.Error("We have two different variables in the SUM, assigned to true.")
		}
	} else {
		t.Error("One of the four free variables must be SET to true.")
	}

	// ---------------------------------------------------------------------------------------------------
	// Second case:  [SEL is assumed to be false].

	selectors = nil
	selectors = append(selectors, solver.IntToLit(int32(-sel)))

	// We ask the solver to assume that sel is false.
	status = solv.Assume(selectors)

	// Technically, we should solve the problem by Unit propagation, so the return of Assume should be solver.Sat
	if status != solver.Sat {
		t.Error("The ExactlyOne constraint is already satisfied... The status is for now: ", status)
	}

	// As before, if we ask the solver to solve the problem, it should be satisfiable.
	status = solv.Solve()
	if status != solver.Sat {
		t.Error("The ExactlyOne constraint must be satisfiable.")
	}

	model = solv.Model()

	if len(model) != 5 {
		t.Error("Model: ", model)
		t.Fatal("We have a problem, we do not have a truth value for each variable.")
	}

	truthA = model[0]
	truthB = model[1]
	truthC = model[2]
	truthD = model[3]
	truthSel = model[4]

	if truthSel != false {
		t.Error("We have a problem, we have assumed sel to be false, so it must be true in the final model.")
	}

	if truthA != false {
		t.Error("We have assigned a to true. But we cannot since sel is already solving the AtMostOne()")
	}

	if truthB != false {
		t.Error("We have assigned b to true. But we cannot since sel is already solving the AtMostOne()")
	}

	if truthC != false {
		t.Error("We have assigned c to true. But we cannot since sel is already solving the AtMostOne()")
	}

	if truthD != false {
		t.Error("We have assigned d to true. But we cannot since sel is already solving the AtMostOne()")
	}

	// ---------------------------------------------------------------------------------------------------
}

In this test, everything is working as expected except for one case. When we assume the selector to be false, then the problem should be considered as satisfiable after the first Unit Propagation. Unfortunately, it is not the case and the function Assume() when the selector is false returns INDETERMINATE.

Is this normal behaviour or gopherSAT deals incorrectly with selectors in the Assume() function?

[Mystelven]

poke @fdelorme !