1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 | # Number Partitioning # # In this problem, the numbers 1 to N must be arranged in two # different groups A and B in such a way that: # 1. A and B have the same cardinality. # 2. The sum of numbers in A equals the sum of numbers in B. # 3. The sum of the squares of numbers in A equals the sum of # the squares of numbers in B. # # CSPLib Problem 049 - http://www.csplib.org/Problems/prob049/ # # Note: There is no solution for N < 8! Also, there is no solution # if N is not a multiple of 4! (Source: CSPLib - see above link.) from Numberjack import * def get_model(N): assert N % 2 = = 0 , "N should be even" # A and B will have the same cardinality: A = VarArray(N / 2 , 1 , N) B = VarArray(N / 2 , 1 , N) model = Model( # Each of the numbers 1 to N must be present exactly once. AllDiff([x for x in A + B]), # The sum of numbers in A equals the sum of numbers in B. Sum (A) = = Sum (B), # The sum of the squares of numbers in A equals the sum of # the squares of numbers in B. Sum ([x * x for x in A]) = = Sum ([y * y for y in B]) ) # Symmetry breaking model + = A[ 0 ] < B[ 0 ] for i in range (N / 2 - 1 ): model + = A[i] < A[i + 1 ] model + = B[i] < B[i + 1 ] return A, B, model def solve(param): N = param[ 'N' ] A, B, model = get_model(N) solver = model.load(param[ 'solver' ]) solver.setVerbosity(param[ 'verbose' ]) solver.solve() if solver.is_sat(): print "A: " + str (A) print "B: " + str (B) elif solver.is_unsat(): print "Unsatisfiable" else : print "Timed out" print solver.getNodes() if __name__ = = '__main__' : default = { 'N' : 8 , 'solver' : 'Mistral' , 'verbose' : 0 } param = input (default) solve(param) |