Examples using the Pyidp3 API

All of these examples were made to be used in my CI testing pipeline. For each of the examples, I list up what elements are in it in case you’re looking for an example of something specific.

simple_inference

As the title says, this is a simple inference test. Contains:

• nbmodels and xdb options
• Defining constants without value or type
• Constraint
• Satchecking
• Model expanding

#!/usr/bin/python3

"""
This is a very simple and small test.
If this test fails, there's something extremely wrong.
It defines 3 variables, that each are either True or False.
"""
from pathlib import Path
from pyidp3.typedIDP import IDP


home = str(Path.home())
idp = IDP(home+"/idp/usr/local/bin/idp")
idp.nbmodels = 2
idp.xsb = "true"

idp.Constant("P")
idp.Constant("Q")
idp.Constant("R")

idp.Constraint("(P => Q) <=> (P <= R).", True)
idp.Constraint("satisfiable().", True)

idp.check_sat()
idp.model_expand()

harder_inference

This is a bit tougher than the previous example. Contains:

• Type with a range
• Constant with type, no value
• Constraint
• Predicate
• Satchecking
• Model expanding

#!/usr/bin/python3

"""
This is a fairly simple test, it just adds more constants and constraints.
The generated IDP file will have 6 letters (each an int),
which have some constraints (A, E and I need to be even numbers,
while B, C and D need to be uneven).
A, B and C also can't be zero.
No two letters can be the same number.

The following puzzle needs to be solved:
    AI
    BA
+-----
   CDE

Or in other terms: AI + BA = CDE
"""
from pathlib import Path
from pyidp3.typedIDP import *


home = str(Path.home())
idp = IDP(home+"/idp/usr/local/bin/idp")

# Define the range of numbers
idp.Type("Decimal", (0, 9))

# Define the letters
letters = ['A', 'B', 'C', 'I', 'D', 'E']
even_letters = ['A', 'I', 'E']
for letter in letters:
    idp.Constant(letter+": Decimal")
    for letter2 in letters:
        if letter == letter2:
            continue
        idp.Constraint(letter + " ~= " + letter2, True)
    if letter in even_letters:
        idp.Constraint("Even(" + letter + ")", True)
    else:
        idp.Constraint("~Even(" + letter + ")", True)


# Define the Even numbers
idp.Predicate("Even(Decimal)", [0, 2, 4, 6, 8])

# No two letters can have the same value
idp.Constraint("A ~= B & A ~= C & A ~= I & A ~= D & A ~= E & B ~= C & B ~= I"
               "& B ~= D & B ~= E & C ~= I & C ~= D & C ~= E & I ~= D &"
               " I ~= E & D ~= E", True)
idp.Constraint("I + A + 10*A + 10*B = E + 10 * D + 100 * C", True)

idp.check_sat()
idp.model_expand()

definition_test

This is a graphsolver with a Define in it. Other than that, nothing special going on. Contains:

• Type
• Predicate, with and without value
• Define
• Satchecking
• Modelexpansion

#!/usr/bin/python3

"""
This testfile is a graph solver.
Given a set of edges, it finds out what nodes are connected.
To do this is uses a definition consisting of two rules.

"""
from pathlib import Path
from pyidp3.typedIDP import *


home = str(Path.home())
idp = IDP(home+"/idp/usr/local/bin/idp")

# Define Node, Edge and Connected
nodelist = ['A', 'B', 'C', 'D', 'E']
idp.Type("Node", nodelist)
idp.Predicate("Edge(Node, Node)", ["A,B", "A,C", "B,E", "C,D", "C,E", "D,E",
                                   "E,B"])
idp.Predicate("Connected(Node, Node)")

idp.Define("!x[Node] y[Node]: Connected(x,y) <- Edge(y,x). \n"
           "!x[Node] y[Node] z[Node]: Connected(x,y) "
           "<- Connected(x,z) & Connected(z,y)", True)

idp.check_sat()
idp.model_expand()

constructed_from

This file was mainly made to test the constructed from keyword. It contains:

• Type, with constructed from
• Predicate, with value
• Constraint
• Satchecking
• Modelexpansion

