pb обозначает псевдо-логическое. Псевдо-булева функция - это функция от логического значения до некоторого другого домена, обычно Real. conflict происходит, когда выбор переменной приводит к неудовлетворительному набору предложений, после чего решатель должен вернуться назад. Поддержание минимального обратного отслеживания крайне важно для эффективности, и многие из двигателей SAT тщательно отслеживают это число. Хотя детали полностью зависят от решателя (т. Е. Эти два числа, о которых вы спрашиваете), в целом, чем выше эти числа, тем больше конфликтных ситуаций встречается, и, следовательно, может быть принято решение полностью сбросить состояние или предпринять какое-либо другое действие. Часто есть параметры, которые пользователи могут установить, чтобы указать, когда такие действия предпринимаются, и какие именно. Но опять же, это полностью решает и зависит от реализации.
Поиск в Google по псевдобулевой оптимизации приведет к множеству научных статей, которые вы, возможно, захотите просмотреть.
Если вы действительно хотите найти обработку псевдо-логических значений в Z3, тогда вам лучше всего взглянуть на саму реализацию: https://github.com/Z3Prover/z3/blob/master/src/smt/theory_pb.cpp