Like Tree3Likes
  • 2 Post By KCfromNC
  • 1 Post By Coldev

C Satisfiability Solver

This is a discussion on C Satisfiability Solver within the C Programming forums, part of the General Programming Boards category; Hi everyone I have this project for my programming class and would appreciate it if someone could point me in ...

  1. #1
    Registered User
    Join Date
    Nov 2011
    Posts
    4

    C Satisfiability Solver

    Hi everyone I have this project for my programming class and would appreciate it if someone could point me in the right direction. The objective of the lab is to write a C program that will be able to solve a boolean formula and print all the satisfying assignments. This is also known as boolean satisfiability. So basically if we are given the boolean formula


    f = (x1 OR 'x2 OR x3) AND ('x1 OR x2 OR x3)


    this means we need to find all the assignments for the variables that make this formula true. When there is a ' before the variable that means it is in the complemented form, so a False assignment would make it evaluate to true.


    So for the above formula these would be the satisfying assignnments:


    x1x2x3
    -----
    F F F
    F F T
    F T T
    T F T
    T T F
    T T T


    So there are 2^n possiblities that need to be evaluated where n is the number of variables. Each clause (what's inside the brackets) will have exactly 3 variables and they will be provided by input from the user. The number of clauses and variables will be provided when the program is run. So for example, the user might run the program and say there 4 variables and 5 clauses, then they would input the following formula:


    1 -2 3
    3 -4 2
    3 1 2
    4 -2 1
    3 -1 2


    where each number represents a variable and if it's negative then it's in complemented form.


    The formula for the first sample would be:
    1 -2 3
    -1 2 3


    --
    Each clause will have exactly three literals (variables) and no repeated variables. Also, the satisfying assignments need to be printed in an order where they first start with one where x1 is false are printed before x1 being true, and for those where x1 is false, all those with x2 being false are printed first and so on.


    We must use recursion to create this program.
    ----
    Okay, so first of all I'm not looking for anyone to give me any code, I'm just looking for some help and pointers in the right direction. Here's what I've done so far:


    I've coded a way for the user to input the formula variables which are stored into a c X 3 matrix where c is the number of clauses, so if there input would be stored like this:


    3 2 1
    -2 3 1


    just like a regular table.


    Now I've thought about this problem can be satisfied recursively and here's what I came up with:

    Name:  H9gFE.jpg
Views: 647
Size:  11.7 KB


    So I suppose the algorithm should have two parts, one where it keeps checking the right side (= 0) first then going left. This will satisfy the requirement of printing all the assignments in the correct order. But here is where I'm stuck, first of all:


    1. What would be the condition for the function to stop recursing or repeating


    2. Let's say it keeps recursing and somehow I'm at x1 is FALSE, x2 is FALSE, x3 is FALSE, and x4 is FALSE, how do I substitute those assignments into all the clauses I have in my formula and make sure it satisfies them all? I mean nothing is arranged in any certain order so I am really lost here on how I would replace them and then make sure they all evaluate to true when assigning everything to false.


    3. I realize that having more variables doesn't matter since the function would be the same if you had just one variable which would give you two branches or 30 variables. Because each branch just repeats, so if I just have x1, then first it will check if setting x1 to false evaluates to true, if not it will set it to true and see if that satisfies it. So even if there are many branches/variables it's just the same thing happening over and over again.


    I spent an entire day trying to come up with a solution and reading tons of articles on satisfiability algorithms and the DLPP algorithm but this is a first year course so thesis papers on the subject didn't help me very much.


    Any help you can give me is appericiated..and wow that is one long post. :0

  2. #2
    Registered User
    Join Date
    Sep 2006
    Posts
    8,868
    Welcome to the forum, Coldev!

    I have to say, this is THE best first post I have seen in a long while! Couldn't help but bump your thread.

    No, I can't help you, atm, but others no doubt will assist.

  3. #3
    Registered User
    Join Date
    Mar 2009
    Posts
    344
    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].
    Last edited by KCfromNC; 11-07-2011 at 08:13 AM.
    MK27 and Coldev like this.

  4. #4
    Registered User
    Join Date
    Nov 2011
    Posts
    4
    Thank you so much for your response. I'm overloaded with other work for the next 2 days but after that I will read your post very carefully while trying to come up with some code. The lab is due on the 19th of the month so hopefully I can get it done by then with the help of you awesome people.

  5. #5
    Registered User
    Join Date
    Nov 2011
    Posts
    4
    Hi KC, thanks again for your help, I've worked on the first part of the program which will test the values array against all the sub expressions, now I'm stuck on the second part.

    There are some things I don't understand about the second piece of code your wrote. Assuming we have a single clause and 3 variables, like this:

    1 2 3

    The permutations that should be generated are:
    0 0 0
    0 0 1
    0 1 0
    0 1 1
    1 0 0
    1 0 1
    1 1 0
    1 1 1

    "
    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 // okay, so you're saying that we have values = [0, 0, 0]; correct?
    void recursive (int values[], int length, int last_changed) //what are length and last changed? I assumed that length would be either how many possible permutations there could be (in this case 8) or how many variables there are (3)... as for last_changed, would we pass that as 0 the first time we use the function?
    {
       test with current values[] array //understood
       if (last_changed == length) //so is last_changed a counter of how many possible solutions we've tested? so once we've tried all the solutions we stop, but that would mean length would be need to set to 8 or 2^n (n = num of variables), correct?
          return; /* you've tested everything */
       flip values[last_changed] //really did not understand this, what are we flipping here exactly? if last_changed is 0, then do you mean we need to flip values[0] and make it opposite? but that doesn't make sense since last_changed will go up to 8, and values[8] doesn't exist
       recursive(values, length, last_changed+1); 
       flip values[last_change] back to original value //is last_change different than last_changed? why are we changing it back to original value if there is no more testing going on?
    }
    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."




    I really tried understanding that second piece of code and writing the function but I'm still pretty confused at this point.

  6. #6
    Registered User
    Join Date
    Mar 2009
    Posts
    344
    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.
    Last edited by KCfromNC; 11-11-2011 at 08:19 AM.

  7. #7
    Registered User
    Join Date
    Nov 2011
    Posts
    1
    i am stucked at the very beginning...
    Last edited by nprocex; 11-11-2011 at 07:48 PM.

  8. #8
    Registered User
    Join Date
    Nov 2011
    Posts
    4
    Finished! Thanks again for your help, I would never have been able to finish it without you. Also, I tested with up to 20 variables and 90 clauses and it prints all the solutions instantly, and I don't think the tester program will use more than that, so pruning the search tree was not necessary :-)

    Thanks again!
    KCfromNC likes this.

  9. #9
    Registered User
    Join Date
    Nov 2011
    Posts
    2
    By some stroke of luck I happened across this forum. I'm working on the same lab, and I was wondering if someone could clear something up regarding some of the terminology. Above it's mentioned that one should "flip values[last_changed]". What exactly is being flipped? Also, regarding this section:

    foreach term T
    unsigned variable = value[abs(input[S][T])];
    negate variable if input[S][T] < 0;
    term = term | variable;

    It seems that S represents each clause, but what is T? Also, what is the variable as distinct from 'term'?
    My understanding of the situations is somewhat clouded at the moment...

  10. #10
    Registered User
    Join Date
    Nov 2011
    Posts
    1
    I have worked on this problem myself before I came to know such a thread...

    Won't the anticheat catch you guys?? lul trololol :|

  11. #11
    Registered User
    Join Date
    Mar 2009
    Posts
    344
    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.
    Last edited by KCfromNC; 11-17-2011 at 07:39 AM.

  12. #12
    Registered User
    Join Date
    Nov 2011
    Posts
    2
    Quote Originally Posted by KCfromNC View Post

    And hopefully my pseudo-code is vague enough that there will be some understanding and innovation required to actually code it up -
    I think you're right, it's enough to plant ideas and give some sense of direction, which a lot of people working on this lab require. This lab is a massive leap from anything else we've done, and to make matters worst there is minimal instruction as to how to solve the problem. So I think it's far from cheating.

    Thanks for all your assistance. I anticipate a couple long nights ahead of me... but this thread should help.

Popular pages Recent additions subscribe to a feed

Similar Threads

  1. Sudoku solver...
    By matsp in forum C++ Programming
    Replies: 24
    Last Post: 02-14-2011, 07:30 PM
  2. Sudoku solver
    By M-S-H in forum C Programming
    Replies: 10
    Last Post: 12-15-2009, 02:26 PM
  3. sudoku solver
    By manav in forum Game Programming
    Replies: 11
    Last Post: 02-03-2008, 09:38 PM
  4. Target Solver
    By P4R4N01D in forum C Programming
    Replies: 4
    Last Post: 01-14-2008, 04:49 PM
  5. Scrabble Solver
    By Coder87C in forum C++ Programming
    Replies: 3
    Last Post: 08-11-2005, 03:36 PM

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21