Csolver encoding is working fine for hard examples ...

diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py
index 653905886bc0755c798b5904be5628198c8a13af..361d3e6bac2403b0e1b9923a02b2ca5eb4b017b4 100755 (executable)
--- a/hexiom/csolverHexiom.py
+++ b/hexiom/csolverHexiom.py
@@ -8,13 +8,14 @@ from hexiom_config import *
 import pycsolver as ps
 from ctypes import *
 import os
+from itertools import combinations
 ############################################
 
 ####
 # Helper functions
 ###
 def getType(name):
-    types = ['O','Nps_', 'Ns_', 'Eps', 'Es', 'Tps_', 'Ts_', 'SimEq_']
+    types = ['P', 'O','Nps_', 'Ns_', 'Eps', 'Es', 'Tps_', 'Ts_', 'SimEq_']
     for (i,str) in enumerate(types):
         if name.startswith(str):
             return i
@@ -121,11 +122,38 @@ class RuleSet(object):
                     index = index + vsrev[i+1]*(base+1)
             assert index < self.size
             return index
-   
+        
+#         def valuesOfIndex(self, n):
+#             for i in range(self.multipliers[0]):
+#                 index = n*self.multipliers[0] +i
+#                 val = self.csolverlb.getBooleanValue(self.csolver, self.csvars[index])
+#                 if val == 1:
+#                     return i;
+#             print("ERROR: invalid value for index")
+#             sys.exit(1)
+#             
+#         def printVariables(self):
+#             vars = []
+#             index = 0
+#             ruller = [i for i in range(self.multipliers[0]+1)]
+#             print ruller
+#             for i, var in enumerate(self.csvars):
+#                 if i!=0 and i%self.multipliers[0] == 0:
+#                     print str(index) + "=>" + str(vars)
+#                     vars[:]=[]
+#                     index = index + 1
+#                 vars.append(str(hex(self.csvars[i]))+"="+str(self.csolverlb.getBooleanValue( self.csolver, self.csvars[i])))
+#             print str(index) + "=>" + str(vars)
+               
     def VarSet(self, name, csolverlb, csolver, dims):
         return RuleSet.VariableSet(self, name, csolverlb, csolver, dims)
-
-
+    
+    def printAllVariables(self):
+        for name in list(self.vsets_by_name.keys()):
+            varset = self.vsets_by_name[name]
+            print "*******************"+str(name)+"******************"
+            varset.printVariables()
+    
     def get_varset_by_name(self, name):
         return self.vsets_by_name.get(name)
 
@@ -148,19 +176,17 @@ class And(CSConstraint):
     def __init__(self, csolverlb, csolver, cs):
         self.csolverlb = csolverlb
         self.csolver = csolver
-        cs = [con.getConstraint() for con in cs]
-        b = (c_void_p*len(cs))(*cs)
-        self.constr = self.csolverlb.applyLogicalOperation(self.csolver, ps.LogicOps.SATC_AND, b, c_uint(len(cs)))
+        constrs = [con.getConstraint() for con in cs]
+        b = (c_void_p*len(constrs))(*constrs)
+        self.constr = self.csolverlb.applyLogicalOperation(self.csolver, ps.LogicOps.SATC_AND, b, c_uint(len(constrs)))
          
-    
-  
 class Or(CSConstraint):
     def __init__(self, csolverlb, csolver, cs):
         self.csolverlb = csolverlb
         self.csolver = csolver
-        cs=[con.getConstraint() for con in cs]
-        b = (c_void_p*len(cs))(*cs)
-        self.constr = self.csolverlb.applyLogicalOperation(self.csolver, ps.LogicOps.SATC_OR, b, c_uint(len(cs)))
+        constrs=[con.getConstraint() for con in cs]
+        b = (c_void_p*len(constrs))(*constrs)
+        self.constr = self.csolverlb.applyLogicalOperation(self.csolver, ps.LogicOps.SATC_OR, b, c_uint(len(constrs)))
   
 def Implies(csolverlb, csolver,a,b):
     return Or(csolverlb, csolver,[-a, +b])
