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.
SAT solvers are chaotic, in the sense that they are sensitive to seemingly irrelevant input conditions (e.g., the order of the constraints, the random seed, the polarity of the variables).
This butterfly effect follows from the fact that SAT solvers try to solve hard problems. Often, only a couple of solutions exist in a huge search space of possible solutions. Or if the problem is unsatisfiable, there exist only a couple of short resolution proofs in an even larger space of possible resolution proofs. In both cases, the internal heuristics have to "get lucky" to find a solution/proof. Getting lucky depends on all input conditions, hence the performance differences observed when reordering certain CNFs.