CODEWITHSUNDEEP
sat
MSJ
MSJ

Reputation: 97

Converting Problems to CIRCUIT-SAT

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

Upvotes: 1

Views: 368

Answers (1)

Valentin Montmirail
Valentin Montmirail

Reputation: 2640

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 :

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 :).

Upvotes: 1

Related Questions