7l7w - 3 colors solutions in SMT solvers

cvc4_pysmt.py

#!/usr/bin/env python3

# Installing CVC4's python bindings is a PITA, so we use the
# pysmt wrapper instead.

# Enum/Sum types not yet supported...
#  https://github.com/pysmt/pysmt/issues/187
#  https://github.com/pysmt/pysmt/issues/538

# This program is based on:
# - https://github.com/pysmt/pysmt/blob/master/examples/einstein.py
# - https://github.com/pysmt/pysmt/blob/master/examples/allsmt.py

from pysmt.shortcuts import (Symbol, Or, And, Not,
                             ExactlyOne, Implies, AtMostOne,
                             NotEquals, EqualsOrIff)
from pysmt.shortcuts import get_model, get_env, Solver
from pysmt.oracles import get_logic


def state_color_sym(state, color):
    assert color in Colors
    assert state in States
    return Symbol(f'{state}_has_color_{color}') # Boolean symbol


def adjacent_state_cond(state1, state2):
    return And(
        # For each color, and a given pair of states, at most one state
        # in the pair can be of that color.
        AtMostOne(state_color_sym(state1, col), state_color_sym(state2, col))
        for col in Colors
      )


def get_state_color_from_model(state, model):
    return next(
      color
          for color in Colors
          if model[state_color_sym(state, color)].is_true()
    )


def print_result(model):
    for state in States:
        color = get_state_color_from_model(state, model)
        print(f'{state} -> {color}')


def solve_one_solution(formula):
    target_logic = get_logic(final_formula)
    with Solver(name='cvc4', logic=target_logic) as solver:
        solver.add_assertions([final_formula])
        res = solver.solve()
        model = solver.get_model()

    print_result(model)


def solve_all_solutions(formula):
    target_logic = get_logic(formula)
    variables = formula.get_free_variables()
    with Solver(name='cvc4', logic=target_logic) as solver:
        solver.add_assertion(formula)
        soln = 1
        while solver.solve():
            print('-' * 80)
            print(f'Solution #{soln}:')
            soln += 1
            print_result(solver.get_model())

            # To generate new results, disallow the generation of previous ones.
            # EqualsOrIff allows mixing theory and bool variables
            partial_model = [EqualsOrIff(k, solver.get_value(k)) for k in variables]
            solver.add_assertion(Not(And(partial_model)))
        print('-' * 80)



Colors = 'red', 'green', 'blue'
#States = 'Alabama', 'Mississippi', 'Georgia', 'Tennessee', 'Florida'
States = 'Alabama', 'Florida', 'Georgia', 'Mississippi', 'Tennessee'


domain = And(
    # each state has exactly one color.
    ExactlyOne(state_color_sym(s, c) for c in Colors) for s in States
)

facts = And(
    adjacent_state_cond('Mississippi', 'Tennessee'),
    adjacent_state_cond('Mississippi', 'Alabama'),
    adjacent_state_cond('Alabama', 'Tennessee'),
    adjacent_state_cond('Alabama', 'Mississippi'),
    adjacent_state_cond('Alabama', 'Georgia'),
    adjacent_state_cond('Alabama', 'Florida'),
    adjacent_state_cond('Georgia', 'Florida'),
    adjacent_state_cond('Georgia', 'Tennessee')
)


final_formula = And(domain, facts)

#print_result(get_model(final_formula, solver_name='cvc4'))
#solve_one_solution(final_formula)
solve_all_solutions(final_formula)

ex_smt.smt2

; Execute as:
;   z3 -smt2 ex_smt.smt2
;
; SMT-LIB files are a sequence of S-expressions.
;
; Specification:
;  - v1.2.1: https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf
;  - v2.6:   https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
;

;; 1. Model description (exported from z3)
(declare-datatypes ((Color 0)) (((red) (green) (blue))))
(declare-fun Tennessee () Color)
(declare-fun Mississippi () Color)
(declare-fun Alabama () Color)
(declare-fun Georgia () Color)
(declare-fun Florida () Color)
(assert (distinct Mississippi Tennessee))
(assert (distinct Mississippi Alabama))
(assert (distinct Alabama Tennessee))
(assert (distinct Alabama Mississippi))
(assert (distinct Alabama Georgia))
(assert (distinct Alabama Florida))
(assert (distinct Georgia Florida))
(assert (distinct Georgia Tennessee))

