Thread: C Satisfiability Solver

First off, don't over think this. Go for a brute force approach first. Once you get it working then tweak it to get rid of unnecessary tests.

The only think I can see that needs recursion is generating a list of permutations of the inputs to test. You need to assume you'll go through all the input permutations, but if you realize that you've found one of your OR clauses is false then you might be able to apply some smarts and skip checking any of the input combinations which aren't used by that OR clause, since it won't change the output.

For example, if you have 5 inputs, (x1 .. x5) and one of the sub-expressions is

(x1 OR x2 or x3)

Once you have x1=x2=x3=x4=x5=0, you know this term is 0. There's no need to check any of the x4=1 or x5=1 cases since you know that won't change the value of the term (obviously, since x4 and x5 aren't used there). This will prune your search tree / recursive calls a bit. Likewise, once you get to checking x1=1, x2..x5=0 you'll see the sub expression is true. No point in checking any other terms with x1=1, since the sub-expression will continue to be true no matter what x2..x5 are set to.

As for how to implement this, you'll have an array set up from your inputs : int [N][3], where N is the number of sub-expressions. Each entry will be the value entered by the user. You'll have an array value[N] that holds the current value of x1..xN you're testing. You'll have a 2x nested loop which substitutes each of the inputs in the appropriate places in the sub-expressions, keeping track of the value that generates. Something like

Code:

unsigned result = 1;
For each subexpression s 
  unsigned term = 0;
  for each term T
    unsigned variable = value[abs(input[S][T])];
    negate variable if input[S][T] < 0;
    term = term | variable;
  end for
  result = result & term
end for
if result == 1
  print value array since it satisfies the expression

You can bail out early if any subexpression == 0 since that will mean the whole expression is 0.

For the recursive part, you'll need to keep track of which of the values array you just tested, and then flip it before the next call.

Code:

assume values is initialized to all 0s
void recursive (int values[], int length, int last_changed)
{
   test with current values[] array
   if (last_changed == length)
      return; /* you've tested everything */
   flip values[last_changed]
   recursive(values, length, last_changed+1);
   flip values[last_change] back to original value
}

ETA- you'll want to go though the values array backwards to hit the "in order printing" condition from the assignment even though this example works though them in the other direction. Same idea, should be trivial to switch.

If you add some smarts to get rid of redundant checks, you'll do it by being smarter about which values you flip and how you update last_changed to match. For example, if values[0] is such that you don't have to check the rest of values[1..length-1], you'll skip the last 3 steps in the function to avoid the unneeded testing of values[1..length-1].

There are two problems with my pseudo-code. First off, add the red line. Second move the test code into the if() block.

Code:

assume values is initialized to all 0s, as is last_changed.  length is the number of entries in value
void recursive (int values[], int length, int last_changed)
{
   
   if (last_changed == length)
   {
      /* you've now generated all input values, so use them to test the equations */
      test with current values[] array
      return; 
   }
   recursive(values, length, last_changed+1); /* A */
   flip values[last_changed]
   recursive(values, length, last_changed+1);  /* B */
   flip values[last_change] back to original value
}

length is the length of the values[] array - it's the count of how many inputs there are, not a count of the number of permutations
last_changed is the index in values[] you last flipped - this is also an index into the values array and not a count of the number of permutations tested - it indicates which level of recursion you're at, which is also the same as the bit you're currently changing to generate all permutations deeper in the search tree.

Each level of the recursive call sets a given index in value to 0, tests all the permutations of the higher indexes, then changes that given value to 1 and again tests all of the permutations at higher indexes

So the first call to recursive will set values[0] == 0 at comment A - this will then test all cases where values[0] == 0 and values[1..length-1] == both 0 and 1. The second recursive call at B will test all cases where value[0] == 1 and values[1..length-1] == both 0 and 1.

Think about it at the last level of recursion - last_changed will be the last index in values. All the others will have been set to something by previous calls. So the first call at A will make sure the last bit is 0 and call recursive. This final call will enter the if-block, test the equation, and then return. You'll then flip the last bit, call the code at B, and do the same test with that LSB at 1.

You'll return from that level, and move on to flip length-2 (the second to last bit). The call at B will then call recursion and go through the same steps, only with the second to last bit being the opposite value this time.

And then the code will return up one more level, flip the third most significant bit, and repeat the whole process again. And so on, until all bits have been tested.

You can ignore my edit - using the code as-is will generate the values in-order.

As for pruning the search tree, it's going to be a bit more difficult than I thought. You might want to experiment with using a 3rd value in values to indicate a don't care / uninitialized state. When you see this value in your code, test the equation with that value at both 0 and 1 (*) (you'll need to add this as an extra test at the start of the recursive function(), otherwise you'll only be checking when all values have been assigned a value so there's no children to prune from the search tress). If you get the same result for either input value, the uninitialized value doesn't matter in the final result. This means that you don't have to do the flip-and-check code for that bit, since you know that it doesn't change the result. You'll still have to track it, though, and you'll have to modify your print function to print both 0 and 1 as valid for these uninitialized values, though. In the end I think this is more than is expected for an assignment where you're just learning how to use recursion, but it might be fun to play with

* Or you could be smarter with your logic and instead of using the builtin & and | operators, code up your own & and | functions which handle an X state. I.e, an OR function would be :

Code:

In12 Out
0 0 = 0
0 1 = 1
0 X = X
1 0 = 1
1 1 = 1
1 X = 1

This makes it very similar to a normal OR function - at least one value must be 1 for the output to be 1 - but it adds the case where one input is 0 and the other is unknown to be equal to the unknown variable.

i am stucked at the very beginning...

The x1 .. xN values are being flipped (inverted, whatever you want to call it). Look at the truth table in post 5 and see how as you work down the list you're flipping one bit compared to the previous line - this comes from the first flip in the pseudo-code. Sometimes you're first "unflipping" a series of less significant bits (e.g when going from 011 to 100) - this corresponds to the second flip in the pseudo-code I listed (inverting a bit twice returns it to its original value).

variable is the (optionally inverted) value of a single variable in your input expression. term is a running total of what you get as you OR those variables together in each (xN or xM or ...) subexpression. Likewise, result is the running total as you AND each of those subexpressions together to get a final value of the whole expression.

And hopefully my pseudo-code is vague enough that there will be some understanding and innovation required to actually code it up - which means that I'm not getting in the way of the goal of the assignment which should be to 1 - understand the problem and 2 - come up with and code a solution to it. That's why I'm using lots of words and vague pseudo-code (possibly with bugs?) as an example.