The stuff in this paper/essay/thing is a bit complicated, as it came from a course in Artificial Intelligence, and while I tried to explain it pretty well along the way, don't worry if it doesn't jive with you; nobody else seems to have looked into this problem so it must not be a priority to have vast knowledge on the Local Search algorithm to find solutions to a CNF logic problem.
Here's a link to download it, as the formatting gets funky when it gets thrown on the website. The first little bit will be included to give you a taste of what it's all about.
Have yourself a lovely day and see you when the whims of fate bring me back!
Results of an Experimentation on Backtracking and Local Search Algorithms with CNF by Mac Clevinger, October 11, 2018
This is a brief report on the results of experimentation on the efficiencies of different approaches to finding a solution to sets of sentences in propositional logic modeled in Conjunctive Normal Form (CNF), those approaches being a Backtracking Algorithm and a Local Search Algorithm. The tests used to generate these results comes from random generation of problems in CNF of varying difficulty as represented by the number of clauses and variables.
CNF is a way by which we can represent complicated logical statements as a series of clauses connected by ‘and’ statements, within each clause placing a consistently ordered set of variables connected by ‘or’ statements. This simplifies the process of searching for solutions, as we can now model CNF as a multi-dimensional array, wherein each position corresponds to a variable in a clause which is represented by three values: ‘-1’, ‘0’, and ‘1’, respectively being interpreted as the ‘not’ of that variable, the variable not being present in that clause, and that variable being present normally. When we pose a solution to this system of clauses representing logical statements, we can do so simply as a vector of similar values: ‘-1’, ‘0’, and ‘1’, corresponding respectively to assigning ‘false’ to that variable, having no value necessary to be assigned to that variable, or assigning ‘true’ to that variable. Testing a solution then becomes as simple as applying this vector of values assigned to each variable to the set of clauses and checking that each clause is made true by the chosen values for each variable, that result then corresponding to the original problem statement we converted first to CNF and then to our model. This structure permits easy creation of logic problems to solve for the sake of testing algorithms and allows for the generation of problem-solutions by simply assigning values to each position in the solution vector and testing it against the set of clauses. Testing is a simple process in our model: if our solution vector contains a value that matches its corresponding variable in a given clause, the clause is considered satisfied. (With the caveat that it is not an unassigned solution value nor an unassigned variable in the clause.) This is due to the fact that CNF simplifies to a set of variables connected by ‘or’ statements, requiring only one to be satisfied for the entire clause to be satisfied.