1

I have two .cnf files containing CNF clauses. Both these files solve one problem, which means that the CNF clauses in the two files are the same, but the order of CNF clauses in each file is different. I've set timeout = 1800s, but only one .cnf file can solve that problem in 1800s, the other doesn't. Hence, I wonder if the order of CNF clauses in .cnf file affects the way Sat4j solve the problem or not.

I want to know more about the way Sat4j (Minisat) solves CNF clauses.

Anh
  • 13
  • 5
  • For such questions, sat4j provides a [list of references](https://www.sat4j.org/allabout.php). The [Wikipedia entry](https://en.wikipedia.org/wiki/SAT_solver#CDCL_solvers) is also a possible starting point. – Axel Kemper Apr 06 '23 at 21:17
  • @AxelKemper As far as I know, these documents don't mention this issue. – Anh Apr 07 '23 at 07:16
  • Yes. The references are meant to address your final question. Most If not all SAT solvers have a high degree of non-determinism. Therefore, the ordering of clauses may have a similar effect than a changed seed value of their random number generator. – Axel Kemper Apr 07 '23 at 13:50

0 Answers0