I know there are commonly used boolean satisfiability problem-solving methods (such as DPLL etc.). As far as I know, such methods mostly depend on converting boolean expression into the CNF or DNF form. However, I’m trying to solve the given expressions “as-is”, without conversion to other forms. So, for boolean expression, I’m building a tree, consisting of many logical gates (AND, OR, NOT, XOR, VAR, CONST) and trying to propagate the right values by applying boolean laws.
step 1 – Common boolean laws
In such an approach there are some trivial steps like if AND has a value of 1 then the inputs must be both 1 and 1, or if XOR has a value of 1, and one input is 0, then the second input must be 1, etc. This step I call “propagation of values”, and it is performed until there are no values to resolve.
step 2 – Resolution by conflict
The second step is to assign value to the random gate, without a value assigned/resolved yet, name it X temporarily, then do “propagation of values”, and observe if in the expression tree some conflicts occurred. By conflict, I mean illegal state of the gate like AND(1,1)->0. So if the conflict occurred, this tells us that value assigned to the X gate is illegal, so I can assign the opposite value, and get back to the first step. This step I call “resolution by conflict”.
step 3 – Resolution by commons
The third step is to assign a value of 0 to the random gate, without a value assigned/resolved yet. Perform “propagation of values”, collect results (the assigned values of gates from the tree), in other words, do a “snapshot” of the tree after assignment. Then back to the original state before this step, assign a value of 1 to the same gate, perform propagation of values, then collect the second “snapshot”, then back to the original state again. Now, if the snapshots are both conflict-free, we could look at values that are both the same in the first and the second snapshot. These values are independent of the initial gate assignment and valid, so we can safely assign them to their gates. This step I call “resolution by commons”.
These steps were tested by me (program in C++) and worked pretty well.
So, the question is, what other kinds of steps can apply for this kind of resolution / BSAT solving? I’m asking because there are still some problems that with these steps I can’t go further (algorithm with these steps “see” that is nothing to do more).
If something is unclear, please let me know in the comments. Also if such an approach is known I’ll be thankful for references or links to resources about the topic.