Added specific launcher for KTH experiments.

Need some polish from Anne to make sure the current mapping to options
makes sense. Encapsulated some fields of PBSolverCP to make them more
easily configurable.

build.xml

@@ -179,6 +179,30 @@
                 </antcall>
 	</target>
 
+	<target name="kth" depends="core,pseudo,maxsat" description="Build a jar file suitable for KTH">
+		<echo>Building the Java SAT Solvers toolkit for KTH experiments</echo>
+                <antcall target="build">
+		   <param name="package" value="sat"/>
+		   <param name="src" value="org.sat4j.sat/src/main/java" />
+                   <param name="jarname" value="org.sat4j.sat"/>
+		</antcall>
+                <echo>Create All-In-One auto-executable package</echo>
+                <jar destfile="${dist}/${release}/sat4j-kth.jar" basedir="${build}">		 
+                   <manifest>
+                       <attribute name="Main-Class" value="org.sat4j.sat.KTHLauncher"/>
+                   </manifest>
+		   <zipgroupfileset dir="${dist}/${release}">
+                           <include name="org.sat4j.core.jar"/>
+                           <include name="org.sat4j.pb.jar"/>
+			   <include name="org.sat4j.sat.jar"/>
+		   </zipgroupfileset>
+                   <zipgroupfileset dir="${lib}">
+                           <include name="commons-cli.jar"/>
+                           <include name="commons-logging.jar"/>
+		   </zipgroupfileset>
+               </jar>
+	</target>
+
 	<target name="remote" depends="core,pseudo,maxsat" description="Build a jar file suitable for build the incredible sat4j remote control">
 		<echo>Building the Java SAT Solvers toolkit</echo>
                 <antcall target="build">

org.sat4j.pb/src/main/java/org/sat4j/pb/SolverFactory.java

@@ -728,7 +728,7 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
      * 
      * @return the best available cutting planes based solver of the library.
      */
-    public static IPBSolver newCuttingPlanes() {
+    public static PBSolverCP newCuttingPlanes() {
         return newCompetPBCPMixedConstraintsObjective();
     }
 
@@ -762,13 +762,13 @@ public final class SolverFactory extends ASolverFactory<IPBSolver> {
                 new VarOrderHeapObjective(), true, false);
     }
 
