I need SAT instances, involving 9 to 20 variables. They need to be hard to solve for humans. Both SAT and UNSAT instances are needed.

I tried random-SAT generators on the web, but the results were not satisfactory because they are trivial. A good example of what I'm looking for is the following 4-variable instance from The Art of Computer Programming: $$12\bar3, 23\bar4, 134, \bar124, \bar1\bar23, \bar2\bar34, \bar1\bar3\bar4, 1\bar2\bar4.$$

  • 3
    $\begingroup$ "They need to be hard to solve for humans." Arguably any SAT instance would do since the average human does not even know what SAT is. $\endgroup$ – dkaeae Jan 25 '19 at 8:40
  • $\begingroup$ Start building a solution, and add random SAT lines that respects it until no other solution is possible. You won't likely obtain a trivial problem with 9 to 20 variables. $\endgroup$ – Optidad Jan 25 '19 at 9:20
  • $\begingroup$ @Vince: I tried random kSAT with 9 variables, 6 literals per clause and 600 clauses and finally got it to be unsatisfiable. 500 clauses wouldn't work. It's so big. I need smaller and more carefully designed instances. $\endgroup$ – Zirui Wang Feb 5 '19 at 4:05
  • $\begingroup$ @dkaeae Best but not so lucky human. $\endgroup$ – Zirui Wang Feb 13 '19 at 12:46
  • 1
    $\begingroup$ Generating random instances is unlikely to work: random SAT is computationally easy in most parameterizations. $\endgroup$ – David Richerby Aug 14 '19 at 13:10

To build a satisfiable instance, start by picking an assignment to the variables that will be a solution. Then, randomly generate clauses that are satisfied by this assignment. Add as many clauses as desired. If you add enough clauses, then with high probability your chosen solution will be the only one, and the problem will be non-trivial.

For instance, suppose your assignment is $x_1=\text{True}$, $x_2=\text{False}$. Then you could add any subset of the clauses $x_1 \lor x_2$, $x_1 \lor \neg x_2$, or $\neg x_1 \lor \neg x_2$. For example, one random formula you could generate might be $(x_1 \lor x_2) \land (\neg x_1 \lor \neg x_2)$.

To build an unsatisfiable instance, proceed as above; then add one more clause that is violated by the solution you chose in advance. If you added enough clauses, it is likely that there will be no other solution, so the problem will be unsatisfiable. Check with a SAT solver just to be sure.

  • $\begingroup$ Give me an instance, maybe. $\endgroup$ – Zirui Wang Feb 13 '19 at 12:43
  • $\begingroup$ @ZiruiWang, See edited answer for a simple example. You should be able to generate more yourself using the procedure listed here. That will involve writing a little bit of code; since it's your problem, I'll let you do that, as I have no particular interest in writing the code myself. $\endgroup$ – D.W. Feb 13 '19 at 16:58
  • 1
    $\begingroup$ @ZiruiWang, I don't follow you. I'm not sure what distinction you're tryin g to draw. When you talk about efficiency, I'm not sure what you're trying to compare about. My answer is not based on efficiency; it's based on meeting your requirements. $\endgroup$ – D.W. Feb 19 '19 at 5:49
  • 1
    $\begingroup$ @ZiruiWang, OK. I suggest writing a new question, where you define these new requirements in a precise way. I recommend that you state how small you need them to be; that you define "better"; that you list the metrics or criteria you will use to evaluate possible solutions; and that you show what methods you've already tried and how well they work along those metrics. That might help us meet your needs better. $\endgroup$ – D.W. Feb 21 '19 at 18:16
  • 1
    $\begingroup$ @ZiruiWang, if you can't articulate your requirements clearly, we probably can't come up with a scheme that meets them. $\endgroup$ – D.W. Feb 23 '19 at 19:46

I will do a quick calculation to show that small instances are rare. Consider an UNSAT instance. Suppose it’s $k$-SAT and every clause has exactly $k$ literals. Then there are at least $k$ variables, or some clauses will be trivial. So there are $2^k$ assignments and all of them have to be unsatisfiable. An assignment is unsatisfiable if there is a clause, in which all literals are false. When this happen, let’s call the assignment is covered by the clause. So your aim is to cover the entire $2^k$ assignments by clauses. But in this case, a clause can cover at most 1 assignment, so there are at least $2^k$ clauses in order to be unsatisfiable. When $k=6$, this is 64 and this is optimal. When $k=9$, this is 512. When $n>k$, the best case doesn’t change, but the probability shrinks as there is more noise.

  • $\begingroup$ OK but this doesn't answer your question. $\endgroup$ – David Richerby Aug 14 '19 at 13:09
  • $\begingroup$ @DavidRicherby OK but this shows that my expectation was too high and thus gives some kind of a negative answer: the instances have to be huge. Especially if you calculate the probabilities. By the way, I did figure out a way to generate instances both systematically and randomly. And also the number of instances, which is doubly exponential. So it’s better to survey rather than scan. That’s where I get. And the covering idea suggests that I should seek efficient data structures if I want to create a new, fast SAT solver. I.e., if everything is covered then it’s UNSAT and vice versa. Any idea? $\endgroup$ – Zirui Wang Aug 14 '19 at 13:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.