From ffea4d8cf97138ddf2b1f9425d110cd8d322e5a0 Mon Sep 17 00:00:00 2001 From: Ettore Di Giacinto Date: Wed, 28 Oct 2020 17:58:43 +0100 Subject: [PATCH] Fix priority constraint formula The parallel solver made the issue more visible, the constraints needed to be less relaxed and needed to be exclusive so our candidate is looked up at it first --- pkg/package/package.go | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkg/package/package.go b/pkg/package/package.go index 6e1b41c7..ebcb61e0 100644 --- a/pkg/package/package.go +++ b/pkg/package/package.go @@ -656,7 +656,7 @@ func (pack *DefaultPackage) buildFormula(definitiondb PackageDatabase, db Packag C = bf.Var(encodedC) // Or the Candidate is true, or all the others might be not true // This forces the CDCL sat implementation to look first at a solution with C=true - formulas = append(formulas, bf.Or(bf.Not(A), bf.Or(bf.Or(C, bf.Or(priorityConstraints...)), bf.Or(bf.Not(C), bf.Or(priorityALO...))))) + formulas = append(formulas, bf.Or(bf.Not(A), bf.Or(bf.And(C, bf.Or(priorityConstraints...)), bf.And(bf.Not(C), bf.Or(priorityALO...))))) } // AMO - At most one