#!/usr/bin/python3

"""
Tests for "constructed_from".
This .idp file can only work when "constructed_from" works.
"""
from pathlib import Path
from pyidp3.typedIDP import *


home = str(Path.home())
idp = IDP(home+"/idp/usr/local/bin/idp")

days_of_the_week = ["Monday", "Tuesday", "Wednesday", "Thursday", "Friday",
                    "Saturday", "Sunday"]
idp.Type("Day", days_of_the_week, constructed_from=True)
idp.Predicate("Weekend(Day)", ["Saturday", "Sunday"])
idp.Constant("Easter: Day")

idp.Constraint("Weekend(Easter)", True)
idp.Constraint("Easter ~= Saturday", True)

idp.check_sat()
idp.model_expand()

initial_group_assign

This file is part of my master’s thesis. It’s a simplified version of my initial group assign, where the IDP-system tries to assign students to groups as best as it can. It tries to minimize a term “Totaal”. This currently isn’t in English, for which I’m sorry.

It contains:

• mxtimeout option
• Types, with lists as values
• Predicate
• Function
• Constant
• Define
• Constraint
• Satchecking
• Modelexpansion
• Minimization, using the Totaal term.

#!/usr/bin/python3

"""
Testfile to test if the initial solution to our problem still works as it
should be.
It minimizes, and then it modelexpands.
"""
from pathlib import Path
from pyidp3.typedIDP import *


home = str(Path.home())
idp = IDP(home+"/idp/usr/local/bin/idp")
idp.mxtimeout = 10

WoonDict = {1: 87, 2: 98, 3: 80, 4: 80, 5: 83, 6: 88, 7: 90, 8: 86, 9: 80, 10:
            53, 11: 98, 12: 57, 13: 86, 14: 82, 15: 98, 16: 83, 17: 15, 18: 88,
            19: 22, 20: 78, 21: 80, 22: 86, 23: 27, 24: 57, 25: 84}
ZoneDict = {1: 2, 2: 1, 3: 2, 4: 2, 5: 2, 6: 2, 7: 2, 8: 2, 9: 2, 10: 2, 11: 1,
            12: 2, 13: 2, 14: 2, 15: 1, 16: 2, 17: 2, 18: 1, 19: 2, 20: 1, 21:
            2, 22: 2, 23: 2, 24: 2, 25: 2}

idp.Type("Student", list(range(1, 26)))
idp.Type("Getal", list(range(int(1000000))))
idp.Type("Postcode", list(range(0, 100)))
idp.Type("Zone", list(range(0, 10)))

idp.Predicate("Samen(Student,Student)")
idp.Predicate("VolSamen(Student, Student)")

idp.Function("Woont(Student): Postcode", WoonDict)
idp.Function("WoontZone(Student): Zone", ZoneDict)

idp.Predicate("Wortel(Student)")
idp.Predicate("Blad(Student)")
idp.Function("Aant(Student): Getal")

idp.Constant("SamenSchool: Getal")
idp.Constant("Afstand: Getal")
idp.Constant("UitZone: Getal")
idp.Constant("Totaal: Getal")


idp.Define("Wortel(x) <- x < min{y[Student]: Samen(y,x):y}.", True)
idp.Define("Blad(x) <- ~Wortel(x).", True)

idp.Constraint("#{x[Student]: Wortel(x)} = 5", True)
idp.Constraint("!x[Student]: Blad(x) <=> ?y[Student]: Wortel(y) & Samen(y,x)",
               True)
idp.Constraint("!x[Student]: Aant(x) = #{y[Student]: Samen(x,y) | Samen(y,x)}",
               True)
idp.Constraint("!x[Student]: Wortel(x) <=> 4 =< Aant(x) =< 6", True)
idp.Constraint("!x[Student]: Blad(x) <=> Aant(x) = 1", True)
idp.Constraint("!x[Student] y[Student]: Samen(x,y) => Wortel(x) & Blad(y)",
               True)
idp.Define("!x[Student] y[Student] z[Student]: VolSamen(y,z) <- Wortel(x) & y"
           " < z & Samen(x,y) & Samen(x,z).\n"
           "!x[Student] y[Student]: VolSamen(x,y) <- Wortel(x) & Samen(x,y).",
           True)
