From 9c30d01414561e579c0d8f474d7f3171f77b478e Mon Sep 17 00:00:00 2001
From: Mark Powers <mark@marks.kitchen>
Date: Sun, 14 Jul 2024 15:25:52 -0500
Subject: Initial commit

---
 convert_to_sat.py | 266 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 266 insertions(+)
 create mode 100644 convert_to_sat.py

(limited to 'convert_to_sat.py')

diff --git a/convert_to_sat.py b/convert_to_sat.py
new file mode 100644
index 0000000..d538b08
--- /dev/null
+++ b/convert_to_sat.py
@@ -0,0 +1,266 @@
+from z3 import *
+import sys
+
+
+variables = {}
+def reachable(graph, node_reachable):
+    # check reachability to node_reachable
+    clauses = []
+    # at least one pebble can be gotted to node_reachble (from config or otherwise)
+    clauses.append(1 <= Sum(list(variables[node_reachable]["in"].values())))
+    return clauses
+
+def build_model(graph, add_property, node_reachable, config=None, config_count=0):
+    clauses = []
+    for node in graph["v"]:
+        variables[node] = {"out":{}, "in":{}}
+    # creat symbolic variables for each edge in/out
+    for node in graph["v"]:
+        for edge in graph["e"][node]:
+            variables[node]["out"][edge] = Int(node+"_out_"+edge)
+            variables[edge]["in"][node] = Int(edge+"_in_"+node)
+        # add initial pebbles
+        variables[node]["in"]["config"] = Int(node+"_in_config")
+
+
+    if config is not None:
+        for node in graph["v"]:
+            clauses.append(variables[node]["in"]["config"] == config[node])
+    else:
+        sum_terms = []
+        for node in graph["v"]:
+            clauses.append(variables[node]["in"]["config"] >= 0)
+            sum_terms.append(variables[node]["in"]["config"])
+        clauses.append(Sum(sum_terms) == config_count)
+
+    # make edges linked
+    for node in graph["v"]:
+        for edge in graph["e"][node]:
+            clauses.append(variables[node]["out"][edge] == variables[edge]["in"][node])
+
+    # encode possible moves
+    # make sure we don't move too many total from pebble
+    for node in graph["v"]:
+        sum_out = Sum(list(variables[node]["out"].values()))
+        sum_in = Sum(list(variables[node]["in"].values()))
+        # The number of pebbles out from a node is no more than half the sum
+        # of all pebbles that are moved into a node
+        clauses.append( Implies(sum_in % 2 == 0,  sum_out <= (sum_in/2 )) )
+        clauses.append( Implies(sum_in % 2 == 1,  sum_out <= ((sum_in-1)/2 )) )
+    # make sure each move is a valid amount
+    for node in graph["v"]:
+        for in_var in variables[node]["in"].values():
+            clauses.append(in_var >= 0)
+        for out_var in variables[node]["out"].values():
+            sum_in = Sum(list(variables[node]["in"].values()))
+            clauses.append( 
+                    Implies(And(sum_in % 2 == 0, sum_in > 2),
+                            And(0 <= out_var, out_var <= (sum_in/2 ))) )
+            clauses.append( 
+                    Implies(And(sum_in % 2 == 1, sum_in > 2),
+                            And(0 <= out_var, out_var <= ((sum_in-1)/2 ))) )
+
+    # encode cycle lemma
+    # TODO get all cycles, and remove them?
+    for node in graph["v"]:
+        # if we along one edge, do not move back along it
+        for edge in graph["e"][node]:
+            in1 = variables[node]["in"][edge]
+            in2 = variables[edge]["in"][node]
+            clauses.append(Implies(in1 > 0, in2 == 0))
+    clauses += add_property(graph, node_reachable)
+
+    return And(clauses)
+
+def is_sat(f, output=True):
+    s = Solver()
+    s.add(f)
+    if output:
+        print(f)
+    if s.check() == sat:
+        if output:
+            print("SAT")
+        model = s.model()
+        # print(model)
+        moves = []
+        for key in model:
+            if "_in_" in key.name() and 0<model[key].as_long():
+                parts = key.name().split("_in_")
+                if parts[1] != "config":
+                    moves.append(parts[1] + " sends " + str(model[key])+" pebbles to "  +parts[0])
+        moves.sort()
+        if output:
+            print("\n".join(moves))
+        return moves
+    if output:
+        print("UNSAT")
+    return None
+
+def test_simple_path():
+    config = {
+        "a": 4,
+        "b": 0,
+        "c": 0,
+    }
+    graph = {
+        "v": ["a", "b", "c"],
+        "e": {
+            "a": ["b"],
+            "b": ["a", "c"],
+            "c": ["b"],
+        },
+    }
+    node_reachable = "c"
+    run_reachable_test_case(graph, config, node_reachable, True)
+
+    config = {
+        "a": 3,
+        "b": 0,
+        "c": 0,
+    }
+    run_reachable_test_case(graph, config, node_reachable, False)
+
+    config = {
+        "a": 5,
+        "b": 0,
+        "c": 0,
+    }
+    run_reachable_test_case(graph, config, node_reachable, True)
+
+    config = {
+        "a": 2,
+        "b": 1,
+        "c": 0,
+    }
+    run_reachable_test_case(graph, config, node_reachable, True)
+
+def test_cycle():
+    config = {
+        "a": 4,
+        "b": 0,
+        "c": 0,
+        "d": 0,
+    }
+    graph = {
+        "v": ["a", "b", "c", "d"],
+        "e": {
+            "a": ["b", "d"],
+            "b": ["a", "c"],
+            "c": ["b", "d"],
+            "d": ["a", "c"],
+        },
+    }
+    node_reachable = "c"
+    run_reachable_test_case(graph, config, node_reachable, True)
+
+def test_merge():
+    #   a
+    #  / \
+    # b   c
+    #  \ /
+    #   d
+    #   |
+    #   e
+    graph = {
+        "v": ["a", "b", "c", "d", "e"],
+        "e": {
+            "a": ["b", "c"],
+            "b": ["a", "d"],
+            "c": ["a", "d"],
+            "d": ["b", "c", "e"],
+            "e": ["d"],
+        },
+    }
+    node_reachable = "e"
+    config = {
+        "a": 4,
+        "b": 1,
+        "c": 1,
+        "d": 0,
+        "e": 0,
+    }
+    run_reachable_test_case(graph, config, node_reachable, True)
+
+    config = {
+        "a": 4,
+        "b": 1,
+        "c": 0,
+        "d": 0,
+        "e": 0,
+    }
+    run_reachable_test_case(graph, config, node_reachable, False)
+
+def test_lemke():
+    #  /-x-\
+    # / | | \
+    # a-b c d
+    # \ \ | /
+    #  e--f
+    #   \/
+    #    v
+    graph = {
+        "v": ["a", "b", "c", "d", "e", "f", "v", "x"],
+        "e": {
+            "a": ["b", "e", "x"],
+            "b": ["a", "f", "x"],
+            "c": ["x", "f"],
+            "d": ["x", "f"],
+            "e": ["a", "f", "v"],
+            "f": ["b", "c", "d", "e", "v"],
+            "v": ["e", "f"],
+            "x": ["a", "b", "c", "d"],
+        },
+    }
+    config = {
+        "a": 0,
+        "b": 0,
+        "c": 0,
+        "d": 0,
+        "e": 0,
+        "f": 0,
+        "v": 0,
+        "x": 8,
+    }
+    run_reachable_test_case(graph, config, "v", True)
+
+    config = {
+        "a": 1,
+        "b": 1,
+        "c": 1,
+        "d": 1,
+        "e": 0,
+        "f": 0,
+        "v": 0,
+        "x": 4,
+    }
+    run_reachable_test_case(graph, config, "v", True)
+    run_pebbling_number_test_case(graph, 7)
+
+def run_reachable_test_case(graph, config, node_reachable, expected_is_sat):
+    variables = {}
+    z3_model = build_model(graph, reachable, node_reachable, config=config)
+    out = is_sat(z3_model, output=False)
+    if (expected_is_sat and not out) or (not expected_is_sat and out):
+        print(z3_model)
+        print(out)
+        print("failed!")
+
+def run_pebbling_number_test_case(graph, count):
+    variables = {}
+    for node_reachable in graph["v"]:
+        # TODO model is wrong, we need to say there is not a configure in
+        # which this isn't possible. This is solvability?
+        z3_model = build_model(graph, reachable, node_reachable, config_count=count)
+        out = is_sat(z3_model, output=False)
+        if not out:
+            print("failed peb. number: ", count, node_reachable)
+        print(out)
+
+def main():
+    test_simple_path()
+    test_cycle()
+    test_merge()
+    test_lemke()
+
+if __name__ == '__main__':
+    main()
-- 
cgit v1.2.3