In [1]:
from dominosa import (dominosa_from_1_in_3_sat, draw_dominosa_to_tikz_strlist,
                      tikztemplate_top, tikz_commands, tikztemplate_bottom,
                      verify_dominosa_solution, tikz_passed, tikz_failed)

from graphtex import (tex2svg)

from IPython.display import display #, Image
from IPython.core.display import Image as IImage, SVG

import tempfile
import subprocess


def draw_tikz(tikz_strlist,width=1200,use_png=True):
    """
    Draws the insides of a tikzpicture TeX element, which is input as a list of strings.

    Draws to ipython notebook.

    Optionally draws using a png; this allows saving of the image, or using imgur
    extensions etc. to put it online.
    """
    
    tikzpicture = [r'\begin{tikzpicture}[]','\n\n'] + tikz_strlist
    tikzpicture += [r'\end{tikzpicture}','\n']
    tikz = [tikztemplate_top, '\n'*10, tikz_commands] + tikzpicture + ['\n'*5, tikztemplate_bottom]
    svg = tex2svg(''.join(tikz), scale_to_width=width)
    
    if not use_png:
        display(SVG(data=svg))
    else:
        
        with tempfile.NamedTemporaryFile(suffix='.png') as pngfile:
            with tempfile.NamedTemporaryFile(suffix='.svg') as svgfile:
                svgfile.write(svg)
                svgfile.flush()
                
                cmd = ['rsvg-convert', '-f','png', svgfile.name, '-o', pngfile.name]
                subprocess.check_call(cmd)
                
                display(IImage(filename=pngfile.name))



def options2dict(**kwargs):
    return dict(kwargs)
options = options2dict(
             clip_top=True,
             clip_right=True,
             
             draw_all_squares=False,
             draw_wires=False,
             draw_clauses=False,
             draw_forcing_gadgets=False,
             draw_filler_squares=False,
             
             draw_wire_gadgets=False,
             draw_double_clause_gadgets=False,
             draw_clause_gadgets=False,
             draw_contra_clause_gadgets=False,
             mark_forcing_gadgets=False,
             draw_horizontal_walls=False,
             draw_vertical_walls=False,
             
             tile_horizontal_walls=False,
             tile_vertical_walls=False,
             tile_filler_vtiles=False,
             tile_filler_htiles=False,
             tile_witness=False)


#cnfx = [(1,3,4),(2,3,4)]

# Vor's example, I think it is UNSAT
#cnfx = (x1 v -x2 v x3) AND (x2 v -x3 v x4) AND (-x1 v -x3 v x2)

# My example, witness gives 3 different clause states for demonstration
cnfx = [(1,-2, 3), (2,-3,4), (1,-4,-2)]
cnf_witness = set([3, 2,-1,-4])

details = dominosa_from_1_in_3_sat(cnfx,witness=cnf_witness,increment_extra_n=True)





n = details['n']
min_width = details['min_width']
square_placements = details['square_placements']
witness_htiles = details['witness_htiles']
witness_vtiles = details['witness_vtiles']
view_size = 20

verified = verify_dominosa_solution(n,square_placements,witness_htiles,witness_vtiles)

if verified:
    tikz_strlist = tikz_passed()
    draw_tikz(tikz_strlist,width=200)
    
    print 'congrats, witness solution passed verification'
else:
    tikz_strlist = tikz_failed()
    draw_tikz(tikz_strlist,width=200)
    print 'uh oh, witness solution failed verification'
congrats, witness solution passed verification
In [2]:
# just horizontal walls
options['draw_horizontal_walls']=True
options['tile_horizontal_walls']=True

tikz_strlist = draw_dominosa_to_tikz_strlist(details,**options)
draw_tikz(tikz_strlist)
In [3]:
# horizontal walls and gadgets
options['draw_wires'] = True
options['draw_clauses'] = True
options['draw_forcing_gadgets'] = True
options['draw_wire_gadgets'] = True
options['draw_clause_gadgets'] = True
options['draw_contra_clause_gadgets'] = True
options['mark_forcing_gadgets'] = True

tikz_strlist = draw_dominosa_to_tikz_strlist(details,**options)
draw_tikz(tikz_strlist)
In [4]:
# draw the vertical walls too
options['draw_vertical_walls'] = True
options['tile_vertical_walls'] = True

tikz_strlist = draw_dominosa_to_tikz_strlist(details,**options)
draw_tikz(tikz_strlist)