SearchForAllSolutions in CP-SAT returns same solution repeatedly

[jeremydover]

What version of OR-Tools and what language are you using? Version: 9.5.2237 Language: Python

Which solver are you using (e.g. CP-SAT, Routing Solver, GLOP, BOP, Gurobi) CP-SAT

What operating system (Linux, Windows, ...) and version? Windows 11

What did you do? Steps to reproduce the behavior:

1. Execute this code: isolate.txt

from __future__ import print_function
from __future__ import print_function
import sys
import math
import colorama
from ortools.sat.python import cp_model
from array import *
from colorama import Fore,Back,init
init()

class SolutionPrinter(cp_model.CpSolverSolutionCallback):
    """Print intermediate solutions."""
    def __init__(self, variables):
        cp_model.CpSolverSolutionCallback.__init__(self)
        self.__variables = variables
        self.__solution_count = 0
        self.__printAll = False
        self.__debug = False
        self.__testMode = False
        self.__testStringArray = []

    def setPrintAll(self):
        self.__printAll = True

    def setDebug(self):
        self.__debug = True

    def setTestMode(self):
        self.__testMode = True

    def TestString(self):
        return ''.join(sorted(self.__testStringArray))

    def OnSolutionCallback(self):
        self.__solution_count += 1
        cntr = 0

        if self.__testMode is True:
            self.__testStringArray.append(''.join(map(str,[self.Value(v) for v in self.__variables])))

        elif self.__printAll is True:
            if self.__debug is False:
                for v in self.__variables:
                    print('%i' % (self.Value(v)), end = ' ')
                    cntr += 1
                    if cntr == 9:
                        print ()
                        cntr = 0
                print()
            else:
                for v in self.__variables:
                    print('%s=%i' % (v,self.Value(v)))

    def SolutionCount(self):
        return self.__solution_count