idp.Constraint("Afstand = sum{x[Student] y[Student]: x < y & VolSamen(x,y) &"
               " WoontZone(x) = WoontZone(y): abs(Woont(x) - Woont(y))}", True)
idp.Constraint("UitZone = #{x[Student] y[Student]: x < y & VolSamen(x,y) &"
               " WoontZone(x) ~= WoontZone(y) }", True)

idp.Constraint("Totaal = Afstand  + UitZone * 100", True)
idp.check_sat()
idp.model_expand()
sols = idp.minimize("Totaal")


for sol in sols:
    print(sol)
    if sol['satisfiable']:
        for x in sol['Samen']:
            print(x)

initial_group_assign_plus

This file is an expanded version of the previous, where schools are taken into account.

It contains:

• mxtimeout and nbmodels option
• Types, with lists as values
• Predicate
• Function
• Constant
• Define
• Constraint
• Satchecking
• Modelexpansion
• Minimization, using the Totaal term.

#!/usr/bin/python3

"""
Testfile that checks whether ISSUE-1 (the {x..y} in structs) is still valid.
"""
from pathlib import Path
from pyidp3.typedIDP import *


home = str(Path.home())
idp = IDP(home+"/idp/usr/local/bin/idp")
idp.mxtimeout = 10
idp.nbmodels = 5

WoonDict = {1: 87, 2: 98, 3: 80, 4: 80, 5: 83, 6: 88, 7: 90, 8: 86, 9: 80, 10:
            53, 11: 98, 12: 57, 13: 86, 14: 82, 15: 98, 16: 83, 17: 15, 18: 88,
            19: 22, 20: 78, 21: 80, 22: 86, 23: 27, 24: 57, 25: 84}
ZoneDict = {1: 2, 2: 1, 3: 2, 4: 2, 5: 2, 6: 2, 7: 2, 8: 2, 9: 2, 10: 2, 11: 1,
            12: 2, 13: 2, 14: 2, 15: 1, 16: 2, 17: 2, 18: 1, 19: 2, 20: 1, 21:
            2, 22: 2, 23: 2, 24: 2, 25: 2}
SchoolDict = {1: "GO! atheneum Anderlecht",
              2: "KONINKLIJK ATHENEUM KOEKELBERG",
              3: "TSM-Bovenbouw"', 4: '"TSM-Bovenbouw",
              5: "PTS, Provinciale Scholen voor Tuinbouw en Techniek",
              6: "Onze-Lieve-Vrouw-Presentatie", 7: "Sint-Ludgardisschool",
              8: "Mater Salvatorisinstituut", 9: "Scheppersinstituut",
              10: "Sint-Gabriëlcollege", 11: "Scheppersinstituut",
              12: "Sint-Norbertusinstituut 2", 13: "Ursulinen Mechelen 1",
              14: "College Hagelstein 2", 15: "Scheppersinstituut",
              16: "TSM-Bovenbouw", 17: "TOEKOMSTONDERWIJS HOBOKEN",
              18: "Gemeentelijk Technisch Instituut",
              19: "Heilig Hart - Bovenbouw 1",
              20: "Gemeentelijke Technische en Beroepsschool",
              21: "GO! Busleyden Atheneum-campus Pitzemburg",
              22: "College Hagelstein 2",
              23: "Kardinaal van Roey-Instituut ASO",
              24: "Sint-Gummaruscollege", 25: "GO! atheneum Boom"}


idp.Type("Student", (1, 25))
idp.Type("Getal", (0, 10000000))
idp.Type("Postcode", (0, 100))
idp.Type("Zone", (0, 10))

idp.Predicate("Samen(Student,Student)")
idp.Predicate("VolSamen(Student, Student)")

idp.Function("Woont(Student): Postcode", WoonDict)
idp.Function("WoontZone(Student): Zone", ZoneDict)
idp.Function("School(Student): string", SchoolDict)

idp.Predicate("Wortel(Student)")
idp.Predicate("Blad(Student)")
idp.Function("Aant(Student): Getal")