@@ -185,16 +211,16 @@ def sumOfVariables(csolverlb, csolver, S, T, variables, maxk):
     # T(k)   = there are k truthy values
      
     n = len(variables)
-     
+      
     if(maxk is None): maxk = n
- 
+  
     rules = []
- 
+  
     ## S
- 
+  
     for i in range(0, n+1):
         rules.append( S(0, i) )
- 
+  
     for k in range(1, maxk+1):
         rules.append( -S(k, 0) )
         for i in range(1, n+1):
@@ -205,17 +231,16 @@ def sumOfVariables(csolverlb, csolver, S, T, variables, maxk):
                     And(csolverlb, csolver,[ variables[i-1], S(k-1, i-1) ])
                 ])
             ))
- 
+  
     ## T
     for k in range(0, maxk):
         rules.append(Equivalent(csolverlb, csolver,
             T(k), And(csolverlb, csolver,[S(k, n), -S(k+1, n)])
         ))
-
+ 
     rules.append(Equivalent(csolverlb, csolver,
         T(maxk), S(maxk,n)
     ))
- 
     return And(csolverlb, csolver,rules)
 
 def vectorLessThenOrEqual(csolverlb, csolver, E, xs, ys):
@@ -505,33 +530,33 @@ def read_input(fil):
 def generateElements(csolverlb, csolver, slot_range, value_range):
     elems = []
     for slot in range(slot_range[0], slot_range[-1]+1):
-        s1 = [ i for i in range(value_range[0],value_range[-1]+2)]
+        s1 = [ i for i in range(value_range[0],value_range[-1]+1)]
         set1 = (c_long* len(s1))(*s1)
         s1 = csolverlb.createSet(csolver, c_uint(11), set1, c_uint(len(s1)))
         e1 = csolverlb.getElementVar(csolver,s1)
-        csolverlb.mustHaveValue(csolver, e1)
+#         csolverlb.mustHaveValue(csolver, e1)
         elems.append(e1)
     return elems
 
 def Placement(csolverlb, csolver, elems, m, n):
     e1 = elems[m]
-    e2 = csolverlb.getElementConst(csolver, c_uint(12), n+1)
+    e2 = csolverlb.getElementConst(csolver, c_uint(12), n)
     equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS))
     inp = [e1,e2]
     inputs = (c_void_p*len(inp))(*inp)
     b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2))
     return CSConstraint(csolverlb, csolver, b)
 
-def Occupied(csolverlb, csolver, elems, m):
-    e1 = elems[m]
-    e2 = csolverlb.getElementConst(csolver, c_uint(12), 0)
-    equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS))
-    inp = [e1,e2]
-    inputs = (c_void_p*len(inp))(*inp)
-    b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2))
-    return CSConstraint(csolverlb, csolver, b)
+# def Occupied(csolverlb, csolver, elems, m):
+#     e1 = elems[m]
+#     e2 = csolverlb.getElementConst(csolver, c_uint(12), 7)
+#     equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS))
+#     inp = [e1,e2]
+#     inputs = (c_void_p*len(inp))(*inp)
+#     b= csolverlb.applyPredicate(csolver,equals, inputs, c_uint(2))
+#     return CSConstraint(csolverlb, csolver, b)
     
-def replaceWithElemConst(csolver, solver, elems, m, n):
+def replaceWithElemConst(csolverlb, solver, elems, m, n):
     elems[m] = csolverlb.getElementConst(solver, c_uint(10), n)
 ####
 # Create clauses
@@ -558,10 +583,10 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
     
     # (m,n) = There is an n-valued tile at slot m
     #         The m-th slot has n occupied neighbors
-#     Placement = ruleset.VarSet('P', [slot_range, value_range])
+#     Placement = ruleset.VarSet('P', csolverlb, csolver, [slot_range, value_range])
     elems = generateElements(csolverlb, csolver, slot_range, value_range)
     # (m) = is the m-th tile occupied?
-#     Occupied = ruleset.VarSet('O', csolverlb, csolver, [slot_range])
+    Occupied = ruleset.VarSet('O', csolverlb, csolver, [slot_range])
 
     # (m)(k,i) = m-th slot has k occupied slots among its first i neighbours
     NeighbourPartialSum = []
