Results 1 to 9 of 9
  1. #1
    EBamber is offline Member
    Join Date
    Apr 2014
    Posts
    30
    Rep Power
    0

    Default Trying to implement DPLL

    Java Code:
    public boolean DPLL(ArrayList<ArrayList<String>> AND)
        {  
            ArrayList<String> OPP;
            OPP= new ArrayList<>();      
            //preprocess will remove clauses which are definitely true from the CNF representation and add them to the
            //list of true clauses and literals
            //it will 
            C.preprocess();
            if(AND.isEmpty())
            {
                System.out.println("isEMPTY");
                x = Rule1(C.TRUTH);
            }
            else
            {
                for(int i =AND.size()-1;i>=0;i--)
                {
                    if(AND.get(i).contains("!x")||AND.get(i).contains("!y")||AND.get(i).contains("!z")||AND.get(i).contains("!w"))
                    {  
                        for(int j=0;j<AND.get(i).size();j++)
                        {
                            if(AND.get(i).get(j).charAt(0)=='!')
                            {
                                System.out.println("here1");
                                OPP.add(AND.get(i).get(j).substring(1));
                                System.out.println(OPP);
                                C.OPPAND.add(OPP);
                                System.out.println(C.OPPAND);
                            }
                            else
                            {
                                System.out.println("here2");
                                OPP.add('!'+AND.get(i).get(j));
                                System.out.println(OPP);
                                C.OPPAND.add(OPP);
                                System.out.println(C.OPPAND);
                            }
                        }
                    }
                    else
                    {
                        System.out.println("here3");
                        C.OPPAND.add(AND.get(i));
                        System.out.println(C.OPPAND);
                    }
                    AND.remove(i);
                    System.out.println(AND);
                }
                DPLL(AND);
            }
            return x;
        }
    Above is the full method being used written mostly iteratively.
    IsEmpty() checks if the CNF sentence I'm working with has any more clauses to work with
    Rule1 says that if the list of true items doesn't contain a negative literal, then the sentence is satisfiable
    preprocess() adds a clause to the list of true items if any one of the literals is definitely true and removes the clause from the working set "AND"

    The logic that I used is that if the working set is empty, then the answer to the satisfiability problem depends on whether or not there are negative literals in the TRUTH list, otherwise it's going to iterate through the working set and add the clauses which will make the sentence satisfiable to the Operation of AND list OPPAND (with OPP being a buffer)
    If any one of the literals in a clause is negative "!x", then that clause is processed as whatever literals are negative are added to OPPAND as a positive clause, the positive literals are added as negative clauses (De Morgan's Law)

    If none of the literals in a clause are negative, then the clause is added as is to OPPAND, the clause processed is then removed from AND to empty it out recursively

    I tested it out with the clauses (x)(!x)
    which should return the output false due to the fact that a literal is conjuncted with it negator, but instead I get the output

    (x)(!x)
    exit
    here1
    [x]
    [[x]]
    [[x]]
    here3
    [[x], [x]]
    []
    isEMPTY
    true

    This is definitely a flaw in my logic, can anybody help me find where that flaw is?
    1. Are my rules defined well?
    2. Am I right to be using the data structures I'm using?
    3. Why won't the two clauses cancel out?

  2. #2
    Norm's Avatar
    Norm is offline Moderator
    Join Date
    Jun 2008
    Location
    Eastern Florida
    Posts
    17,902
    Rep Power
    25

    Default Re: Trying to implement DPLL

    Do you have a way to compile and execute the code for testing?

    There aren't any comments in the code describing the algorithm that it is implementing. Can that be fixed?
    If you don't understand my response, don't ignore it, ask a question.

  3. #3
    EBamber is offline Member
    Join Date
    Apr 2014
    Posts
    30
    Rep Power
    0

    Default Re: Trying to implement DPLL

    I'll add some comments and re post the algorithm

  4. #4
    EBamber is offline Member
    Join Date
    Apr 2014
    Posts
    30
    Rep Power
    0

    Default Re: Trying to implement DPLL

    Java Code:
    public boolean DPLL(ArrayList<ArrayList<String>> AND)
        {  
            ArrayList<String> OPP;
            OPP= new ArrayList<>();      
            //preprocess will remove clauses which are definitely true from the CNF representation and add them to the
            //list of true clauses and literals
            C.preprocess();
            if(AND.isEmpty())
            {
                //if the List of clauses is empty it will check the truth list for rule 1
                //rule 1 states that if the list of truth is empty, then the sentence holds in CNF
                System.out.println("isEMPTY");
                x = Rule1(C.TRUTH);
            }
            else
            {
                //otherwise it will search through the sentence for the solutions to each clause 
                for(int i =AND.size()-1;i>=0;i--)
                {
                    //if any of the literals in a clause are false
                    if(AND.get(i).contains("!x")||AND.get(i).contains("!y")||AND.get(i).contains("!z")||AND.get(i).contains("!w"))
                    {  //loop through the literals
                        for(int j=0;j<AND.get(i).size();j++)
                        {
                            //negate both literals and add them as two different clauses to add the equivalent to the negative
                            //of a clause by De Morgan's laws
                            if(AND.get(i).get(j).charAt(0)=='!')
                            {
                                //if the literal is negative, make it positive
                                System.out.println("here1");
                                OPP.add(AND.get(i).get(j).substring(1));
                                System.out.println(OPP);
                                C.OPPAND.add(OPP);
                                System.out.println(C.OPPAND);
                            }
                            else
                            {
                                //if the literal is positive, make it negative
                                System.out.println("here2");
                                OPP.add('!'+AND.get(i).get(j));
                                System.out.println(OPP);
                                C.OPPAND.add(OPP);
                                System.out.println(C.OPPAND);
                            }
                        }
                    }
                    //if none of the literals in a clause are negative
                    else
                    {
                        //add the whole clause
                        System.out.println("here3");
                        C.OPPAND.add(AND.get(i));
                        System.out.println(C.OPPAND);
                    }
                    //remove the processed clause from the list of clauses and run through the next iteration
                    AND.remove(i);
                    System.out.println(AND);
                }
                //call the method again to run the case where the list is empty
                DPLL(AND);
            }
            return x;
        }
    I think the problems are that:
    1. I'm checking the truth list without adding or processing any of the data in it (in this method)
    2. There's a logical error in the part where I process false clauses

  5. #5
    Norm's Avatar
    Norm is offline Moderator
    Join Date
    Jun 2008
    Location
    Eastern Florida
    Posts
    17,902
    Rep Power
    25

    Default Re: Trying to implement DPLL

    How can the code be compiled and executed for testing?
    If you don't understand my response, don't ignore it, ask a question.

  6. #6
    EBamber is offline Member
    Join Date
    Apr 2014
    Posts
    30
    Rep Power
    0

    Default Re: Trying to implement DPLL

    Java Code:
    package dpll;
    import java.util.Scanner;
    import java.lang.String;
    import java.util.Arrays;
    import java.util.List;
    import java.util.ArrayList;
    
    
    public class main 
    {
        public static void main(String[] args) 
        {
            //input and CNF representation
            Scanner sc = new Scanner(System.in);
            sc.useDelimiter("\n");
            String x,y;
            String[] z,w;
            CNF C = new CNF();
            System.out.println("Type in a CNF input. 'exit' to close");
            do
            {
                //the first step is to remove blank spaces and turn the clauses into a form
                //which can be represented in java as ArrayList elements
                x  = sc.next();
                y = x.replaceAll(" ", "");
                y = y.replace("(","");
                y = y.replace(".","");
                y = y.replace(")"," ");
                z = y.split(" ");
                //all of the clauses are put into different elements of array z by a split function
                if(!y.toLowerCase().equals("exit"))
                {
                   if("=true".equals(y.substring(1, y.length()))){C.TRUTH.add(y.substring(0, 1));}
                   else if("=false".equals(y.substring(1, y.length()))){C.TRUTH.add("!"+y.substring(0, 1));}
                   else
                    {
                        for (String z1 : z) 
                        {
                        //literals in each clause are then split by the commas that seperate them
                        //they are then added to an ArrayList of literals joined by an OR function
                        //finally they are added to an ArrayList of clauses joined by an AND function 
                            w = z1.split(",");
                            C.OR = new ArrayList(Arrays.asList(w));
                            C.addAND(C.OR);
                        }
                    }
                }
            }
            while(!(y.toLowerCase().equals("exit")));
            DPLL D = new DPLL();
            C.process(C.TRUTH);
            System.out.println(D.DPLL(C.AND));               
        }     
    }
    Java Code:
    package dpll;
    import java.util.ArrayList;
    
    public class CNF 
    {
        ArrayList<String> OR;
        ArrayList<ArrayList<String>> AND;
        ArrayList<ArrayList<String>> OPPAND;
        ArrayList<String> TRUTH;
        
        public CNF()
        {
            this.AND = new ArrayList<>();
            this.TRUTH = new ArrayList<>();
            this.OPPAND = new ArrayList<>();
        }
        
        public void addAND(ArrayList<String> or)
        {
            AND.add(or);
        }
        
        public void newOR()
        {
            this.OR = new ArrayList<>();
        }
        
        public ArrayList<String> getOR()
        {
            return this.OR;
        }
        
        public void process(ArrayList<String> X)
        {
            for(int i = X.size()-1;i>=0;i--)
            {
                if(X.get(i).charAt(0)!='!')
                {
                    X.remove(i);
                }
            }
        }
        
        public void preprocess()
        {   
            boolean y = false;
            //search for all clauses in the list which contain a value in TRUTH
            for(int i=AND.size()-1;i>=0;i--)
            {
                for(int j=AND.get(i).size()-1;j>=0;j--)
                {
                    if(TRUTH.contains(AND.get(i).get(j)))
                    {
                        y=true;
                        String x="";
                        for(String s: AND.get(i))
                        {
                            x+= s+",";
                        }
                        TRUTH.add(x);
                        j=0;
                    }     
                }
                if(y==true)
                {
                    AND.remove(i);
                }
            }
            
        }
    
    }
    Java Code:
    package dpll;
    import java.util.ArrayList;
    
    public class DPLL 
    {
        boolean y =false;
        boolean x =false;
        CNF C = new CNF();
        public boolean Rule1(ArrayList<String> TRUTH)
        {
            y= TRUTH.isEmpty();
            return y;
        }
        
        public boolean DPLL(ArrayList<ArrayList<String>> AND)
        {  
            ArrayList<String> OPP;
            OPP= new ArrayList<>();      
            //preprocess will remove clauses which are definitely true from the CNF representation and add them to the
            //list of true clauses and literals
            C.preprocess();
            if(AND.isEmpty())
            {
                //if the List of clauses is empty it will check the truth list for rule 1
                //rule 1 states that if the list of truth is empty, then the sentence holds in CNF
                System.out.println("isEMPTY");
                x = Rule1(C.TRUTH);
            }
            else
            {
                //otherwise it will search through the sentence for the solutions to each clause 
                for(int i =AND.size()-1;i>=0;i--)
                {
                    //if any of the literals in a clause are false
                    if(AND.get(i).contains("!x")||AND.get(i).contains("!y")||AND.get(i).contains("!z")||AND.get(i).contains("!w"))
                    {  //loop through the literals
                        for(int j=0;j<AND.get(i).size();j++)
                        {
                            //negate both literals and add them as two different clauses to add the equivalent to the negative
                            //of a clause by De Morgan's laws
                            if(AND.get(i).get(j).charAt(0)=='!')
                            {
                                //if the literal is negative, make it positive
                                System.out.println("here1");
                                OPP.add(AND.get(i).get(j).substring(1));
                                System.out.println(OPP);
                                C.OPPAND.add(OPP);
                                System.out.println(C.OPPAND);
                            }
                            else
                            {
                                //if the literal is positive, make it negative
                                System.out.println("here2");
                                OPP.add('!'+AND.get(i).get(j));
                                System.out.println(OPP);
                                C.OPPAND.add(OPP);
                                System.out.println(C.OPPAND);
                            }
                        }
                    }
                    //if none of the literals in a clause are negative
                    else
                    {
                        //add the whole clause
                        System.out.println("here3");
                        C.OPPAND.add(AND.get(i));
                        System.out.println(C.OPPAND);
                    }
                    //remove the processed clause from the list of clauses and run through the next iteration
                    AND.remove(i);
                    System.out.println(AND);
                }
                //call the method again to run the case where the list is empty
                DPLL(AND);
            }
            return x;
        }
    }
    Here's all the source code if that's what you meant by your question

    All of the println's were written with the purpose of testing the data flow of the program

  7. #7
    Norm's Avatar
    Norm is offline Moderator
    Join Date
    Jun 2008
    Location
    Eastern Florida
    Posts
    17,902
    Rep Power
    25

    Default Re: Trying to implement DPLL

    The testing program needs input. Can you change the Scanner class's constructor to provide testing input in a String?
    Java Code:
            Scanner sc = new Scanner("PUT THE INPUT HERE");
    Where in the printout does it show the code going wrong?
    Last edited by Norm; 05-07-2014 at 06:09 PM.
    If you don't understand my response, don't ignore it, ask a question.

  8. #8
    EBamber is offline Member
    Join Date
    Apr 2014
    Posts
    30
    Rep Power
    0

    Default Re: Trying to implement DPLL

    This might sound like a stupid question but what do you mean by:
    The testing program needs input. Can you change the Scanner class's constructor to provide testing input in a String?
    Java Code:
    1
    Scanner sc = new Scanner("PUT THE INPUT HERE");
    ?

    My program is getting input and i was testing the logic visually

    As for where it all goes wrong
    (x)(!x)
    exit
    here1
    [x]
    [[x]]
    [[x]]
    here3
    [[x], [x]]
    []
    isEMPTY
    true

    The CNF input here was supposed to be equivalent to X^!X which should evaluate to false, but I got true so I'm guessing it goes wrong in rule1 due to something that happens in DPLL

  9. #9
    Norm's Avatar
    Norm is offline Moderator
    Join Date
    Jun 2008
    Location
    Eastern Florida
    Posts
    17,902
    Rep Power
    25

    Default Re: Trying to implement DPLL

    The Scanner class's constructor can take a String that will be used by the methods of the class. By defining the program's input there (instead of having to type it in for every test) the testing will be easier and the input to the program will be the same for everyone that is testing this problem.
    For example[code]
    Scanner sc = new Scanner("(x)(!x)\nexit\n");[\code]

    Try doing more debugging by adding println statements to all the methods that print out the values of the variables that they are working with so you can see what the computer sees when the code is executed. For example what is in the arraylist ADD at all the methods and places it is used?
    If you don't understand my response, don't ignore it, ask a question.

Similar Threads

  1. How to implement a LispList?
    By fultonwilcox in forum New To Java
    Replies: 0
    Last Post: 09-14-2012, 06:02 AM
  2. Best way to implement an ActionListener.
    By VisionIncision in forum New To Java
    Replies: 4
    Last Post: 12-07-2010, 01:52 AM
  3. Implement a timeout
    By pjmorce in forum Advanced Java
    Replies: 5
    Last Post: 04-27-2010, 03:36 AM
  4. Best way to implement a timer
    By Nuluvius in forum New To Java
    Replies: 11
    Last Post: 01-16-2009, 02:27 AM

Tags for this Thread

Posting Permissions

  • You may not post new threads
  • You may not post replies
  • You may not post attachments
  • You may not edit your posts
  •