idp.Constant("SamenSchool: Getal")
idp.Constant("Afstand: Getal")
idp.Constant("UitZone: Getal")
idp.Constant("Totaal: Getal")


idp.Define("Wortel(x) <- x < min{y[Student]: Samen(y,x):y}.", True)
idp.Define("Blad(x) <- ~Wortel(x).", True)

idp.Constraint("#{x[Student]: Wortel(x)} = 5", True)
idp.Constraint(" !x[Student]: Blad(x) <=> ?y[Student]: Wortel(y) & Samen(y,x)",
               True)
idp.Constraint("!x[Student]: Aant(x) = #{y[Student]: Samen(x,y) | Samen(y,x)}",
               True)
idp.Constraint("!x[Student]: Wortel(x) <=> 4 =< Aant(x) =< 6", True)
idp.Constraint("!x[Student]: Blad(x) <=> Aant(x) = 1", True)
idp.Constraint("!x[Student] y[Student]: Samen(x,y) => Wortel(x) & Blad(y)",
               True)
idp.Define("!x[Student] y[Student] z[Student]: VolSamen(y,z) <- Wortel(x) & y"
           " < z & Samen(x,y) & Samen(x,z).\n"
           "!x[Student] y[Student]: VolSamen(x,y) <- Wortel(x) & Samen(x,y).",
           True)
idp.Constraint("SamenSchool = #{x[Student] y[Student]: x < y & VolSamen(x,y)"
               "& School(x) ~= School(y)}", True)
idp.Constraint("Afstand = sum{x[Student] y[Student]: x < y & VolSamen(x,y) &"
               " WoontZone(x) = WoontZone(y): abs(Woont(x) - Woont(y))}", True)
idp.Constraint("UitZone = #{x[Student] y[Student]: x < y & VolSamen(x,y) &"
               " WoontZone(x) ~= WoontZone(y) }", True)

idp.Constraint("Totaal = Afstand  + UitZone * 100 + SamenSchool*100", True)


solutions = idp.model_expand()
solutions = idp.minimize("Totaal")
idp.check_sat()

print("{:d} solutions!".format(len(solutions)))
for index, sol in enumerate(solutions):
    if sol['satisfiable']:
        print("Sol {:d}:".format(index))
        for x in sol['Samen']:
            print('\t', x)
    else:
        continue

further_group_assign

This is the other part of my master’s thesis. Here we try to reassign students based on their old groups, and a preference.

It contains:

• nbmodels option
• comparing solutions using the compare method
• Type, also one with the isa keyword
• Constant, with value
• Predicate
• Function
• Constraint
• Define
• minimization, using the Total term

#!/usr/bin/python3

"""
Testfile which attempts to assign students to a group, based on a previous
group and a preference.
"""
from pathlib import Path
from pyidp3.typedIDP import *


home = str(Path.home())
idp = IDP(home+"/idp/usr/local/bin/idp")
idp.nbmodels = 5

# All the inputvars
idp.Type("Student", (1, 152))
idp.Type("Number", (0, 10000000))
idp.Type("Group", (2, 11))
idp.Type("Priority", "Number", isa=True)
idp.Constant("MinSize: Number", 14)
idp.Constant("MaxSize: Number", 16)

