Converting Problems to CIRCUIT-SAT

Question

I am interested in converting Partial Weighted Max SAT to SAT. I have been recommended to go through CIRCUIT SAT.

Partial Weighted Max SAT consists of a set of hard clauses and a set of weighted soft clauses. We seek an assignment which satisfies all hard clauses and achieves at least a weight of k from the soft clauses.

How would I encode this as a boolean combinational circuit?

I can see how I can easily encode the hard clauses. But how would I encode the soft clauses, and associate weights with them, and ensure that a weight of at least k is achieved by a satisfying assignment?

Thanks

Answer 1

You need to encode your Partial Weighted Max SAT as a pseudo-boolean problem.

Just consider hard clauses as weighted clauses with a high weight and adapt the target value (the sum).

To encode it as a SAT formula, you can use technics embedded in SMT solvers, for example :

• MiniSAT+
• Z3 by Microsoft Research
• ... (see others here : https://en.wikipedia.org/wiki/Satisfiability_modulo_theories#SMT_solvers)

To understand how, here is an article (Translating Pseudo-Boolean Constraints into SAT) from the creator of MiniSAT+, who will help you to understand.

And from SAT to Circuit SAT, you will have to use the Tseitin transformation, and your problem will be solved :).