Reputation: 97
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: 367
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