-    public static IPBSolver newCuttingPlanesStarClauseLearning() {
+    public static PBSolverCP newCuttingPlanesStarClauseLearning() {
         return newPBCPStarClauseLearning(
                 new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective(), true, false);
     }
 
-    public static IPBSolver newCuttingPlanesStarCardLearning() {
+    public static PBSolverCP newCuttingPlanesStarCardLearning() {
         return newPBCPStarCardLearning(new PBMaxClauseCardConstrDataStructure(),
                 new VarOrderHeapObjective(), true, false);
     }

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCP.java

@@ -56,13 +56,13 @@ public class PBSolverCP extends PBSolver {
      * removing or not satisfied literals at a higher level before cutting
      * planes.
      */
-    protected boolean noRemove = true;
+    private boolean noRemove = true;
 
     /**
      * skipping as much as possible avoidable cutting planes during analysis
      * conflict
      */
-    protected boolean skipAllow = true;
+    private boolean skipAllow = true;
 
     /**
      * @param acg
@@ -226,4 +226,20 @@ public class PBSolverCP extends PBSolver {
     protected void updateNumberOfReducedLearnedConstraints(IConflict confl) {
     }
 
+    public boolean isSkipAllow() {
+        return skipAllow;
+    }
+
+    public void setSkipAllow(boolean skipAllow) {
+        this.skipAllow = skipAllow;
+    }
+
+    public boolean isNoRemove() {
+        return noRemove;
+    }
+
+    public void setNoRemove(boolean noRemove) {
+        this.noRemove = noRemove;
+    }
+
 }

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPCardLearning.java

@@ -88,7 +88,8 @@ public class PBSolverCPCardLearning extends PBSolverCPLong {
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
         return ConflictMapReduceToClause.createConflict(myconfl, level,
-                noRemove, skipAllow, PostProcessToCard.instance(), stats);
+                isNoRemove(), isSkipAllow(), PostProcessToCard.instance(),
+                stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPClauseLearning.java

@@ -93,7 +93,8 @@ public class PBSolverCPClauseLearning extends PBSolverCPLong {
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
         return ConflictMapReduceToClause.createConflict(myconfl, level,
-                noRemove, skipAllow, PostProcessToClause.instance(), stats);
+                isNoRemove(), isSkipAllow(), PostProcessToClause.instance(),
+                stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPLong.java

@@ -81,7 +81,7 @@ public class PBSolverCPLong extends PBSolverCP {
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
         return ConflictMapReduceToClause.createConflict(myconfl, level,
-                noRemove, skipAllow, stats);
+                isNoRemove(), isSkipAllow(), stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPLongDivideBy2.java

@@ -87,8 +87,8 @@ public class PBSolverCPLongDivideBy2 extends PBSolverCPLong {
 
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
-        return ConflictMap.createConflict(myconfl, level, noRemove, skipAllow,
-                PostProcessDivideBy2.instance(), stats);
+        return ConflictMap.createConflict(myconfl, level, isNoRemove(),
+                isSkipAllow(), PostProcessDivideBy2.instance(), stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPLongDivideByGCD.java

@@ -64,8 +64,8 @@ public class PBSolverCPLongDivideByGCD extends PBSolverCPLong {
 
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
-        return ConflictMap.createConflict(myconfl, level, noRemove, skipAllow,
-                PostProcessDivideBy2.instance(), stats);
+        return ConflictMap.createConflict(myconfl, level, isNoRemove(),
+                isSkipAllow(), PostProcessDivideBy2.instance(), stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPLongReduceToCard.java

@@ -88,8 +88,8 @@ public class PBSolverCPLongReduceToCard extends PBSolverCPLong {
 
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
-        return ConflictMapReduceToCard.createConflict(myconfl, level, noRemove,
-                skipAllow, stats);
+        return ConflictMapReduceToCard.createConflict(myconfl, level,
+                isNoRemove(), isSkipAllow(), stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPLongRounding.java

@@ -86,8 +86,8 @@ public class PBSolverCPLongRounding extends PBSolverCPLong {
 
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
-        return ConflictMapRounding.createConflict(myconfl, level, noRemove,
-                skipAllow, stats);
+        return ConflictMapRounding.createConflict(myconfl, level, isNoRemove(),
+                isSkipAllow(), stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPReduceByGCD.java

@@ -63,8 +63,8 @@ public class PBSolverCPReduceByGCD extends PBSolverCP {
 
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
-        return ConflictMapReduceByGCD.createConflict(myconfl, level, noRemove,
-                skipAllow, stats);
+        return ConflictMapReduceByGCD.createConflict(myconfl, level,
+                isNoRemove(), isSkipAllow(), stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCPReduceByPowersOf2.java

@@ -64,7 +64,7 @@ public class PBSolverCPReduceByPowersOf2 extends PBSolverCP {
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
         return ConflictMapReduceByPowersOf2.createConflict(myconfl, level,
-                noRemove, skipAllow, stats);
+                isNoRemove(), isSkipAllow(), stats);
     }
 
     @Override

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverClause.java

@@ -49,7 +49,7 @@ public class PBSolverClause extends PBSolverCP {
 
     @Override
     protected IConflict chooseConflict(PBConstr myconfl, int level) {
-        return ConflictMapClause.createConflict(myconfl, level, noRemove);
+        return ConflictMapClause.createConflict(myconfl, level, isNoRemove());
     }
 
     @Override

org.sat4j.sat/.classpath

@@ -17,7 +17,7 @@
 			<attribute name="maven.pomderived" value="true"/>
 		</attributes>
 	</classpathentry>
-	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6">
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.7">
 		<attributes>
 			<attribute name="maven.pomderived" value="true"/>
 		</attributes>

org.sat4j.sat/.settings/org.eclipse.jdt.core.prefs

 eclipse.preferences.version=1
 org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.6
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.7
 org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
-org.eclipse.jdt.core.compiler.compliance=1.6
+org.eclipse.jdt.core.compiler.compliance=1.7
 org.eclipse.jdt.core.compiler.debug.lineNumber=generate
 org.eclipse.jdt.core.compiler.debug.localVariable=generate
 org.eclipse.jdt.core.compiler.debug.sourceFile=generate
 org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
 org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
 org.eclipse.jdt.core.compiler.problem.forbiddenReference=warning
-org.eclipse.jdt.core.compiler.source=1.6
+org.eclipse.jdt.core.compiler.source=1.7
 org.eclipse.jdt.core.formatter.align_type_members_on_columns=false
 org.eclipse.jdt.core.formatter.alignment_for_arguments_in_allocation_expression=16
 org.eclipse.jdt.core.formatter.alignment_for_arguments_in_annotation=0

org.sat4j.sat/src/main/java/org/sat4j/sat/KTHLauncher.java

+package org.sat4j.sat;
+
+import java.io.BufferedReader;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.net.URL;
+
+import org.apache.commons.cli.CommandLine;
+import org.apache.commons.cli.CommandLineParser;
+import org.apache.commons.cli.HelpFormatter;
+import org.apache.commons.cli.Option;
+import org.apache.commons.cli.Options;
+import org.apache.commons.cli.ParseException;
+import org.apache.commons.cli.PosixParser;
+import org.sat4j.pb.IPBSolver;
+import org.sat4j.pb.OptToPBSATAdapter;
+import org.sat4j.pb.PBSolverHandle;
+import org.sat4j.pb.PseudoOptDecorator;
+import org.sat4j.pb.SolverFactory;
+import org.sat4j.pb.core.PBSolverCP;
+import org.sat4j.pb.reader.OPBReader2012;
+import org.sat4j.reader.ParseFormatException;
+import org.sat4j.specs.ContradictionException;
+import org.sat4j.specs.TimeoutException;
+
+/**
+ * A specific launcher for experimenting various settings in the PB solvers with
+ * Jakob Nordstrom's group @ KTH.
+ * 
+ * @author leberre
+ * @since 2.3.6
+ */
+public class KTHLauncher {
+
+    public static Options createCLIOptions() {
+        Options options = new Options();
+        options.addOption("cl", "coeflim", true,
+                "coefficient limit triggering division");
+        options.addOption("cls", "coeflim-small", true,
+                "coefficient limit for divided constraints");
+        options.addOption("fb", "find-best-divisor-when-dividing-for-overflow",
+                true, "rounding coefficient. Legal values are true or false.");
+        options.addOption("wr", "when-resolve", true,
+                "behavior when performing conflict analysis. Legal values are skip or always.");
+        options.addOption("rr", "round-reason", true,
+                "Rounding strategy during conflict analysis. Legal values are divide-v1, divide-unless-equal, divide-unless-divisor, round-to-gcd, or never.");
+        options.addOption("rwp", "rounding-weaken-priority", true,
+                "Which literals are removed to ensure conflicting constraints. Legal values are any, satisfied, unassigned");
+        options.addOption("tlc", "type-of-learned-constraint", true,
+                "Type of constraints learned. Legal values are general-linear, cardinality, clause");
+        options.addOption("wni", "weaken-nonimplied", true,
+                "Remove literals that are not implied/propagated by the assignment at the backjump level. Legal values are true or false.");
+        Option op = options.getOption("coeflim");
+        op.setArgName("limit");
+        op = options.getOption("coeflim-small");
+        op.setArgName("limit");
+        op = options.getOption("when-resolve");
+        op.setArgName("strategy");
+        op = options.getOption("find-best-divisor-when-dividing-for-overflow");
+        op.setArgName("boolean");
+        op = options.getOption("round-reason");
+        op.setArgName("strategy");
+        op = options.getOption("rounding-weaken-priority");
+        op.setArgName("strategy");
+        op = options.getOption("type-of-learned-constraint");
+        op.setArgName("type");
+        op = options.getOption("weaken-nonimplied");
+        op.setArgName("boolean");
+        return options;
+    }
+
+    public static void log(String str) {
+        System.out.println("c " + str);
+    }
+
+    public static void main(String[] args) {
+        log("SAT4J PB solver for KTH experiments");
+        URL url = KTHLauncher.class.getResource("/sat4j.version");
+        if (url != null) {
+            BufferedReader in = null;
+            try {
+                in = new BufferedReader(
+                        new InputStreamReader(url.openStream()));
+                log("version " + in.readLine()); //$NON-NLS-1$
+            } catch (IOException e) {
+                log("c ERROR: " + e.getMessage());
+            } finally {
+                if (in != null) {
+                    try {
+                        in.close();
+                    } catch (IOException e) {
+                        log("c ERROR: " + e.getMessage());
+                    }
+                }
+            }
+        }
+        CommandLineParser parser = new PosixParser();
+        Options options = createCLIOptions();
+        if (args.length==0) {
+            HelpFormatter formatter = new HelpFormatter();
+            formatter.printHelp( "KTHLauncher", options );
+            return;
+        }
+        try {
+            CommandLine line = parser.parse(options, args);
+            PBSolverCP solver = SolverFactory.newCuttingPlanes();
+            solver.setNoRemove(true);
+            solver.setSkipAllow(false);
+            if (line.hasOption("type-of-learned-constraint")) {
+                String value = line
+                        .getOptionValue("type-of-learned-constraint");
+                switch (value) {
+                case "general-linear": // default case, do nothing
+                    break;
+                case "cardinality":
+                    solver = SolverFactory.newCuttingPlanesStarCardLearning();
+                    break;
+                case "clause":
+                    solver = SolverFactory.newCuttingPlanesStarClauseLearning();
+                    break;
+                default:
+                    log(value
+                            + " is not a supported value for option type-of-learned-constraint");
+                    return;
+                }
+            }
+            if (line.hasOption("when-resolve")) {
+                String value = line.getOptionValue("when-resolve");
+                switch (value) {
+                case "always": 
+                    solver.setSkipAllow(false);
+                    break;
+                case "skip":
+                    solver.setSkipAllow(true);
+                    break;
+                default:
+                    log(value
+                            + " is not a supported value for option when-resolve");
+                    return;
+                }
+            }
+
+            // validate that block-size has been set
+            if (line.hasOption("coeflim")) {
+                log("coeflim option is unsupported at the moment");
+                return;
+            }
+
+            if (line.hasOption("coeflim-small")) {
+                log("coeflim-small option is unsupported at the moment");
+                return;
+            }
+            if (line.hasOption(
+                    "find-best-divisor-when-dividing-for-overflow")) {
+                log("find-best-divisor-when-dividing-for-overflow option is unsupported at the moment");
+                return;
+            }
+            if (line.hasOption("round-reason")) {
+                log("round-reason option is unsupported at the moment");
+                return;
+            }
+            if (line.hasOption("rounding-weaken-priority")) {
+                log("rounding-weaken-priority option is unsupported at the moment");
+                return;
+            }
+            if (line.hasOption("weaken-nonimplied")) {
+                log("weaken-nonimplied option is unsupported at the moment");
+                return;
+            }
+            System.out.println(solver.toString("c "));
+            String [] leftArgs = line.getArgs();
+            if (leftArgs.length==0) {
+                System.err.println("Missing filename");
+                return;
+            }
+            String filename = leftArgs[leftArgs.length-1];
+            PBSolverHandle handle = new PBSolverHandle(new PseudoOptDecorator(solver));
+            OPBReader2012 reader = new OPBReader2012(handle);
+            IPBSolver optimizer = new OptToPBSATAdapter(handle);
+            try {
+                reader.parseInstance(filename);
+                if (optimizer.isSatisfiable()) {
+                    System.out.println("s OPTIMUM FOUND");
+                    System.out.println("v "+reader.decode(optimizer.model())+" 0");
+                } else {
+                    System.out.println("s UNSATISFIABLE");
+                }
+                optimizer.printStat(System.out, "c ");
+            } catch (TimeoutException e) {
+                System.out.println("s UNKNOWN");
+            } catch (ParseFormatException e) {
+                // TODO Auto-generated catch block
+                e.printStackTrace();
+            } catch (IOException e) {
+                // TODO Auto-generated catch block
+                e.printStackTrace();
+            } catch (ContradictionException e) {
+                // TODO Auto-generated catch block
+                e.printStackTrace();
+            }
+        } catch (ParseException exp) {
+            System.out.println("Unexpected exception:" + exp.getMessage());
+        }
+    }
+}

pom.xml

@@ -74,10 +74,10 @@ Sat4j is a full featured boolean reasoning library designed to bring state-of-th
 	</developers>
 	<properties>
 		<!-- compiler params -->
-		<javaSource>1.6</javaSource>
-		<javaTarget>1.6</javaTarget>
-		<testSource>1.6</testSource>
-		<testTarget>1.6</testTarget>
+		<javaSource>1.7</javaSource>
+		<javaTarget>1.7</javaTarget>
+		<testSource>1.7</testSource>
+		<testTarget>1.7</testTarget>
 		<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
 		<!-- common distribution locations -->
 		<siteRepositoryId />