Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Relates to #5: Test case for the xor-chain formula

  • Loading branch information...
commit 9cd8ef2db307737fbe449bd3516a6d0465f96104 1 parent 27e75ae
@dmitrygusev dmitrygusev authored
View
85 3-sat-core/src/test/java/com/anjlab/sat3/TestXorChain.java
@@ -0,0 +1,85 @@
+package com.anjlab.sat3;
+
+import static org.junit.Assert.fail;
+
+import java.util.Properties;
+
+import org.junit.BeforeClass;
+import org.junit.Test;
+
+import cern.colt.list.ObjectArrayList;
+
+import com.anjlab.sat3.EmptyStructureException;
+import com.anjlab.sat3.Helper;
+import com.anjlab.sat3.ICompactTripletsStructure;
+import com.anjlab.sat3.IHyperStructure;
+import com.anjlab.sat3.ITabularFormula;
+
+public class TestXorChain
+{
+ @BeforeClass
+ public static void setup()
+ {
+ Helper.UsePrettyPrint = true;
+ Helper.EnableAssertions = true;
+ System.out.println(TestXorChain.class.getName());
+ }
+
+ @Test
+ public void testStructuresFromReducedHSS() throws Exception
+ {
+ ObjectArrayList cts = new ObjectArrayList(
+ new ITabularFormula[] {
+ Helper.loadFromFile("target/test-classes/xor-chain/basic-cts.cnf"),
+ Helper.loadFromFile("target/test-classes/xor-chain/hss-0-other-cts.cnf"),
+ }
+ );
+
+ Helper.prettyPrint((ITabularFormula) cts.get(0));
+ Helper.prettyPrint((ITabularFormula) cts.get(1));
+
+ try
+ {
+ ObjectArrayList hss = Helper.createHyperStructuresSystem(
+ cts, (ICompactTripletsStructure) cts.get(0), new Properties());
+
+ System.out.println("Writing HSS(0) image to filesystem...");
+ Helper.writeToImage((IHyperStructure) hss.get(0), null, null, "target/test-classes/xor-chain/hs.png");
+ System.out.println("Done");
+
+ fail("Non-empty HSS for UNSAT instance can't be built according to the Theorem 1");
+ }
+ catch (EmptyStructureException e)
+ {
+ // Okay
+ }
+
+ // Save CTS set into a single CNF file
+// SimpleFormula formula = new SimpleFormula();
+// for (int i = 0; i < cts.size(); i++)
+// {
+// ICompactTripletsStructure s = (ICompactTripletsStructure) cts.get(i);
+//
+// for (int j = 0; j < s.getTiers().size(); j++)
+// {
+// ITier tier = s.getTier(j);
+// tier.inverse();
+//
+//// if (tier.isEmpty()) continue;
+//
+// Iterator<ITripletValue> iterator = tier.iterator();
+// while (iterator.hasNext())
+// {
+// ITripletValue tripletValue = iterator.next();
+//
+// formula.add(new SimpleTriplet(
+// tier.getAName() * (tripletValue.isNotA() ? -1 : 1),
+// tier.getBName() * (tripletValue.isNotB() ? -1 : 1),
+// tier.getCName() * (tripletValue.isNotC() ? -1 : 1)));
+// }
+//
+// }
+// }
+// Helper.saveToDIMACSFileFormat(formula, "target/test-classes/xor-chain/formula.cnf");
+ }
+}
View
116 3-sat-core/src/test/resources/xor-chain/basic-cts.cnf
@@ -0,0 +1,116 @@
+p cnf 48 115
+-8 42 37 0
+42 37 7 0
+37 7 2 0
+7 2 -24 0
+2 -24 33 0
+-24 33 32 0
+33 32 10 0
+32 10 15 0
+32 10 -15 0
+10 15 11 0
+10 -15 -11 0
+15 11 34 0
+-15 -11 34 0
+11 34 -43 0
+-11 34 -43 0
+34 -43 -22 0
+-43 -22 18 0
+-22 18 20 0
+-22 18 -20 0
+18 20 -38 0
+18 -20 38 0
+20 -38 -19 0
+-20 38 -19 0
+38 -19 36 0
+38 -19 -36 0
+-38 -19 36 0
+-38 -19 -36 0
+-19 36 -39 0
+-19 -36 39 0
+36 -39 28 0
+-36 39 28 0
+39 28 27 0
+-39 28 27 0
+28 27 23 0
+27 23 47 0
+27 23 -47 0
+23 47 9 0
+23 47 -9 0
+23 -47 9 0
+23 -47 -9 0
+47 9 -16 0
+47 -9 16 0
+-47 9 -16 0
+-47 -9 16 0
+9 -16 48 0
+9 -16 -48 0
+-9 16 48 0
+-9 16 -48 0
+16 48 41 0
+16 48 -41 0
+16 -48 41 0
+16 -48 -41 0
+-16 48 41 0
+-16 48 -41 0
+-16 -48 41 0
+-16 -48 -41 0
+48 41 45 0
+48 41 -45 0
+48 -41 45 0
+48 -41 -45 0
+-48 41 45 0
+-48 41 -45 0
+-48 -41 45 0
+-48 -41 -45 0
+41 45 46 0
+41 -45 -46 0
+-41 45 -46 0
+-41 -45 46 0
+45 46 4 0
+45 -46 4 0
+-45 46 4 0
+-45 -46 4 0
+46 4 31 0
+46 4 -31 0
+-46 4 31 0
+-46 4 -31 0
+4 31 -21 0
+4 -31 21 0
+31 -21 17 0
+-31 21 17 0
+21 17 -1 0
+-21 17 -1 0
+17 -1 29 0
+-1 29 -25 0
+29 -25 13 0
+29 -25 -13 0
+-25 13 -14 0
+-25 -13 14 0
+13 -14 30 0
+13 -14 -30 0
+-13 14 30 0
+-13 14 -30 0
+14 30 12 0
+14 30 -12 0
+14 -30 12 0
+14 -30 -12 0
+-14 30 12 0
+-14 30 -12 0
+-14 -30 12 0
+-14 -30 -12 0
+30 12 6 0
+30 -12 6 0
+-30 12 6 0
+-30 -12 6 0
+12 6 5 0
+12 6 -5 0
+-12 6 5 0
+-12 6 -5 0
+6 5 -40 0
+6 -5 -40 0
+5 -40 -26 0
+-5 -40 -26 0
+-40 -26 3 0
+-26 3 -35 0
+3 -35 -44 0
View
120 3-sat-core/src/test/resources/xor-chain/hss-0-other-cts.cnf
@@ -0,0 +1,120 @@
+p cnf 48 119
+-43 7 17 0
+7 17 4 0
+17 4 -44 0
+4 -44 23 0
+-44 23 -26 0
+23 -26 34 0
+-26 34 3 0
+34 3 18 0
+3 18 -35 0
+18 -35 27 0
+-35 27 6 0
+27 6 32 0
+6 32 42 0
+32 42 15 0
+32 42 -15 0
+42 15 46 0
+42 15 -46 0
+42 -15 46 0
+42 -15 -46 0
+15 46 9 0
+15 -46 -9 0
+-15 46 -9 0
+-15 -46 9 0
+46 9 31 0
+46 9 -31 0
+46 -9 31 0
+46 -9 -31 0
+-46 9 31 0
+-46 9 -31 0
+-46 -9 31 0
+-46 -9 -31 0
+9 31 -21 0
+9 -31 21 0
+-9 31 -21 0
+-9 -31 21 0
+31 -21 -19 0
+-31 21 -19 0
+21 -19 33 0
+-21 -19 33 0
+-19 33 2 0
+33 2 -1 0
+2 -1 -22 0
+-1 -22 -40 0
+-22 -40 37 0
+-40 37 -25 0
+37 -25 -8 0
+-25 -8 29 0
+-8 29 45 0
+-8 29 -45 0
+29 45 -38 0
+29 -45 38 0
+45 -38 11 0
+45 -38 -11 0
+-45 38 11 0
+-45 38 -11 0
+38 11 39 0
+38 11 -39 0
+38 -11 39 0
+38 -11 -39 0
+-38 11 39 0
+-38 11 -39 0
+-38 -11 39 0
+-38 -11 -39 0
+11 39 14 0
+11 -39 -14 0
+-11 39 -14 0
+-11 -39 14 0
+39 14 -24 0
+39 -14 -24 0
+-39 14 -24 0
+-39 -14 -24 0
+14 -24 -13 0
+-14 -24 13 0
+-24 13 16 0
+-24 13 -16 0
+-24 -13 16 0
+-24 -13 -16 0
+13 16 -5 0
+13 -16 5 0
+-13 16 5 0
+-13 -16 -5 0
+16 5 36 0
+16 5 -36 0
+16 -5 36 0
+16 -5 -36 0
+-16 5 36 0
+-16 5 -36 0
+-16 -5 36 0
+-16 -5 -36 0
+5 36 30 0
+5 -36 -30 0
+-5 36 -30 0
+-5 -36 30 0
+36 30 20 0
+36 30 -20 0
+36 -30 20 0
+36 -30 -20 0
+-36 30 20 0
+-36 30 -20 0
+-36 -30 20 0
+-36 -30 -20 0
+30 20 12 0
+30 -20 -12 0
+-30 20 -12 0
+-30 -20 12 0
+20 12 -41 0
+20 -12 41 0
+-20 12 -41 0
+-20 -12 41 0
+12 -41 10 0
+-12 41 10 0
+41 10 28 0
+-41 10 28 0
+10 28 47 0
+10 28 -47 0
+28 47 48 0
+28 47 -48 0
+28 -47 48 0
+28 -47 -48 0
View
124 3-sat-core/src/test/resources/xor-chain/x1_16.shuffled.cnf
@@ -0,0 +1,124 @@
+c A permuted SAT Competition 2002 formula with seed=1073937311
+p cnf 46 122
+17 7 43 0
+-33 -2 1 0
+-29 -8 -25 0
+13 -24 14 0
+30 12 -20 0
+42 32 -6 0
+41 -12 -10 0
+45 38 29 0
+7 -17 -43 0
+15 46 -9 0
+-5 30 36 0
+-5 16 -13 0
+-41 12 -10 0
+37 -42 -8 0
+13 -14 24 0
+-14 11 39 0
+2 -24 -7 0
+17 -7 -43 0
+10 32 -33 0
+1 22 40 0
+-34 -15 -11 0
+-11 39 14 0
+36 5 -30 0
+-26 3 -34 0
+-32 33 10 0
+-1 -22 40 0
+-22 18 43 0
+35 3 18 0
+-4 17 -44 0
+-31 21 19 0
+11 15 -34 0
+-44 23 26 0
+-46 9 15 0
+33 32 -10 0
+19 38 -20 0
+38 -29 -45 0
+-44 4 -17 0
+16 13 5 0
+-35 6 -27 0
+35 6 27 0
+-18 -3 35 0
+-16 5 -13 0
+12 20 -30 0
+3 -35 -18 0
+36 28 39 0
+29 -38 -45 0
+-42 8 -37 0
+35 -27 -6 0
+1 -40 -22 0
+34 -11 15 0
+45 -38 -29 0
+-9 -16 0
+42 37 8 0
+34 -15 11 0
+38 -19 20 0
+13 -16 -5 0
+-39 11 14 0
+-42 6 32 0
+-15 46 9 0
+19 -21 31 0
+-41 46 45 0
+8 29 -25 0
+-43 18 22 0
+-17 43 -7 0
+26 -23 44 0
+40 37 -25 0
+7 -24 -2 0
+9 16 0
+20 19 -38 0
+10 -41 -12 0
+-19 -31 -21 0
+-26 34 -3 0
+7 2 24 0
+28 -27 23 0
+6 42 -32 0
+-7 -2 24 0
+-6 -35 27 0
+-40 22 -1 0
+36 -39 -28 0
+-9 -15 -46 0
+23 44 -26 0
+-34 -3 26 0
+29 -8 25 0
+45 -46 41 0
+2 -33 -1 0
+-21 -4 31 0
+-28 -23 -27 0
+-37 -8 42 0
+23 -28 27 0
+-2 -1 33 0
+30 -12 20 0
+-3 -35 18 0
+-40 25 37 0
+-4 21 -31 0
+24 14 -13 0
+-24 -13 -14 0
+-40 -25 -37 0
+-19 21 31 0
+-23 27 28 0
+17 4 44 0
+33 2 1 0
+-20 -38 -19 0
+4 21 31 0
+-33 -32 -10 0
+25 -29 8 0
+39 -28 -36 0
+-22 -18 -43 0
+-12 -30 -20 0
+-36 -30 -5 0
+-17 44 -4 0
+3 34 26 0
+-32 -6 -42 0
+25 -37 40 0
+-31 -21 4 0
+-36 5 30 0
+-23 -44 -26 0
+-36 28 -39 0
+41 -45 46 0
+-39 -11 -14 0
+10 41 12 0
+-45 -46 -41 0
+22 -18 43 0
Please sign in to comment.
Something went wrong with that request. Please try again.