ограничение мощности z3 для CNF

Question

Я использую z3py для преобразования ограничений мощности в CNF. Я использовал тактику t = Then('simplify', 'card2bv', 'simplify', 'bit-blast', 'tseitin-cnf'). У моей цели 100 ограничений по 800 переменным. Преобразование занимает около 48 минут на процессоре Intel Xeon. Является ли тактика, которую я использовал, наиболее эффективной для такого рода ограничений с точки зрения компактности или скорости?

Реализует ли z3 что-то вроде последовательных счетчиков из Sinz, 2005 [1]?

[1] http://www.carstensinz.de/papers/CP-2005.pdf

Answer 1

Z3 способен использовать ограничения псевдобулевого неравенства, которые могут быть использованы выразить мощность.

import z3

s = z3.Solver()
bvars = [z3.Bool("Var {0}".format(x)) for x in range(10)]
#Exactly 3 of the variables should be true
s.add( z3.PbEq([(x,1) for x in bvars], 3) )
s.check()
m = s.model()

s = z3.Solver()
bvars = [z3.Bool("Var {0}".format(x)) for x in range(10)]
#<=3 of the variables should be true
s.add( z3.PbLe([(x,1) for x in bvars], 3) )
s.check()
m = s.model()

s = z3.Solver()
bvars = [z3.Bool("Var {0}".format(x)) for x in range(10)]
#>=3 of the variables should be true
s.add( z3.PbGe([(x,1) for x in bvars], 3) )
s.check()
m = s.model()