together = [(142, 139, 2), (139, 143, 1), (139, 142, 1)]
not_together = [(142, 143, 2), (142, 141, 2), (142, 140, 2)]
in_group = []
group_dict = {1: 2,  2: 3,  3: 4,  4: 5,  5: 6,  6: 7,  7: 8,  8: 9,  9: 10,
              10: 11,  11: 3,  12: 11,  13: 8,  14: 6,  15: 4,  16: 2,  17: 10,
              18: 8,  19: 7,  20: 5,  21: 4,  22: 3,  23: 2,  24: 11,  25: 9,
              26: 8, 27: 6,  28: 6,  29: 5,  30: 4,  31: 3,  32: 2,  33: 10,
              34: 11,  35: 9,  36: 5,  37: 7,  38: 7,  39: 6,  40: 5,  41: 5,
              42: 4,  43: 3,  44: 3,  45: 2,  46: 10,  47: 10,  48: 11,  49: 8,
              50: 9,  51: 7,  52: 8, 53: 10,  54: 6,  55: 6,  56: 5,  57: 5,
              58: 5,  59: 4,  60: 4,  61: 3, 62: 3,  63: 2,  64: 2,  65: 10,
              66: 7,  67: 10,  68: 11,  69: 11,  70: 9,  71: 9,  72: 8,  73: 8,
              74: 7,  75: 7,  76: 6,  77: 6,  78: 6,  79: 9,  80: 5,  81: 5,
              82: 4,  83: 4,  84: 4,  85: 3,  86: 3,  87: 3,  88: 2,  89: 2,
              90: 2,  91: 2,  92: 10,  93: 11,  94: 10,  95: 8,  96: 11,
              97: 11,  98: 9,  99: 9,  100: 9,  101: 9,  102: 8,  103: 8,
              104: 8, 105: 7,  106: 7,  107: 7,  108: 6,  109: 6,  110: 6,
              111: 6,  112: 5, 113: 5,  114: 5,  115: 5,  116: 4,  117: 4,
              118: 4,  119: 4,  120: 4, 121: 3,  122: 3,  123: 3,  124: 3,
              125: 2,  126: 2,  127: 2,  128: 2, 129: 11,  130: 10,  131: 10,
              132: 10,  133: 10,  134: 10,  135: 11, 136: 11,  137: 11,
              138: 11,  139: 9,  140: 9,  141: 9,  142: 9,  143: 9,  144: 8,
              145: 8,  146: 8,  147: 7,  148: 7,  149: 7,  150: 7,  151:
              7,  152: 6}
idp.Function("InGroup(Student): Group", group_dict)
idp.Predicate("WantsTogether(Student, Student, Priority)", together)
idp.Predicate("NotWantsTogether(Student, Student, Priority)", not_together)
idp.Predicate("WantsInGroup(Student, Group, Priority)", in_group)


# All the inner workings + output
idp.Function("GroupSize(Group): Number")

idp.Constant("Total: Number")
idp.Constant("TotUnsatTogether: Number")
idp.Constant("TotUnsatNotTogether: Number")
idp.Constant("TotUnsatInGroup: Number")
idp.Constant("TotUnsatNewGroup: Number")

idp.Predicate("UnsatTogether(Student, Student)")
idp.Predicate("UnsatNotTogether(Student, Student)")
idp.Predicate("UnsatInGroup(Student, Group)")
idp.Predicate("UnsatNewGroup(Student)")

idp.Function("NewInGroup(Student): Group")


# All the necessary constraints
idp.Constraint("!g[Group]: GroupSize(g) = #{x[Student]: NewInGroup(x) = g}",
               True)
idp.Constraint("!g[Group]: MinSize =< GroupSize(g) =< MaxSize", True)
idp.Constraint("TotUnsatNewGroup = #{x[Student]: InGroup(x) ~= NewInGroup(x)}",
               True)
idp.Constraint("TotUnsatTogether = sum{x[Student] y[Student]:"
               " WantsTogether(x,y,p) & NewInGroup(x) ~= NewInGroup(y): p}",
               True)
idp.Constraint("TotUnsatNotTogether = sum{x[Student] y[Student]:"
               " NotWantsTogether(x,y,p) & NewInGroup(x) = NewInGroup(y): p}",
               True)
idp.Constraint("TotUnsatInGroup = sum{x[Student] g[Group]: WantsInGroup(x,g,p)"
               " & NewInGroup(x) ~= g: p}", True)
idp.Constraint("Total = TotUnsatTogether + TotUnsatNotTogether +"
               " TotUnsatInGroup + TotUnsatNewGroup", True)

idp.Define("!x[Student] y[Student]: UnsatTogether(x,y) <- WantsTogether(x,y,p)"
           " & NewInGroup(x) ~= NewInGroup(y).", True)
idp.Define("!x[Student] y[Student]: UnsatNotTogether(x,y) <- "
           " NotWantsTogether(x,y,p) & NewInGroup(x) = NewInGroup(y).",
           True)