;; 2. Execute SMT solver
(check-sat)

;; 3. Output results
(echo "Model:")
(get-value (Alabama))
(get-value (Florida))
(get-value (Georgia))
(get-value (Mississippi))
(get-value (Tennessee))

(exit)

tst_boolector.py

#!/usr/bin/env python3

import pyboolector

b = pyboolector.Boolector()

# Enable model generation
b.Set_opt(pyboolector.BTOR_OPT_MODEL_GEN, True)

# Boolector does not support enums...
#  https://github.com/Boolector/boolector/issues/177
# Let's use a bitvector of 2 bits instead (discard `11`).

discard_val = b.Const("11")

# Data types ("sorts") declaration
bvsort2 = b.BitVecSort(2)

# Declare "variables"
Alabama = b.Var(bvsort2, "Alabama")
Mississippi = b.Var(bvsort2, "Mississippi")
Georgia = b.Var(bvsort2, "Georgia")
Tennessee = b.Var(bvsort2, "Tennessee")
Florida = b.Var(bvsort2, "Florida")


b.Assert(Mississippi != Tennessee)
b.Assert(Mississippi != Alabama)
b.Assert(Alabama != Tennessee)
b.Assert(Alabama != Mississippi)
b.Assert(Alabama != Georgia)
b.Assert(Alabama != Florida)
b.Assert(Georgia != Florida)
b.Assert(Georgia != Tennessee)

b.Assert(discard_val != Alabama)
b.Assert(discard_val != Mississippi)
b.Assert(discard_val != Georgia)
b.Assert(discard_val != Tennessee)
b.Assert(discard_val != Florida)


bv_to_str = {
    '00': 'red',
    '01': 'green',
    '10': 'blue',
    # '11': 'invalid',
}

result = b.Sat()

match result:
    case b.SAT:
        print('Solution found:')
        print(f' Alabama:     {bv_to_str[Alabama.assignment]}')
        print(f' Florida:     {bv_to_str[Florida.assignment]}')
        print(f' Georgia:     {bv_to_str[Georgia.assignment]}')
        print(f' Mississippi: {bv_to_str[Mississippi.assignment]}')
        print(f' Tennessee:   {bv_to_str[Tennessee.assignment]}')
        
        print('\n\nModel dump:')
        b.Print_model()
    case b.UNSAT:
        print('No solution exists')
    case b.UNKNOWN:
        # https://stackoverflow.com/a/11197516/2180200
        print('unknown result!')

b.Print_model()

tst_z3.py

#!/usr/bin/env python3

# Some tutorials and examples:
# - https://ericpony.github.io/z3py-tutorial/guide-examples.htm
# - https://sat-smt.codes/SAT_SMT_by_example.pdf
# - https://github.com/Z3Prover/z3/blob/z3-4.8.14/examples/python/tutorial/jupyter/advanced.ipynb
# - http://www.cs.toronto.edu/~victorn/tutorials/z3/index.html
# - https://web.archive.org/web/20210119175613/https://rise4fun.com/Z3/tutorial/guide
# - https://theory.stanford.edu/~nikolaj/programmingz3.html

import z3

def main():
    # from z3 import *

    # Declare SMT logic types (a.k.a "sorts")

    # Color is an enumerated sort with 3 valid values.
    Color, (red, green, blue) = z3.EnumSort('Color', ['red', 'green', 'blue'])
    
    # Declare "variables"
    Alabama, Mississippi, Georgia, Tennessee, Florida = \
         z3.Consts('Alabama Mississippi Georgia Tennessee Florida', Color)

    # create solver.
    s = z3.Solver()

    # add conditions
    # (could also group into a big "And(...)" )
    s.add(
        Mississippi != Tennessee,
        Mississippi != Alabama,
        Alabama != Tennessee,
        Alabama != Mississippi,
        Alabama != Georgia,
        Alabama != Florida,
        Georgia != Florida,
        Georgia != Tennessee
    )

    print('\nS-expr SMT model:')
    print(s.sexpr())
    
    # Find any solution.
    print('\nsolving problem...')
    match s.check():
        case z3.sat:
            print('Solution found:')
            print(s.model())
            print('\n\nS-expr solution:')
            print(s.model().sexpr())
        case z3.unsat:
            print('No solution exists')
        case z3.unknown:
            # https://stackoverflow.com/a/11197516/2180200
            print('unknown result!')

if __name__ == '__main__':
    main()