I originally posted the same question on the Japanese version of Stack Overflow, but since it has been 20 days without any answers or comments, I’m posting it here as well.

I’m trying to create a CNF that is difficult to prove unsatisfiable with a SAT Solver. The pigeonhole principle is a known example of a CNF that is difficult to prove unsatisfiable. The pigeonhole principle is the proposition that, if there are n+1 pigeons and n pigeonholes, the following two conditions cannot be satisfied simultaneously:

1. Every pigeon is placed in one of the pigeonholes.
2. No more than one pigeon is placed in each pigeonhole.

It is known that SAT Solvers based solely on CDCL (conflict-driven clause learning) cannot prove the pigeonhole principle in polynomial time. However, SAT Solvers based on SDCL (satisfaction-driven clause learning) can prove the pigeonhole principle in polynomial time (surprisingly fast, actually).

I’ve considered the following CNF as one that might be difficult to solve even for SAT Solvers based on SDCL:

An n-bit natural number x cannot simultaneously satisfy the following two conditions:

1. x is a prime number.
2. x is a composite number.

I’ve named this proposition the “prime and composite tautology.” For proving that x is a prime number, I used this theory. It’s quite challenging to construct this CNF directly, so I decided to use tools called yosys 0.9 (git sha1 1979e0b) and abc 1.01.

Here’s the code I wrote. However, there’s a problem: yosys applies optimizations, and the generated CNF becomes trivially unsatisfiable. How can I generate a meaningful CNF without letting yosys perform optimizations?

What did you try:
I downloaded the yosys source code from GitHub, built it, and tried using it, but it didn’t work.

What were you expecting:
I expected to generate an unsatisfiable CNF (preferably difficult for a SAT solver to solve) that retains the structure of the prime and composite tautology.