idp.Define("!x[Student]: UnsatNewGroup(x) <- InGroup(x) ~= NewInGroup(x).",
           True)
idp.Define("!x[Student] g[Group]: UnsatInGroup(x,g) <- WantsInGroup(x,g,p) &"
           " NewInGroup(x) ~= g.", True)

sols = idp.minimize("Total")

newgroups = []
for sol in sols:
    newgroups.append(sol['NewInGroup'])
print(newgroups)
print("Verschil tussen sols:")
idp.compare(newgroups)
# idp.compare(sols)

sudoku

Sudokusolver.

Contains:

• nbmodels option
• Type
• Constant, with value
• Predicate
• Function
• Constraint
• Define
• Modelexpansion

#!/usr/bin/python3

"""
This testfile solves a sudoku.

"""
from pathlib import Path
from pyidp3.typedIDP import *


home = str(Path.home())
idp = IDP(home+"/idp/usr/local/bin/idp")
idp.nbmodels = 10

idp.Type("Row", (1, 9))
idp.Type("Column", (1, 9))
idp.Type("Number", (1, 9))

start_numbers = [(1, 1, 8), (1, 1, 8),
                 (2, 3, 3), (2, 4, 6),
                 (3, 2, 7), (3, 5, 9), (3, 7, 2),
                 (4, 2, 5), (4, 6, 7),
                 (5, 5, 4), (5, 6, 5), (5, 7, 7),
                 (6, 4, 1), (6, 8, 3),
                 (7, 3, 1), (7, 8, 6),
                 (7, 9, 8),
                 (8, 3, 8),
                 (8, 4, 5),
                 (8, 8, 1),
                 (9, 2, 9),
                 (9, 7, 4)]
idp.Predicate("Square(Row, Column, Row, Column)")
idp.Predicate("Start(Row,Column,Number)", start_numbers)
idp.Predicate("Group(Row, Column, Row, Column)")
idp.Function("Solution(Row, Column): Number")

idp.Constraint("!r[Row] c[Column] number: Start(r, c, number) =>"
               "Solution(r, c) = number", True)
idp.Define("!r1[Row] c1[Column] r2[Row] c2[Column]:"
           "Square(r1,c1,r2,c2) <- r1- (r1-1)%3 = "
           " r2 - (r2-1)%3 & c1-(c1-1)%3 = c2-(c2-1)%3",
           True)
idp.Define("!r1[Row] c1[Column] r2[Row] c2[Column]: Group(r1, c1, r2, c2) "
           "<- Square(r1, c1, r2, c2).\n"
           "!r1[Row] r2[Row] c[Column]: Group(r1, c, r2, c) <- true.\n"
           "!r[Row] c1[Row] c2[Column]: Group(r, c1, r, c2).", True)
idp.Constraint("!r1[Row] c1[Column] r2[Row] c2[Column]: Group(r1, c1, r2, c2)"
               "& (r1 ~= r2 | c1 ~= c2) => Solution(r1,c1) ~="
               "Solution(r2,c2)", True)
idp.check_sat()
sols = idp.model_expand()
for index, sol in enumerate(sols):
    if sol['satisfiable']:
        print("Sol{:d}: ".format(index), sol['Solution'])

masyu

Contains:

• Type, constructed_from
• Constant, with value
• Predicate
• Function
• Constraint
• Define
• Satchecking
• Modelexpansion

#!/usr/bin/python3

"""
This is by far the testfile with the most in it (yet it's not the hardest!).
It solves a masyu puzzle.

"""
from pathlib import Path
from pyidp3.typedIDP import *


home = str(Path.home())
idp = IDP(home+"/idp/usr/local/bin/idp")

idp.Type("Row", (0, 4))
idp.Type("Column", (0, 4))
idp.Type("Pearl", ["Hollow", "Filled"], constructed_from=True)
idp.Type("Wire", ["NS", "EW", "ES", "WS", "NE", "NW", "Empty"],
         constructed_from=True)

pearl_position = [(0, 2, "Filled"),
                  (1, 4, "Filled"),
                  (2, 2, "Filled"),
                  (3, 0, "Filled"), (3, 1, "Filled"),
                  (4, 4, "Hollow")]
