Free cookie consent management tool by TermsFeed Policy Generator

source: branches/OKBJavaConnector/ECJClient/src/ec/app/sat/SAT.java @ 6152

Last change on this file since 6152 was 6152, checked in by bfarka, 13 years ago

added ecj and custom statistics to communicate with the okb services #1441

File size: 3.7 KB
Line 
1package ec.app.sat;
2
3import ec.*;
4import ec.simple.*;
5import ec.vector.*;
6import ec.util.*;
7import java.io.*;
8import java.util.*;
9
10/**
11   SAT implements the boolean satisfiability problem.
12 
13   <p><b>Parameters</b><br>
14   <table>
15   <tr><td valign=top><i>base</i>.<tt>sat-filename</tt><br>
16   <font size=-1>String</td>
17   <td valign=top>(Filename containing boolean satisfiability formula in Dimacs CNF format)</td></tr>
18   </table>
19 
20   @author Keith Sullivan
21   @version 1.0
22*/
23
24public class SAT extends Problem implements SimpleProblemForm
25    {
26       
27    public static final String P_FILENAME = "sat-filename";
28       
29    Clause formula[];
30       
31    public void setup(EvolutionState state, Parameter base)
32        {
33        super.setup(state, base);
34        String fileName = state.parameters.getString(base.push(P_FILENAME), null);
35               
36        try
37            {
38            BufferedReader inFile = new BufferedReader(new FileReader(new File(fileName)));
39            String line="";
40            int cnt=0;
41            boolean start = false;
42            while ((line = inFile.readLine()) != null)
43                {
44                if (start)
45                    {
46                    formula[cnt++] = new Clause(line);
47                    continue;
48                    }
49                               
50                if (line.startsWith("p"))
51                    {
52                    start = true;
53                    line.trim();
54                    int index = line.lastIndexOf(" ");
55                    formula = new Clause[Integer.parseInt(line.substring(index+1))];
56                    }
57                }
58            inFile.close();
59            }
60        catch (IOException e)
61            {
62            state.output.fatal("Error in SAT setup, while loading from file " + fileName +
63                "\nFrom parameter " + base.push(P_FILENAME) + "\nError:\n" + e); 
64            }
65        }
66       
67    /**
68        Evalutes the individual using the MAXSAT fitness function.
69    */
70    public void evaluate(final EvolutionState state, final Individual ind, final int subpopulation, final int threadnum)
71        {
72        BitVectorIndividual ind2 = (BitVectorIndividual) ind;
73        double fitness=0;
74               
75        for (int i=0; i < formula.length; i++)                 
76            fitness += formula[i].eval(ind2);
77               
78        ((SimpleFitness)(ind2.fitness)).setFitness( state, (float) fitness, false);
79        ind2.evaluated = true;
80        }
81       
82       
83    /**
84       Private helper class holding a single clause in the boolean formula. Each clause
85       is a disjunction of boolean variables (or their negation).
86    */
87    public class Clause
88        {
89               
90        int[] variables;
91        public Clause(String c)
92            {
93            StringTokenizer st = new StringTokenizer(c);
94            variables = new int[st.countTokens()-1];
95            for (int i=0; i < variables.length; i++)
96                {
97                variables[i] = Integer.parseInt(st.nextToken());
98                }
99            }
100               
101        /**
102            Evaluates the individual with the clause.  Returns 1 is clase is satisfiabile, 0 otherwise.
103        */
104        public int eval(BitVectorIndividual ind)
105            {
106            boolean tmp;
107            int x;
108            for (int i=0; i < variables.length; i++)
109                {                             
110                x = variables[i];
111                if (x < 0)
112                    tmp = !ind.genome[-x-1];
113                else
114                    tmp =  ind.genome[x-1];
115                               
116                if (tmp) return 1;
117                }
118            return 0;
119            }
120        };     
121    }
Note: See TracBrowser for help on using the repository browser.