<p>You can turn it into CNF using <a href="https://en.wikipedia.org/wiki/Tseitin_transformation" rel="nofollow">the Tseitin transform</a>.  Some SAT front-ends will do the transformation for you: for instance, the <a href="https://stp.github.io/" rel="nofollow">STP solver</a> has native support for all of those operations and thus can handle the transformation for you.</p>

CC BY-SA 3.0
2015-09-16T06:17:24.910Z
2015-09-16T06:17:24.910Z
D.W.
<p>I have a constraint like d >= a ^ b ^ c, where a,b,c,d are binary, ^ is XOR.</p>

<p>Is this a pseudo boolean modularity constraint or not? Most Pseudo boolean modularity constraints I saw are with equality, which confuses me a lot.</p>

<p>My question is</p>

<ol>
<li><p>what is this constraint, a pseudo boolean modularity or something else?</p></li>
<li><p>How can I turn it into a CNF</p></li>
</ol>

<p>Thank you in advance!</p>

<sat>
pseudo boolean modularity constraint?
HoneyB
# pseudo boolean modularity constraint?

(Asked by: username_0 on 2015-09-15)

I have a constraint like d >= a ^ b ^ c, where a,b,c,d are binary, ^ is XOR.

Is this a pseudo boolean modularity constraint or not? Most Pseudo boolean modularity constraints I saw are with equality, which confuses me a lot.

My question is

1. what is this constraint, a pseudo boolean modularity or something else?
2. How can I turn it into a CNF

Thank you in advance!

**Tags:** sat


---

## 1 answers

### Answer by username_1 on 2015-09-16. Score: 2 | Accepted answer

You can turn it into CNF using [the Tseitin transform](https://en.wikipedia.org/wiki/Tseitin_transformation). Some SAT front-ends will do the transformation for you: for instance, the [STP solver](https://stp.github.io/) has native support for all of those operations and thus can handle the transformation for you.


---