class sudoku:
    """A class used to create a square Sudoku puzzle with variable size,
       though 3x3 is the default and best (only?) tested use case.

       Constants
       =========
        Row/Col - can specify a row/column to indicate whether a clue,
                    typically given outside the grid, applies to a row or
                    column. Usually only one choice, but needed for (literally)
                    the corner cases.

        V/X    - specifies type of XV or XVXV Sudoku clue is used

        White/Black - same as XV, but for Kropkis

        Horz/Vert - clues that go on edges are usually specified with the
                    grid of the top/left most cell, and then an H or V to
                    determine whether the clue is on the right (H) or bottom (V)
                    edge

        Location Specifications
        =======================
        Cells are specified by coordinates, with (0,0) at top left, (8,8) at bottom right
        First coordinate is the row, so a change causes vertial motion.

        Quads are specified analogously, on a (0,0) to (7,7) basis.

        Lines are specified as lists of cells. Order within the list usually matters, unless
        it does not matter for the underlying constraint.

        There are a whole fistful of methods, so I'm going to have to figure out a better way
        to document
    """

    Row = 0     #Constant to pass to indicate row/column
    Col = 1     #Constant to pass to indicate row/column

    V = 0       #Constant to distinguish XV sudoku clues
    X = 1       #Constant to distinguish XV sudoku clues

    White = 0   #Constant to distinguish Kropki clues
    Black = 1   #Constant to distinguish Kropki clues

    Horz = 0    #Constant to determine clues going horizontally/vertically
    Vert = 1    #Constant to determine clues going horizontally/vertically

    Min = 0     #Constant to determine whether min/max clues are mins or maxs
    Max = 1     #Constant to determine whether min/max clues are mins or maxs

    Even = 0    # Constant to determine whether parity constraint is even or odd
    Odd = 1     # Constant to determine whether parity constraint is even or odd

    Top = 0     # Constant to determine direction arrow on 2x2 points...note code assumes this value is the same as Left
    Bottom = 1  # Constant to determine direction arrow on 2x2 points
    Left = 2    # Constant to determine direction arrow on 2x2 points
    Right = 3   # Constant to determine direction arrow on 2x2 points
    Up = 0      # Constant for Rossini clues
    Down = 1    # Constant for Rossini clues

    Corner = 0  # Constant to determine clue type for corner/edge clues
    Edge = 1    # Constant to determine clue type for corner/edge clues

    def __init__(self,boardSizeRoot,irregular=None,digitSet=None,model=None):
        self.boardSizeRoot = boardSizeRoot
        self.boardWidth = boardSizeRoot*boardSizeRoot

        self.isBattenburgInitialized = False
        self.isBattenburgNegative = False

        self.isKropkiInitialized = False
        self.isKropkiNegative = False
        self.kropkiDiff = 1
        self.kropkiRatio = 2

        self.isFriendlyInitialized = False
        self.isFriendlyNegative = False

        self.isRossiniInitialized = False
        self.isRossiniNegative = False
        self.rossiniLength = -1

        self.isXVInitialized = False
        self.isXVNegative = False

        self.isXVXVInitialized = False
        self.isXVXVNegative = False

        self.isEntropyQuadInitialized = False
        self.isEntropyQuadNegative = False

        self.isModularQuadInitialized = False
        self.isModularQuadNegative = False

        self.isEntropyBattenburgInitialized = False
        self.isEntropyBattenburgNegative = False

        self.isConsecutiveQuadInitialized = False
        self.isConsecutiveQuadNegative = False

        self.isParityQuadInitialized = False
        self.isParityQuadNegative = False

        self.isParity = False
        self.isEntropy = False
        self.isModular = False
        self.isFullRank = False

        if digitSet is None:
            self.digits = {x for x in range(1,self.boardWidth+1)}
        else:
            self.digits = digitSet
        self.maxDigit = max(self.digits)
        self.minDigit = min(self.digits)
        self.digitRange = self.maxDigit - self.minDigit

        if model is None:
            self.model = cp_model.CpModel()
        else:
            self.model = model
        self.cellValues = []
        self.allVars = []
        self.candTests = [[[None for k in range(len(self.digits))] for j in range(self.boardWidth)] for i in range(self.boardWidth)]
        self.candToExclude=[]

        # Create the variables containing the cell values
        for rowIndex in range(self.boardWidth):
            tempArray = []
            for colIndex in range(self.boardWidth):
                tempCell = self.model.NewIntVar(self.minDigit,self.maxDigit,'cellValue{:d}{:d}'.format(rowIndex,colIndex))
                if (self.maxDigit - self.minDigit) >= self.boardWidth:  #Digit set is not continguous, so force values
                    self.model.AddAllowedAssignments([tempCell],[(x,) for x in digitSet])
                tempArray.append(tempCell)
                self.allVars.append(tempCell)
            self.cellValues.insert(rowIndex,tempArray)

        # Create rules to ensure rows and columns have no repeats
        for rcIndex in range(self.boardWidth):
            self.model.AddAllDifferent([self.cellValues[rcIndex][crIndex] for crIndex in range(self.boardWidth)])   # Rows
            self.model.AddAllDifferent([self.cellValues[crIndex][rcIndex] for crIndex in range(self.boardWidth)])   # Columns

        # Now deal with regions. Default to boxes...leaving stub for irregular Sudoku for now
        self.regions = []
        if irregular is None:
            self.__setBoxes()

    def __setBoxes(self):
        # Create rules to ensure boxes have no repeats
        for rowBox in range(self.boardSizeRoot):
            for colBox in range(self.boardSizeRoot):
                tempCellArray = []
                tempCellIndexArray = []
                for rowIndex in range(self.boardSizeRoot):
                    for colIndex in range(self.boardSizeRoot):
                        tempCellArray.append(self.cellValues[self.boardSizeRoot*rowBox+rowIndex][self.boardSizeRoot*colBox+colIndex])
                        tempCellIndexArray.append((self.boardSizeRoot*rowBox+rowIndex,self.boardSizeRoot*colBox+colIndex))
                self.model.AddAllDifferent(tempCellArray)                   # Squares
                self.regions.append(tempCellIndexArray)

    def __setIndexCell(self,row,col,rc):
        # This is the atomic call to set an index condition. Dealing with whether it's a whole row, whether or not there's a negative
        # constraint is dealt with higher level functions. This is not generally meant to be set outside the class.
        # row,col is exactly what you think
        # rc determines whether the cell is indexing its row or its column: 0 -> row, 1 -> column

        hStep = 0 if rc == sudoku.Col else 1
        vStep = 0 if rc == sudoku.Row else 1        
        target = row+1 if rc == sudoku.Col else col+1
        varBitmap = self.__varBitmap('IndexRow{:d}Col{:d}'.format(row,col),self.boardWidth)
        self.allVars = self.allVars + varBitmap[0]

        for k in range(self.boardWidth):
            self.model.Add(self.cellValues[row][col] == k+1).OnlyEnforceIf(varBitmap[k])
            self.model.Add(self.cellValues[row*hStep+k*vStep][col*vStep+k*hStep] == target).OnlyEnforceIf(varBitmap[k])

    def __setNonIndexCell(self,row,col,rc):
        # This is the atomic call to set a negative constraint on an index condition. Dealing with whether it's a whole row, whether
        # or not there's a negative constraint is dealt with higher level functions. This is not generally meant to be set outside the class.
        # row,col is exactly what you think
        # rc determines whether the cell is indexing its row or its column: 0 -> row, 1 -> column

        hStep = 0 if rc == sudoku.Col else 1
        vStep = 0 if rc == sudoku.Row else 1        
        target = row+1 if rc == sudoku.Col else col+1
        varBitmap = self.__varBitmap('IndexRow{:d}Col{:d}'.format(row,col),self.boardWidth-1)
        self.allVars = self.allVars + varBitmap[0]

        varTrack = 0
        for k in range(self.boardWidth):
            if k+1 == target:
                self.model.Add(self.cellValues[row*hStep+k*vStep][col*vStep+k*hStep] != target)
            else:
                self.model.Add(self.cellValues[row][col] == k+1).OnlyEnforceIf(varBitmap[varTrack])
                self.model.Add(self.cellValues[row*hStep+k*vStep][col*vStep+k*hStep] != target).OnlyEnforceIf(varBitmap[varTrack])
                varTrack = varTrack + 1

    def setIndexColumn(self,col1,neg=False,inlist1=[]):
        # This sets up an indexing column. Each cell indexes the *row* so don't be surprised when we call 
        # the cell method with rc=0.
        # Row is the column number
        # neg is whether or not there is a negative constraint on cells not in the index list
        # inlist is the list of cells that index vs. not index in the negative constraint scenario

        # Convert 1-base to 0-base
        col0 = col1 - 1
        if len(inlist1) == 0:
            if neg is True:
                inlist0 = []
            else:
                inlist0 = [x for x in range(self.boardWidth)]
        else:
            inlist0 = [x-1 for x in inlist1]

        for i in range(self.boardWidth):
            if i in inlist0:
                self.__setIndexCell(i,col0,sudoku.Row)
            elif neg is True:   
                self.__setNonIndexCell(i,col0,sudoku.Row)

    def setKropkiWhite(self,row,col=-1,hv=-1):
        if col == -1:
            (row,col,hv) = self.__procCell(row)
        if self.isKropkiInitialized is not True:
            self.kropkiCells = [(row,col,hv)]
            self.isKropkiInitialized = True
        else:
            self.kropkiCells.append((row,col,hv))
        # Note: row,col is the top/left cell of the pair, hv = 0 -> horizontal, 1 -> vertical
        bit = self.model.NewBoolVar('KropkiWhiteBiggerDigitRow{:d}Col{:d}HV{:d}'.format(row,col,hv))
        self.allVars.append(bit)
        self.model.Add(self.cellValues[row][col] - self.cellValues[row+hv][col+(1-hv)] == self.kropkiDiff).OnlyEnforceIf(bit)
        self.model.Add(self.cellValues[row][col] - self.cellValues[row+hv][col+(1-hv)] == -1*self.kropkiDiff).OnlyEnforceIf(bit.Not())

    def setKropkiBlack(self,row,col=-1,hv=-1):
        if col == -1:
            (row,col,hv) = self.__procCell(row)
        if self.isKropkiInitialized is not True:
            self.kropkiCells = [(row,col,hv)]
            self.isKropkiInitialized = True
        else:
            self.kropkiCells.append((row,col,hv))
        # Note: row,col is the top/left cell of the pair, hv = 0 -> horizontal, 1 -> vertical
        bit = self.model.NewBoolVar('KropkiBlackBiggerDigitRow{:d}Col{:d}HV{:d}'.format(row,col,hv))
        self.allVars.append(bit)
        self.model.Add(self.cellValues[row][col] == self.kropkiRatio*self.cellValues[row+hv][col+(1-hv)]).OnlyEnforceIf(bit)
        self.model.Add(self.kropkiRatio*self.cellValues[row][col] == self.cellValues[row+hv][col+(1-hv)]).OnlyEnforceIf(bit.Not())

    def setKropkiWhiteArray(self,cells):
        for x in cells: self.setKropkiWhite(x)

    def setKropkiBlackArray(self,cells):
        for x in cells: self.setKropkiBlack(x)

    def setKropkiDifference(self,diff=1):
        # Sets the difference used in all subseqequent white Kropki dots
        self.kropkiDiff = diff

    def setKropkiRatio(self,ratio=2):
        # Sets the ratio used in all subseqequent black Kropki dots
        self.kropkiRatio = ratio

    def setGammaEpsilon(self):
        self.setKropkiDifference(5)
        self.setKropkiRatio(3)

    def __varBitmap(self,string,num):
        # Utility function to create a list of Boolean variable propositions that encode num possibilities exactly.
        # string is used to label the variables
        # Implements model constraints to ensure "extra"

        n = math.ceil(math.log(num,2))
        bits = []
        for i in range(n):
            bits.append(self.model.NewBoolVar(string + 'BM{:d}'.format(i)))

        # Create full array of first n-1 variables. We need them all.
        var = [[bits[0]],[bits[0].Not()]]
        for i in range(1,n-1):
            for j in range(len(var)):
                var.append(var[j] + [bits[i].Not()])
                var[j].append(bits[i])

        # We repeat the same procedure, except when we are done, instead of appending new variable lists.
        # we create constraints to ensure these cases cannot happen

        for j in range(len(var)):
            if len(var) < num:
                var.append(var[j] + [bits[-1].Not()])
            else:
                # This ensures an unused combination of variables cannot occur
                #self.model.AddBoolAnd([bits[-1]]).OnlyEnforceIf(var[j] + [bits[-1].Not()])
                self.model.AddBoolAnd(var[j] + [bits[-1]]).OnlyEnforceIf(var[j] + [bits[-1].Not()])

            # Either way append to existing lists
            var[j].append(bits[-1])

        return var

    def __procCell(self,cell):
        # Utility function that processes an individual cell into a tuple format

        # Note: This function assumes that the first two elements are a row/column index, 1-base
        # so it converts them to 0-base.

        if type(cell) is tuple:
            myCell = cell 
        elif type(cell) is str:
            myCell = tuple(map(int,list(cell)))
        elif type(cell) is int:
            myCell = tuple(map(int,list(str(cell))))

        return tuple([myCell[i]-1 for i in range(2)] + [myCell[i] for i in range(2,len(myCell))])

    def __procCellList(self,inlist):
        # Utility function to process a list from one of several input formats into the tuple format
        # required by our functions
        return list(map(lambda x: self.__procCell(x),inlist))

    def countSolutions(self,printAll = False,debug = False,test=False):
        self.solver = cp_model.CpSolver()
        consolidatedCellValues = []
        for tempArray in self.cellValues: consolidatedCellValues = consolidatedCellValues + tempArray
        if debug is True:
            solution_printer = SolutionPrinter(self.allVars)
        else:   
            solution_printer = SolutionPrinter(consolidatedCellValues)
        if printAll is True: solution_printer.setPrintAll()
        if debug is True: solution_printer.setDebug()
        if test is True: solution_printer.setTestMode()
        self.solveStatus = self.solver.SearchForAllSolutions(self.model, solution_printer)

        if test is True:
            return str(solution_printer.SolutionCount())+':'+solution_printer.TestString()
        else:
            print('Solutions found : %i' % solution_printer.SolutionCount())
            if printAll is False and self.solveStatus == cp_model.OPTIMAL:
                print('Sample solution')
                self.printCurrentSolution()

    def printCurrentSolution(self):
        dW = max([len(str(x)) for x in self.digits])
        for rowIndex in range(self.boardWidth):
            for colIndex in range(self.boardWidth):
                print('{:d}'.format(self.solver.Value(self.cellValues[rowIndex][colIndex])).rjust(dW),end = " ")
            print()
        print()

