Add Z3 powered packer as an alternative to BinPacker

extend_types.py

@@ -111,6 +111,17 @@ def register():
     bpy.types.Scene.smc_save_path = StringProperty(
         description='Select the directory in which the generated texture atlas will be saved',
         default='')
+    bpy.types.Scene.smc_use_advanced_packer = BoolProperty(
+        name='Use advanced packing',
+        description='Use the Z3 SMT powered packing optimizer to minimize texture size',
+        default=True)
+    bpy.types.Scene.smc_advanced_packing_round_time_limit = IntProperty(
+        name="Advanced packing round time limit in seconds",
+        description="The time limit for each round of packing. Depending on your settings and " +
+        "source textures, packing may take 1 to 4 rounds",
+        default=5,
+        min=1,
+        max=600)
 
     bpy.types.Material.root_mat = PointerProperty(
         name='Material Root',
@@ -147,6 +158,12 @@ def unregister():
     del bpy.types.Scene.smc_size
     del bpy.types.Scene.smc_size_width
     del bpy.types.Scene.smc_size_height
+    del bpy.types.Scene.smc_crop
+    del bpy.types.Scene.smc_diffuse_size
+    del bpy.types.Scene.smc_gaps
+    del bpy.types.Scene.smc_save_path
+    del bpy.types.Scene.smc_use_advanced_packer
+    del bpy.types.Scene.smc_advanced_packing_round_time_limit
 
     del bpy.types.Material.root_mat
     del bpy.types.Material.smc_diffuse

globs.py

@@ -7,6 +7,7 @@
 try:
     from PIL import Image
     from PIL import ImageChops
+    from z3 import Solver
 
     pil_exist = True
 except ImportError:

operators/combiner/combiner.py

@@ -1,6 +1,7 @@
 from bpy.props import *
 from .combiner_ops import *
 from .packer import BinPacker
+from .z3_packer import Z3Packer, UnsatError
 from ... import globs
 
 
@@ -22,7 +23,28 @@ def execute(self, context):
             self.invoke(context, None)
         scn = context.scene
         scn.smc_save_path = self.directory
-        self.structure = BinPacker(get_size(scn, self.structure)).fit()
+
+        images = get_size(scn, self.structure)
+
+        if scn.smc_use_advanced_packer:
+            packer = None
+            if scn.smc_size == 'CUST':
+                # max width/height can only be specified in custom mode in the UI, hence we only
+                # provide it in custom mode here, even though specifying it in other modes is also
+                # allowed.
+                packer = Z3Packer(images, mode='CUST', width=scn.smc_size_width,
+                    height=scn.smc_size_height, timeout=scn.smc_advanced_packing_round_time_limit*1000)
+            else:
+                packer = Z3Packer(images, mode=scn.smc_size,
+                    timeout=scn.smc_advanced_packing_round_time_limit*1000)
+            try:
+                self.structure = packer.fit()
+            except (ValueError, UnsatError) as e:
+                self.report({'ERROR'}, 'Advanced packer failed: ' + str(e))
+                return {'FINISHED'}
+        else:
+            self.structure = BinPacker(images).fit()
+
         size = (max([i['gfx']['fit']['x'] + i['gfx']['size'][0] for i in self.structure.values()]),
                 max([i['gfx']['fit']['y'] + i['gfx']['size'][1] for i in self.structure.values()]))
         if any(size) > 20000:

operators/combiner/z3_packer.py

@@ -0,0 +1,188 @@
+import z3
+from itertools import combinations
+
+class UnsatError(Exception):
+    pass
+
+class Z3Packer:
+    po2_sizes = [
+        (128, 128), (256, 128), (128, 256),
+        (256, 256), (512, 256), (256, 512),
+        (512, 512), (1024, 512), (512, 1024),
+        (1024, 1024), (2048, 1024), (1024, 2048),
+        (2048, 2048), (4096, 2048), (2048, 4096),
+        (4096, 4096), (8192, 4096), (4096, 8192),
+        (8192, 8192), (16384, 8192), (8192, 16384),
+        (16384, 16384)
+    ]
+
+    def __init__(self, images, mode='PO2', width=0, height=0, timeout=5000):
+        '''
+        mode can be 'PO2', 'QUAD', 'AUTO', 'CUST'
+        '''
+        self.original_images = images
+        self.images = [img for img in images.values()]
+
+        print(self.images[0]['gfx'])
+        self.sym_image = [(z3.Int(f'img_{i}_x'), z3.Int(f'img_{i}_y')) for i in range(len(self.images))]
+        self.model_max_height = z3.Int('max_height')
+        self.model_max_width = z3.Int('max_width')
+        self.total_pixels = sum([img['gfx']['size'][0] * img['gfx']['size'][1] for img in self.images])
+        self.max_height = 0
+        self.max_width = 0
+        self.mode = mode
+        self.timeout = timeout
+
+    def sym_max(self, x, y):
+        return z3.If(x > y, x, y)
+
+    def __get_po2_candidates(self):
+        '''
+        gets the potential size candidates for PO2
+        '''
+        for i in range(len(self.po2_sizes)):
+            if (self.po2_sizes[i][0] * self.po2_sizes[i][1]) >= self.total_pixels:
+                return self.po2_sizes[i:]
+        return []
+
+    def __constrain_images(self):
+        '''
+        adds common constraints to the solver
+        '''
+        # ensure the images don't overlap with each other
+        for pair in combinations(range(len(self.images)), 2):
+            a = pair[0]
+            a_tl = self.sym_image[a]
+            a_br = (a_tl[0] + self.images[a]['gfx']['size'][0], a_tl[1] + self.images[a]['gfx']['size'][1])
+
+            b = pair[1]
+            b_tl = self.sym_image[b]
+            b_br = (b_tl[0] + self.images[b]['gfx']['size'][0], b_tl[1] + self.images[b]['gfx']['size'][1])
+
+            self.s.add(z3.Or(a_tl[0] >= b_br[0], b_tl[0] >= a_br[0],
+                a_br[1] <= b_tl[1], b_br[1] <= a_tl[1]))
+
+
+        sym_max_width = 0
+        sym_max_height = 0
+
+        # ensure the images are within the bounds of the atlas
+        for i in range(len(self.images)):
+            sym_img = self.sym_image[i]
+            img = self.images[i]
+            self.s.add([sym_img[0] >= 0, sym_img[1] >= 0])
+            sym_max_width = self.sym_max(sym_max_width, sym_img[0] + img['gfx']['size'][0])
+            sym_max_height = self.sym_max(sym_max_height, sym_img[1] + img['gfx']['size'][1])
+
+        self.s.add(self.model_max_height == sym_max_height)
+        self.s.add(self.model_max_width == sym_max_width)
+
+    def __push_size_constriants(self, width, height):
+        '''
+        pushes a backtracking point and constrains the size of the atlas
+        '''
+        self.s.push()
+        if width == 0 and height == 0:
+            return
+
+        for i in range(len(self.images)):
+            sym_img = self.sym_image[i]
+            img = self.images[i]
+            if width > 0:
+                self.s.add((sym_img[0] + img['gfx']['size'][0]) <= width)
+            if height > 0:
+                self.s.add((sym_img[1] + img['gfx']['size'][1]) <= height)
+
+
+    def __optimize(self):
+        '''
+        optimizes the atlas size (rather than solving for a particular size)
+        '''
+        if not isinstance(self.s, z3.Optimize):
+            raise ValueError('optimize can only be called when mode is QUAD or AUTO')
+
+        self.s.minimize(self.model_max_height + self.model_max_width)
+        return self.__check()
+
+
+    def __solve(self):
+        '''
+        solves the atlas size (rather than optimizing to be a minimal size)
+        '''
+        if not isinstance(self.s, z3.Solver):
+            raise ValueError('solve can only be called when mode is PO2 or CUST')
+
+        return self.__check()
+
+    def __check(self):
+        '''
+        checks the solver for satisfiability and returns the result if satisfiable
+        '''
+        result = self.s.check()
+        if result == z3.sat:
+            model = self.s.model()
+            print("z3_packer: solved model:", model)
+            for i in range(len(self.images)):
+                sym_img = self.sym_image[i]
+                img = self.images[i]
+                img['gfx']['fit'] = {
+                    'x': model[sym_img[0]].as_long(),
+                    'y': model[sym_img[1]].as_long()
+                }
+        elif result == z3.unsat:
+            raise UnsatError('The constraints given were unsatisfiable (not possible to fit ' +
+                'images in atlas). Try increasing the maximum size of the atlas.')
+        else:
+            raise UnsatError('The constraints given were unsatisfiable in the time limit given. ' +
+                'Try increasing the timeout or maximum size of the atlas.')
+
+        return self.original_images
+
+    def fit(self):
+        '''
+        fits the images to the atlas
+        '''
+        if self.max_width < 0 or self.max_height < 0:
+            raise ValueError('max width and height must be positive')
+
+        if self.mode in ['PO2', 'CUST']:
+            self.s = z3.Solver()
+        elif self.mode in ['QUAD', 'AUTO']:
+            self.s = z3.Optimize()
+        else:
+            raise ValueError('mode must be PO2, QUAD, AUTO, or CUST')
+
+        self.s.set('timeout', self.timeout)
+
+        if self.mode == 'CUST':
+            if self.max_width == 0 or self.max_height == 0:
+                raise ValueError('width and height must both be specified when running in CUST mode')
+
+        self.__constrain_images()
+
+        if self.mode == 'PO2' and (self.max_width == 0 or self.max_height == 0):
+            candidates = self.__get_po2_candidates()
+            for po2_candidate in candidates[:4]:
+                candidate = po2_candidate
+                if self.max_width > 0:
+                    candidate = (min(self.max_width, candidate[0]), candidate[1])
+                if self.max_height > 0:
+                    candidate = (candidate[0], min(self.max_height, candidate[1]))
+                self.__push_size_constriants(*candidate)
+                try:
+                    return self.__solve()
+                except UnsatError:
+                    pass
+
+                # reset the constraints on each attempt
+                self.s.pop()
+
+            raise UnsatError('Attempted all candidates and none were satisfiable. Your final ' +
+                'atlas size is likely beyond 16384x16384 which is unsupported')
+
+        self.__push_size_constriants(self.max_width, self.max_height)
+
+        if isinstance(self.s, z3.Optimize):
+            return self.__optimize()
+
+        return self.__solve()

operators/get_pillow.py

@@ -9,21 +9,22 @@
 
 class InstallPIL(bpy.types.Operator):
     bl_idname = 'smc.get_pillow'
-    bl_label = 'Install PIL'
-    bl_description = 'Click to install Pillow. This could take a while and might require you to start Blender as admin'
+    bl_label = 'Install Dependencies'
+    bl_description = 'Click to install dependencies (Pillow and Z3). This could take a while and might require you to start Blender as admin'
 
     def execute(self, context):
         python_executable = bpy.app.binary_path_python if bpy.app.version < (3, 0, 0) else sys.executable
         try:
             import pip
             try:
                 from PIL import Image, ImageChops
+                from z3 import Solver
             except ImportError:
-                call([python_executable, '-m', 'pip', 'install', 'Pillow', '--user', '--upgrade'], shell=True)
+                call([python_executable, '-m', 'pip', 'install', 'Pillow', 'z3-solver', '--user', '--upgrade'], shell=True)
         except ImportError:
             call([python_executable, os.path.join(os.path.dirname(os.path.abspath(__file__)), 'get_pip.py'),
                   '--user'], shell=True)
-            call([python_executable, '-m', 'pip', 'install', 'Pillow', '--user', '--upgrade'], shell=True)
+            call([python_executable, '-m', 'pip', 'install', 'Pillow', 'z3-solver', '--user', '--upgrade'], shell=True)
         globs.smc_pi = True
         self.report({'INFO'}, 'Installation complete')
         return {'FINISHED'}

operators/ui/include.py

@@ -29,11 +29,11 @@ def draw_ui(context, m_col):
             col.label(text='Please restart Blender', icon_value=get_icon_id('null'))
         else:
             col = m_col.box().column()
-            col.label(text='Python Imaging Library required to continue')
+            col.label(text='Dependencies (Pillow and Z3) required to continue')
             col.separator()
             row = col.row()
             row.scale_y = 1.5
-            row.operator('smc.get_pillow', text='Install Pillow', icon_value=get_icon_id('download'))
+            row.operator('smc.get_pillow', text='Install Dependencies', icon_value=get_icon_id('download'))
             col.separator()
             col.separator()
             col.label(text='If the installation process is repeated')

ui/main_menu.py

@@ -32,24 +32,37 @@ def draw(self, context):
             if scn.smc_size == 'CUST':
                 box.prop(scn, 'smc_size_width')
                 box.prop(scn, 'smc_size_height')
-            box.scale_y = 1.2
+            box.scale_y = 1.0
+            box.prop(scn, 'smc_use_advanced_packer')
+            row = box.row()
+            col = row.column()
+            col.label(text=bpy.types.Scene.smc_advanced_packing_round_time_limit[1]["name"])
+            col = row.column()
+            col.scale_x = .75
+            col.scale_y = 1.0
+            col.alignment = 'RIGHT'
+            col.prop(scn, 'smc_advanced_packing_round_time_limit', text='')
+            if scn.smc_use_advanced_packer:
+                col.enabled = True
+            else:
+                col.enabled = False
             box.prop(scn, 'smc_crop')
             row = box.row()
             col = row.column()
-            col.scale_y = 1.2
+            col.scale_y = 1.0
             col.label(text='Size of materials without image')
             col = row.column()
             col.scale_x = .75
-            col.scale_y = 1.2
+            col.scale_y = 1.0
             col.alignment = 'RIGHT'
             col.prop(scn, 'smc_diffuse_size', text='')
             row = box.row()
             col = row.column()
-            col.scale_y = 1.2
+            col.scale_y = 1.0
             col.label(text='Size of gaps between images')
             col = row.column()
             col.scale_x = .75
-            col.scale_y = 1.2
+            col.scale_y = 1.0
             col.alignment = 'RIGHT'
             col.prop(scn, 'smc_gaps', text='')
             col = box.column()
@@ -63,11 +76,11 @@ def draw(self, context):
                 col.label(text='Installation complete', icon_value=get_icon_id('done'))
                 col.label(text='Please restart Blender', icon_value=get_icon_id('null'))
             else:
-                col.label(text='Python Imaging Library required to continue')
+                col.label(text='Dependencies (Pillow and Z3) required to continue')
                 col.separator()
                 row = col.row()
                 row.scale_y = 1.5
-                row.operator('smc.get_pillow', text='Install Pillow', icon_value=get_icon_id('download'))
+                row.operator('smc.get_pillow', text='Install Dependencies', icon_value=get_icon_id('download'))
                 col.separator()
                 col.separator()
                 col = col.box().column()