Optimization
The current function "satisfyopt(n,clauseall,clauseneg)" is identical
with the nonoptimized version. The variable "n" is the number of
variables, the variables "clauseall" and "clauseneg" are arrays of
numbers representing a clause. To understand the coding, one has
to view upon the numbers in binary form and to write them from lower
bits to higher bits instead of the usual way from higher bits to lower ones.
Here an example stating that Clause[2] is not x[0] or x[3] or not x[4]:
Variable Decimal Number Binary from low to high Meaning: which variables
clauseall[2] 25 10011000 x[0], x[3], x[4] occur
clauseneg[2] 17 10001000 x[0], x[4] negated
In general, if the bit i is 1 in clauseall[j] then this
means that x[i] occurs in the Clause[j]. Furthermore, if bit i is also set
in clauseneg[j] then this means that not "x[i]" but its negation ("neg x[i]")
occurs in Clause[j]. The implemented function downcounts a variable a
in steps one from the starting solution to the last possible value which
is 0. In the case that a clause is not satisfied, this downcounting
might be speeded up and this might be an key idea to spead up the
whole function. It might be useful to precompute some information
before entering the loop as well in order to speed up the operations
inside the loop. Having done this, the resulting function should perform
well for 20 variables without a warning that a script causes the page
to run slowly.