idp.Predicate("PearlPosition(Row, Column, Pearl)", pearl_position)
idp.Predicate("WireStraight(Wire)", ["NS", "EW"])
idp.Predicate("WireCurve(Wire)", ["ES", "WS", "NE", "NW"])
idp.Predicate("WireNorth(Wire)", ["NS", "NE", "NW"])
idp.Predicate("WireEast(Wire)", ["ES", "NE", "EW"])
idp.Predicate("WireSouth(Wire)", ["NS", "WS", "ES"])
idp.Predicate("WireWest(Wire)", ["EW", "WS", "NW"])
idp.Predicate("Link(Row, Column, Row, Column)")
idp.Predicate("Connected(Row, Column, Row, Column)")
idp.Function("Solution(Row, Column): Wire")

idp.Constraint("!r c: WireNorth(Solution(r,c)) => WireSouth(Solution(r-1,c))",
               True)
idp.Constraint("!r c: WireSouth(Solution(r,c)) => WireNorth(Solution(r+1,c))",
               True)
idp.Constraint("!r c: WireEast(Solution(r,c)) => WireWest(Solution(r,c+1))",
               True)
idp.Constraint("!r c: WireWest(Solution(r,c)) => WireEast(Solution(r,c-1))",
               True)
idp.Constraint("!r c parel: PearlPosition(r,c,parel) & parel = Hollow => "
               "WireCurve(Solution(r,c))", True)
idp.Constraint("!r c parel: PearlPosition(r,c,parel) & parel = Filled => "
               "WireStraight(Solution(r,c))", True)
idp.Constraint("!r c parel: PearlPosition(r,c,parel) & parel = Hollow & "
               "WireNorth(Solution(r,c)) => WireStraight(Solution(r-1,c))",
               True)
idp.Constraint("!r c parel: PearlPosition(r,c,parel) & parel = Hollow & "
               "WireSouth(Solution(r,c)) => WireStraight(Solution(r+1,c))",
               True)
idp.Constraint("!r c parel: PearlPosition(r,c,parel) & parel = Hollow & "
               "WireEast(Solution(r,c)) => WireStraight(Solution(r,c+1))",
               True)
idp.Constraint("!r c parel: PearlPosition(r,c,parel) & parel = Hollow & "
               "WireWest(Solution(r,c)) => WireStraight(Solution(r,c-1))",
               True)
idp.Constraint("!r c parel: PearlPosition(r,c,parel) & parel = Filled & "
               "WireNorth(Solution(r,c)) => (WireCurve(Solution(r-1,c)) | "
               "WireCurve(Solution(r+1,c)))", True)
idp.Constraint("!r c parel: PearlPosition(r,c,parel) & parel = Filled & "
               "WireEast(Solution(r,c)) => (WireCurve(Solution(r,c-1)) | "
               "WireCurve(Solution(r,c+1)))", True)
idp.Constraint("!r1 c1 r2 c2: (Solution(r1,c1) ~= Empty & Solution(r2,c2) ~= "
               "Empty) => Connected(r1,c1,r2,c2)", True)
idp.Define("!r c: Link(r,c,r-1,c) <- WireNorth(Solution(r,c)) & "
           "WireSouth(Solution(r-1,c)). "
           "!r c: Link(r,c,r+1,c) <- WireSouth(Solution(r,c)) & "
           "WireNorth(Solution(r+1,c)). "
           "!r c: Link(r,c,r,c+1) <- WireEast(Solution(r,c)) & "
           "WireWest(Solution(r,c+1)). "
           "!r c: Link(r,c,r,c-1) <- WireWest(Solution(r,c)) &"
           "WireEast(Solution(r,c-1)).", True)

idp.Define("!r1 c1 r2 c2: Connected(r1,c1,r2,c2) <- Link(r1,c1,r2,c2). "
           "!r1 c1 r2 c2: Connected(r1,c1,r2,c2) <- ?r3 k3: "
           "Connected(r3,k3,r2,c2) & Connected(r1,c1,r3,k3). ", True)
idp.check_sat()
idp.model_expand()