Z3-solver throws 'model is not available' exception on python 3

Question

Для решения SAT-проблемы я решил использовать Z3-решатель от Microsoft и Python 3. Целью является использование длинной модели (до 500 000 функций) и найти все возможные решения. Чтобы найти их, я хочу добавить первое решение S1 в исходное уравнение и исключить S1 и т. Д. Я сделаю это, используя цикл while. Решение SAT-проблемы важно для меня, потому что я хочу анализировать модели функций.

Но у меня возникла проблема с добавлением sth в исходное уравнение. Поделюсь минимальный пример:

# Import statements 
import sys 
sys.path.insert(0,'/.../z3/bin') 
from z3 import *  # https://github.com/Z3Prover/z3/wiki 

def main(): 

    ''' 
    Solves after transformation a given boolean equation by using the Z3-Solver from Microsoft. 
    ''' 

    fd = dict() 
    fd['_r'] = Bool('_r') 
    fd['_r_1'] = Bool('_r_1') 

    equation = '''And(fd.get("_r"),Or(Not(fd.get("_r")),fd.get("_r_1")))''' 

    # Solve the equation 
    s = Solver() 
    exec('s.add(' + equation + ')') 
    s.check() 
    print(s.model()) 

    ################################### 
    # Successfull until here. 
    ################################### 

    s.add(Or(fd['_r'] != bool(s.model()[fd.get('_r')]))) 
    # s.add(Or(fd['_r'] != False)) 

    s.check() 
    print(s.model()) 


if __name__=='__main__': 
    main() 

Первая линия закодированы после # Successfull... выбрасывает z3types.Z3Exception: model is not available ошибку. Поэтому я попробовал линию выше, добавив просто модель false. Это работает отлично.

Я застрял здесь. Я считаю, что ошибку легко решить, но я не вижу решения. Кто-нибудь из вас? Благодаря!

Answer 1

Модели станут доступны только после того, как s.check() вернется в режим "sat". Модель отображает булевые предложения в {True, False} и , как правило, сопоставляет константы и функции фиксированным значениям. Требование состоит в том, чтобы модель предоставляла интерпретацию , которая удовлетворяет формуле, которая добавляется к решателю '. Мы не знаем, выполнено ли состояние решателя до , мы назвали 's.check()'.

Предположим, что вы хотите сказать:

s.add(Or(fd['_r'] != bool(s.model()[fd.get('_r')]))) 

означает, что в модели, которая удовлетворяет ограничению должны иметь свойство, что если «_r» истинно в соответствии с моделью, то FD [ «_ г»] ! = Истинно, и если '_r' ложно под моделью, то fd ['_ r']! = False. Это эквивалентно высказыванию fd ['_ r']! = '_r'. Поэтому нет необходимости обращаться к значению из '_r' в любой модели, которая может оценить '_r', чтобы сказать что-то об оценке.