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

<p>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. </p>

<p>How would I encode this as a boolean combinational circuit?</p>

<p>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?</p>

<p>Thanks</p>

CC BY-SA 3.0
2015-07-30T08:02:10.007Z
You an encode the Partial Weighted Max SAT as a pseudo-boolean problem (0-1 ILP problem). Just consider hard clauses as weighted clauses with a high weight and adjust the target sum value. To encode it as a boolean formula you can use one of the technique implemented in many [SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) solvers ; see for example this one: [Translating Pseudo-Boolean Constraints into SAT](http://minisat.se/downloads/MiniSat+.pdf) (MiniSAT+).
Marzio De Biasi
CC BY-SA 3.0
2015-07-30T13:29:45.357Z
note that you need logarithmic number of calls to a SAT solver to solve MaxSAT. As pointed above there's a number of encoding cardinality constraits, ie testing whether you can satisfy at least k clauses. Also I should say there's an extensive literature on MaxSAT, with many algorithms. See [this survey](http://dx.doi.org/10.1007/s10601-013-9146-2) for instance.
Mikolas
<sat>
Converting Partial Weighted Max SAT to CIRCUIT SAT
MSJ
# Converting Partial Weighted Max SAT to CIRCUIT SAT

(Asked by: username_0 on 2015-07-29)

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

**Tags:** sat
> **Comments:**
> **username_1**: You an encode the Partial Weighted Max SAT as a pseudo-boolean problem (0-1 ILP problem). Just consider hard clauses as weighted clauses with a high weight and adjust the target sum value. To encode it as a boolean formula you can use one of the technique implemented in many [SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) solvers ; see for example this one: [Translating Pseudo-Boolean Constraints into SAT](http://minisat.se/downloads/MiniSat+.pdf) (MiniSAT+).  
> **username_2**: note that you need logarithmic number of calls to a SAT solver to solve MaxSAT. As pointed above there's a number of encoding cardinality constraits, ie testing whether you can satisfy at least k clauses. Also I should say there's an extensive literature on MaxSAT, with many algorithms. See [this survey](http://dx.doi.org/10.1007/s10601-013-9146-2) for instance.  

---

## 0 answers

