Author: jvanzyl
Date: Sun Jun 1 21:01:41 2008
New Revision: 662312
URL: http://svn.apache.org/viewvc?rev=662312&view=rev
Log:
MARTIFACT-20: We now have ranges calculating correctly with the simple model
and the SAT solver
Submitted by: Oleg Gusakov
Modified:
maven/sandbox/trunk/mercury/.settings/org.eclipse.jdt.core.prefs
maven/sandbox/trunk/mercury/.settings/org.maven.ide.eclipse.prefs
maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java
maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java
maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java
maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java
Modified: maven/sandbox/trunk/mercury/.settings/org.eclipse.jdt.core.prefs
URL:
http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/.settings/org.eclipse.jdt.core.prefs?rev=662312&r1=662311&r2=662312&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/.settings/org.eclipse.jdt.core.prefs (original)
+++ maven/sandbox/trunk/mercury/.settings/org.eclipse.jdt.core.prefs Sun Jun 1
21:01:41 2008
@@ -1,6 +1,23 @@
-#Fri May 23 16:49:34 PDT 2008
+#Mon Jun 02 19:04:45 PDT 2008
eclipse.preferences.version=1
org.eclipse.jdt.core.builder.cleanOutputFolder=ignore
+org.eclipse.jdt.core.builder.duplicateResourceTask=warning
+org.eclipse.jdt.core.builder.invalidClasspath=abort
+org.eclipse.jdt.core.builder.recreateModifiedClassFileInOutputFolder=ignore
+org.eclipse.jdt.core.builder.resourceCopyExclusionFilter=*.launch
+org.eclipse.jdt.core.circularClasspath=error
+org.eclipse.jdt.core.classpath.exclusionPatterns=enabled
+org.eclipse.jdt.core.classpath.multipleOutputLocations=enabled
+org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5
+org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
org.eclipse.jdt.core.compiler.compliance=1.5
+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.maxProblemPerUnit=100
+org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
+org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
org.eclipse.jdt.core.compiler.source=1.5
+org.eclipse.jdt.core.incompatibleJDKLevel=ignore
+org.eclipse.jdt.core.incompleteClasspath=error
Modified: maven/sandbox/trunk/mercury/.settings/org.maven.ide.eclipse.prefs
URL:
http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/.settings/org.maven.ide.eclipse.prefs?rev=662312&r1=662311&r2=662312&view=diff
==============================================================================
--- maven/sandbox/trunk/mercury/.settings/org.maven.ide.eclipse.prefs (original)
+++ maven/sandbox/trunk/mercury/.settings/org.maven.ide.eclipse.prefs Sun Jun
1 21:01:41 2008
@@ -1,9 +1,9 @@
-#Fri May 23 16:49:28 PDT 2008
+#Mon Jun 02 12:43:42 PDT 2008
activeProfiles=
eclipse.preferences.version=1
-filterResources=true
+filterResources=false
includeModules=false
resolveWorkspaceProjects=true
resourceFilterGoals=process-resources resources\:testResources
-useMavenFolders=true
+useMavenFolders=false
version=1
Modified:
maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java
URL:
http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java?rev=662312&r1=662311&r2=662312&view=diff
==============================================================================
---
maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java
(original)
+++
maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolver.java
Sun Jun 1 21:01:41 2008
@@ -77,17 +77,26 @@
public SatConstraint addOrGroup( List<List<ArtifactMetadata>> orGroup )
throws SatException
{
+ if( orGroup == null || orGroup.size() < 1 )
+ throw new SatException("cannot process empty OR group");
+
SatConstraint constraint = null;
+ int minLen = orGroup.get(0).size();
+
for( List<ArtifactMetadata> branch : orGroup )
{
if( constraint == null )
constraint = new SatConstraint( branch, context );
else
- constraint.addOr( branch, context );
+ constraint.addOrGroupMember( branch, context );
+ if( branch.size() < minLen )
+ minLen = branch.size();
}
if( constraint != null )
{
+ constraint.cardinality = minLen;
+ System.out.println("Contraint is "+constraint.toString() );
SatClause clause = constraint.getClause();
try
{
@@ -112,17 +121,11 @@
{
SatConstraint constraint = new SatConstraint( pivot, context );
-System.out.print("\n context is : "+context.toString() );
-System.out.println("\n pivot is : "+pivot );
-
try
{
int [] vars1 = constraint.getVarray();
int varCount1 = vars1.length;
-System.out.print("\n\n array is
:");SatHelper.show(vars1);System.out.print("\n");
-System.out.flush();
-
solver.addPseudoBoolean(
SatHelper.getSmallOnes( vars1 )
, SatHelper.getBigOnes( varCount1 )
@@ -133,22 +136,15 @@
int [] vars2 = constraint.getVarray();
int varCount2 = vars2.length;
-System.out.print(">= 1 is OK\n array is
:");SatHelper.show(vars2);System.out.print("\n");
-System.out.flush();
-
solver.addPseudoBoolean(
SatHelper.getSmallOnes( vars2 )
, SatHelper.getBigOnes( varCount2, true )
, true
, new BigInteger("-1")
);
-
-System.out.println(">= -1 is OK");
-System.out.flush();
}
catch (ContradictionException e)
{
-e.printStackTrace();
throw new SatException( e );
}
@@ -165,8 +161,6 @@
if( solver.isSatisfiable() )
{
res = new ArrayList<ArtifactMetadata>( context.varCount );
-System.out.println("Resulting model : "+solver.model() );
-
for( SatVar v : context.variables )
{
boolean yes = solver.model( v.getNo() );
@@ -174,10 +168,6 @@
res.add( v.getMd() );
}
}
- else
- {
-System.out.println("Failed to solve the problem");
- }
}
catch (TimeoutException e)
{
@@ -186,10 +176,5 @@
return res;
}
//-----------------------------------------------------------------------
- private int addConstraint( ArtifactMetadata md )
- {
- return -1;
- }
- //-----------------------------------------------------------------------
//-----------------------------------------------------------------------
}
Modified:
maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java
URL:
http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java?rev=662312&r1=662311&r2=662312&view=diff
==============================================================================
---
maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java
(original)
+++
maven/sandbox/trunk/mercury/src/main/java/org/apache/maven/mercury/metadata/sat/SatConstraint.java
Sun Jun 1 21:01:41 2008
@@ -23,6 +23,7 @@
variables = new HashMap<Integer,Integer>( mdl.size() );
+ // first member of the group => do not decrement cardinality
for( ArtifactMetadata md : mdl )
{
SatVar var = context.find( md );
@@ -30,25 +31,31 @@
}
}
//----------------------------------------------------------------------------
- private void add( SatVar var )
+ /**
+ * @return true if a new literal was added to this constraint
+ */
+ private boolean add( SatVar var )
{
Integer varNo = new Integer( var.getNo() );
// TODO ?? check if this does not break the solver
if( variables.containsKey(varNo) )
- return;
+ return false;
variables.put( varNo, new Integer(1) );
++cardinality;
+ return true;
}
//----------------------------------------------------------------------------
- public void addOr(List<ArtifactMetadata> branch, SatContext context )
+ public void addOrGroupMember(List<ArtifactMetadata> branch, SatContext
context )
throws SatException
{
+ boolean newVars = false;
for( ArtifactMetadata md : branch )
{
SatVar var = context.find( md );
- add( var );
+ if( add( var ) )
+ newVars = true;
}
}
//----------------------------------------------------------------------------
@@ -111,7 +118,7 @@
{
sb.append( " +"+e.getValue()+"*x"+e.getKey() );
}
- return sb.toString();
+ return sb.toString()+" >= "+cardinality;
}
//----------------------------------------------------------------------------
Modified:
maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java
URL:
http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java?rev=662312&r1=662311&r2=662312&view=diff
==============================================================================
---
maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java
(original)
+++
maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/DefaultSatSolverTest.java
Sun Jun 1 21:01:41 2008
@@ -14,6 +14,7 @@
extends TestCase
{
DefaultSatSolver ss;
+ String title;
List< List<ArtifactMetadata> > or;
//----------------------------------------------------------------------
@@ -41,9 +42,42 @@
assert ss.context.varCount == 3 : "expected 3 variables in the context,
but found "+ss.context.varCount;
}
//----------------------------------------------------------------------
+ public void testSimpleResolution()
+ throws SatException
+ {
+ title = "simple 3-node tree";
+ ss = (DefaultSatSolver) DefaultSatSolver.create(6);
+
+ or = new ArrayList< List<ArtifactMetadata> >(3);
+
+ ss.addPivot( SatHelper.createList("t:b:1","t:b:2","t:b:3") );
+
+ or.add( SatHelper.createList("t:a:1","t:b:1") );
+ or.add( SatHelper.createList("t:a:1","t:b:2") );
+ or.add( SatHelper.createList("t:a:1","t:b:3") );
+ ss.addOrGroup(or);
+
+ List<ArtifactMetadata> res = ss.solve();
+
+ assert res != null : "Failed to solve "+title;
+ assert res.size() == 2 : "result contains "+res.size()+" artifacts instead
of 2";
+
+ if( res != null )
+ {
+ System.out.println("\nResult:");
+ for( ArtifactMetadata md : res )
+ {
+ System.out.print(" "+md);
+ }
+ }
+ }
+ //----------------------------------------------------------------------
public void testResolution()
throws SatException
{
+ title = "simple 2 ranges tree";
+ System.out.println("\n"+title);
+
ss = (DefaultSatSolver) DefaultSatSolver.create(6);
or = new ArrayList< List<ArtifactMetadata> >(3);
@@ -63,16 +97,19 @@
or.add( SatHelper.createList("t:a:1","t:c:2","t:b:2") );
or.add( SatHelper.createList("t:a:1","t:c:2","t:b:3") );
ss.addOrGroup(or);
+
+ System.out.println( "Context: "+ss.context.toString() );
List<ArtifactMetadata> res = ss.solve();
- if( res != null )
- for( ArtifactMetadata md : res )
- {
- System.out.println(md);
- }
- else
- System.out.println( "Result: "+res);
+ assert res != null : "Failed to solve "+title;
+// assert res.size() == 2 : "result contains "+res.size()+" artifacts
instead of 2";
+
+ System.out.println("\n"+title+" result:");
+ for( ArtifactMetadata md : res )
+ {
+ System.out.print(" "+md);
+ }
}
//----------------------------------------------------------------------
//----------------------------------------------------------------------
Modified:
maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java
URL:
http://svn.apache.org/viewvc/maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java?rev=662312&r1=662311&r2=662312&view=diff
==============================================================================
---
maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java
(original)
+++
maven/sandbox/trunk/mercury/src/test/java/org/apache/maven/mercury/metadata/sat/SatFeedTest.java
Sun Jun 1 21:01:41 2008
@@ -213,5 +213,182 @@
showRes( title );
}
//---------------------------------------------------------------
+ public void testSmallestRealProblem()
+ throws ContradictionException, TimeoutException
+ {
+ // x2
+ // x1 <or
+ // x3
+ String title = "Smallest Real problem";
+ pbSolver.newVar(3);
+
+ // x2 + x3 = 1
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 2, 3 )
+ , SatHelper.getBigOnes(2)
+ , true, new BigInteger("1")
+ );
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 2, 3 )
+ , SatHelper.getBigOnes( 2, true )
+ , true, new BigInteger("-1")
+ );
+
+ // x1 + x2 >= 2 OR x1 + x3 >= 2
+ // x1 + x2 + x3 >= 2
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 1, 2, 3 )
+ , SatHelper.getBigOnes( 3 )
+ , true, new BigInteger("2")
+ );
+
+ boolean satisfiable = pbSolver.isSatisfiable();
+ assert satisfiable : "Cannot find a solution to "+title+" problem";
+
+ assert pbSolver.model(1) : "x1 should be true";
+ assert pbSolver.model(2) || pbSolver.model(3) : "x2 or x3 should be true";
+
+ showRes( title );
+ }
+ //---------------------------------------------------------------
+ public void testTwoStepRealProblem()
+ throws ContradictionException, TimeoutException
+ {
+ // x3
+ // x2 <or
+ // / x4
+ // x1 <
+ // \
+ // x5 - x6
+ // \ or
+ // x7
+ String title = "2-step real problem";
+ pbSolver.newVar(7);
+
+ // x3 + x4 = 1
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 3, 4 )
+ , SatHelper.getBigOnes(2)
+ , true, new BigInteger("1")
+ );
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 3, 4 )
+ , SatHelper.getBigOnes( 2, true )
+ , true, new BigInteger("-1")
+ );
+
+ // x6 + x7 = 1
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 6, 7 )
+ , SatHelper.getBigOnes(2)
+ , true, new BigInteger("1")
+ );
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 6, 7 )
+ , SatHelper.getBigOnes( 2, true )
+ , true, new BigInteger("-1")
+ );
+
+ // x1 + x2 + x3 >= 2 OR x1 + x2 + x4 >= 2
+ // x1 + x2 + x3 +x4 >= 3
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 1, 2, 3, 4 )
+ , SatHelper.getBigOnes( 4 )
+ , true, new BigInteger("3")
+ );
+
+ // x1 + x5 + x6 >= 3 OR x1 + x5 + x7 >= 3
+ // x1 + x5 + x6 + x7 >= 3
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 1, 5, 6, 7 )
+ , SatHelper.getBigOnes( 4 )
+ , true, new BigInteger("3")
+ );
+
+ boolean satisfiable = pbSolver.isSatisfiable();
+ assert satisfiable : "Cannot find a solution to "+title+" problem";
+
+ assert pbSolver.model(1) : "x1 should be true";
+ assert pbSolver.model(2) : "x2 should be true";
+ assert pbSolver.model(3) || pbSolver.model(4) : "x3 or x4 should be true";
+ assert ! (pbSolver.model(3) && pbSolver.model(4)) : "x3 or x4 should be
false";
+ assert pbSolver.model(5) : "x5 should be true";
+ assert pbSolver.model(6) || pbSolver.model(7) : "x6 or x7 should be true";
+ assert ! (pbSolver.model(6) && pbSolver.model(7)) : "x6 or x7 should be
false";
+
+ showRes( title );
+ }
+ //---------------------------------------------------------------
+ public void testTwoOrsInOneBranch()
+ throws ContradictionException, TimeoutException
+ {
+ // x3
+ // x2 <or
+ // / x4
+ // / \
+ // / x5 - x6
+ // / \ or
+ // / +- x7
+ // x1 <
+ // \ x8 - x7
+ String title = "really real problem";
+ pbSolver.newVar(8);
+
+ // x3 + x4 = 1
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 3, 4 )
+ , SatHelper.getBigOnes(2)
+ , true, new BigInteger("1")
+ );
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 3, 4 )
+ , SatHelper.getBigOnes( 2, true )
+ , true, new BigInteger("-1")
+ );
+
+ // x6 + x7 = 1
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 6, 7 )
+ , SatHelper.getBigOnes(2)
+ , true, new BigInteger("1")
+ );
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 6, 7 )
+ , SatHelper.getBigOnes( 2, true )
+ , true, new BigInteger("-1")
+ );
+
+ // x1 + x2 + x3 >= 3 OR x1 + x2 + x4 + x5 + x6 >= 5 OR x1 + x2 + x4 + x5 +
x7 >= 5
+ // x1 + x2 + x3 >= 3 OR x1 + x2 + x4 + x5 + x6 +x7 >= 5
+ // x1 + x2 + x3 + x4 + x5 + x6 +x7 >= 5
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 1, 2, 3, 4, 5, 6, 7 )
+ , SatHelper.getBigOnes( 7 )
+ , true, new BigInteger("5")
+ );
+
+ // x1 + x8 + x7 >= 3
+ pbSolver.addPseudoBoolean(
+ SatHelper.getSmallOnes( 1, 8, 7 )
+ , SatHelper.getBigOnes( 3 )
+ , true, new BigInteger("3")
+ );
+
+ boolean satisfiable = pbSolver.isSatisfiable();
+ assert satisfiable : "Cannot find a solution to "+title+" problem";
+
+ assert pbSolver.model(1)
+ && pbSolver.model(2)
+ && pbSolver.model(4)
+ && pbSolver.model(5)
+ && pbSolver.model(7)
+ && pbSolver.model(8)
+ : "x1 & x2 & x4 & x5 & x7 & x8 should be true";
+ assert !pbSolver.model(3) : "x3 should be false";
+ assert !pbSolver.model(6) : "x6 should be false";
+
+ showRes( title );
+ }
+ //---------------------------------------------------------------
//---------------------------------------------------------------
}