def main(boardSizeRoot):
    # This version uses full syntax for clarity
    p = sudoku(boardSizeRoot)
    p.setIndexColumn(1,False,[4,6])
    p.setIndexColumn(5,True,[2,4,6,9])
    p.setIndexColumn(9,False,[2,6,9])
    p.setGammaEpsilon()
    p.setKropkiWhiteArray([210,260,441,520,751,920])
    p.setKropkiBlackArray([171,251,281,620,660,661,731,861,870])

    p.countSolutions(printAll=True,debug=True)

if __name__ == '__main__':
    # By default, solve the 9x9 problem.
    boardSizeRoot = 3
    if len(sys.argv) > 1:
        boardSizeRoot = int(sys.argv[1])
    main(boardSizeRoot)

What did you expect to see There should only be one solution, which is confirmed by running the model variable by variable (at least the main sudoku cell variables) for each possible value.

What did you see instead? The solver produces the same solution repeatedly in what is presumably an infinite loop.

Anything else we should know about your project / environment Some of the model conditions are complex, and often when I see repeated solutions there is a logic area in the Boolean variables which allows them to "flap" on the same grid solution. But in this case, all of the Boolean variables used are the same in every solution.

[lperron]

it is not an infinite loop. Thanks for the report.

[lperron]

Thanks for the report. I pushed the fix.

The issue were that we created Boolean variables, one per contiguous interval in the (lit1 && lit2 && lit3) => var in [a..b]U[c..d]. These literals were unbound when lit1 && lit2 && lit3 == false. This led to duplicate solutions.

[jeremydover]

Thank you very much for the quick solution! I'll check out the code at the next release and test.