Regarding Cardinality Constraint Encoding

[hadipourh]

Dear Nikolaj,

Hope you are well. I have created a cryptographic tool in which I am using Z3 as a SMT solver and as a CNF converter as well. Regarding the former one (as the converter), I am using it to convert a SMT problem to the CNF format in which all constraints are simple logical constraints except for one which is a cardinality constraint. The aim of this conversion is using the state of the art SAT solvers. You might know a better tool to do this. If so, I would be most grateful if you let me know.

I am using the following commands to convert my SMT problem to the CNF format:

        G = z3.Goal()
        G.add(solver.assertions())
        cnf_format = z3.Then("card2bv", "tseitin-cnf")
        temp = cnf_format(G)
        dimacs_format = temp[0].dimacs()

I checked it several times, and it works well. However, I am not sure if it is the best way for this conversion? Besides does it always preserve the satisfiability of the original SMT problem?

I had also the following observation:

• When I use cnf_format = z3.Tactic("card2bv") or cnf_format = z3.Then('simplify', 'bit-blast', 'tseitin-cnf'), it doesn't preserve the satisfiability. I mean the original SMT problem is UNSAT, while the converted one become SAT. Thank you in advance for your time.

Kind regards,
Hosein

[NikolajBjorner]

There are a number of different ways to control the encoding. These weren't well exposed so I have pushed a fix for this now.
With the fix, you can run the following tests to explore the space:

(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)
(declare-const u Bool)
(push)
(assert ((_ at-most 2) x y z u))
(apply (using-params card2bv :cardinality.encoding unate))
(apply (using-params card2bv :cardinality.encoding grouped))
(apply (using-params card2bv :cardinality.encoding ordered))
(apply (using-params card2bv :cardinality.encoding bimander))
(apply (using-params card2bv :cardinality.encoding circuit))
(pop)

(push)
(assert ((_ pble 4 2 3 1 2) x y z u))
(apply (using-params card2bv :pb.solver solver))
(apply (using-params card2bv :pb.solver circuit))
(apply (using-params card2bv :pb.solver totalizer))
(apply (using-params card2bv :pb.solver sorting))
(apply (using-params card2bv :pb.solver binary_merge))
(pop)

When pb.solver is set to solver, which is the default, Pseudo-Booleans are not going to be converted.
With the other options it may produce bit-vectors or just clauses.
You would need to bit-blast the bit-vectors before converting to CNF. Otherwise, the dimacs file is only an abstraction and does not preserve satisfiability. Generally, you can create a dimacs serialized output from non-propositional formulas. Since dimacs only captures propositional logic this information wil be lost in the output. The dimacs output should then contain information about this abstraction as comments in the end of the file.

[hadipourh]

Thanks for your kind helps.