@@ -584,13 +609,13 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
         replaceWithElemConst(csolverlb, csolver, elems, m, n) 
           
     for m in board_input.blocked_positions:
-        csolverlb.addConstraint(csolver, (-Occupied(csolverlb, csolver, elems, m)).getConstraint() )
+        csolverlb.addConstraint(csolver, (-Occupied(m)).getConstraint() )
 
     print 'Creating tile placement rules...'
     rules =[]
     for m in topology.ps:
         csolverlb.addConstraint(csolver, BruteForceOnlyOne(csolverlb, csolver,
-            [-Occupied(csolverlb, csolver, elems, m)] + [+Placement(csolverlb, csolver, elems,m,n) for n in range(7)]
+            [-Occupied(m)] + [+Placement(csolverlb, csolver, elems,m,n) for n in range(7)]
         ).getConstraint())
 
     adj_graph = topology.pos_adjacency_graph()
@@ -611,20 +636,20 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
 
         csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver,
             NPSum, NSum,
-            [+Occupied(csolverlb, csolver, elems, v) for v in adj_graph[m]],
+            [+Occupied(v) for v in adj_graph[m]],
             None
         ).getConstraint())
 
         for n in range(0, nvs+1):
             csolverlb.addConstraint(csolver, Implies(csolverlb, csolver,
-                Occupied(csolverlb, csolver, elems, m),
+                Occupied(m),
                 Equivalent(csolverlb, csolver, +Placement(csolverlb, csolver, elems,m,n), +NSum(n) )
             ).getConstraint())
         
         for n in range(nvs+1, 7):
             csolverlb.addConstraint(csolver, (-Placement(csolverlb, csolver, elems,m,n)).getConstraint() )
 
-    print 'Creating constraints for the amount of tiles used...'
+    print 'Creating constraints for the number of empty cell...'
 
     empty_count = len(topology.ps) - sum([c for (_,c) in board_input.counts])
 
@@ -638,10 +663,10 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
 
     csolverlb.addConstraint(csolver, sumOfVariables(csolverlb, csolver,
         EmptyPartialSum, EmptySum,
-        [ -Occupied(csolverlb, csolver, elems, m) for m in topology.ps ],
+        [ -Occupied(m) for m in topology.ps ],
         empty_count + 1
     ).getConstraint())
-
+    print 'Creating constraints for the amount of tiles used...'
     for n in range(0, 7):
         tile_count = assoc_get(n, board_input.counts)
 
@@ -680,7 +705,7 @@ def SAT_formulation_from_board_input(board_input, csolverlb, csolver):
     def vars_from_sim(ms):
         vs = []
         for m in ms:
-            vs.append( +Occupied(csolverlb, csolver, elems, m) )
+            vs.append( +Occupied(m) )
             vs.extend([ +Placement(csolverlb, csolver, elems,m,n) for n in range(0, 7) ])
         return vs
 
@@ -714,11 +739,12 @@ def print_board_from_assignments(csolverlb, csolver, formulation):
     elems = formulation.elems
 
     layout = [None for p in topology.ps]
-    
-    for i, e in enumerate(elems):
-        elem= csolverlb.getElementValue(csolver, e)
-        if elem != 0:
-            layout[i]= elem 
+    O = ruleset.get_varset_by_name('O')
+
+    for i, var in enumerate(O.csvars):
+        val = csolverlb.getBooleanValue(csolver, var)
+        if val == 1:
+            layout[i] = csolverlb.getElementValue(csolver, elems[i]) 
 
     print '=== Initial input: ==='
     formulation.board_input.print_to_stdout()
@@ -753,8 +779,7 @@ def main():
     formulation = SAT_formulation_from_board_input(board_input, csolverlb, csolver)
    
     print '=== Done! Calling CSolver solver now ==='
-#     csolverlb.serialize(csolver)
-    csolverlb.printConstraints(csolver)
+#     csolverlb.printConstraints(csolver)
     if csolverlb.solve(csolver) != 1:
         print '*** Got UNSAT result! ***'
         sys.exit(1)