Skip to content

Instantly share code, notes, and snippets.

@meitinger

meitinger/lics-3.dimacs

Created October 27, 2018 22:43
Show Gist options
  • Save meitinger/ccd369e75b56e9edf47d1445904c3b68 to your computer and use it in GitHub Desktop.
Save meitinger/ccd369e75b56e9edf47d1445904c3b68 to your computer and use it in GitHub Desktop.
Download ZIP
All LICS excercises.
Raw
lics-3.dimacs
c 1 = Burgenland, Rot
c 2 = Burgenland, Gruen
c 3 = Burgenland, Blau
c 4 = Kaernten, Rot
c 5 = Kaernten, Gruen
c 6 = Kaernten, Blau
c 7 = Niederoesterreich, Rot
c 8 = Niederoesterreich, Gruen
c 9 = Niederoesterreich, Blau
c 10 = Oberoesterreich, Rot
c 11 = Oberoesterreich, Gruen
c 12 = Oberoesterreich, Blau
c 13 = Salzburg, Rot
c 14 = Salzburg, Gruen
c 15 = Salzburg, Blau
c 16 = Steiermark, Rot
c 17 = Steiermark, Gruen
c 18 = Steiermark, Blau
c 19 = Tirol, Rot
c 20 = Tirol, Gruen
c 21 = Tirol, Blau
c 22 = Vorarlberg, Rot
c 23 = Vorarlberg, Gruen
c 24 = Vorarlberg, Blau
c 25 = Wien, Rot
c 26 = Wien, Gruen
c 27 = Wien, Blau
p cnf 27 102
1 2 3 0
4 5 6 0
7 8 9 0
10 11 12 0
13 14 15 0
16 17 18 0
19 20 21 0
22 23 24 0
25 26 27 0
-1 -2 0
-1 -3 0
-2 -1 0
-2 -3 0
-3 -1 0
-3 -2 0
-4 -5 0
-4 -6 0
-5 -4 0
-5 -6 0
-6 -4 0
-6 -5 0
-7 -8 0
-7 -9 0
-8 -7 0
-8 -9 0
-9 -7 0
-9 -8 0
-10 -11 0
-10 -12 0
-11 -10 0
-11 -12 0
-12 -10 0
-12 -11 0
-13 -14 0
-13 -15 0
-14 -13 0
-14 -15 0
-15 -13 0
-15 -14 0
-16 -17 0
-16 -18 0
-17 -16 0
-17 -18 0
-18 -16 0
-18 -17 0
-19 -20 0
-19 -21 0
-20 -19 0
-20 -21 0
-21 -19 0
-21 -20 0
-22 -23 0
-22 -24 0
-23 -22 0
-23 -24 0
-24 -22 0
-24 -23 0
-25 -26 0
-25 -27 0
-26 -25 0
-26 -27 0
-27 -25 0
-27 -26 0
-1 -7 0
-2 -8 0
-3 -9 0
-1 -16 0
-2 -17 0
-3 -18 0
-4 -13 0
-5 -14 0
-6 -15 0
-4 -16 0
-5 -17 0
-6 -18 0
-4 -19 0
-5 -20 0
-6 -21 0
-7 -10 0
-8 -11 0
-9 -12 0
-7 -16 0
-8 -17 0
-9 -18 0
-7 -25 0
-8 -26 0
-9 -27 0
-10 -13 0
-11 -14 0
-12 -15 0
-10 -16 0
-11 -17 0
-12 -18 0
-13 -16 0
-14 -17 0
-15 -18 0
-13 -19 0
-14 -20 0
-15 -21 0
-19 -22 0
-20 -23 0
-21 -24 0
Raw
lics-7-net.cs
/* Copyright (C) 2017, Manuel Meitinger
*
* This program is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 2 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program. If not, see <http://www.gnu.org/licenses/>.
*/
#define DEPTH
#if SOLVING || IDEAL
#define COMPARATORS
#endif
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
static class Program
{
struct Comparator
{
public readonly int LoWire;
public readonly int HiWire;
public readonly int LoShift;
public readonly int HiShift;
public Comparator(int loWire, int hiWire)
{
LoWire = loWire;
HiWire = hiWire;
LoShift = 1 << loWire;
HiShift = 1 << hiWire;
}
public override string ToString()
{
return "(" + (LoWire + 1) + "<=" + (HiWire + 1) + ")";
}
}
class Step : IComparable<Step>
{
#if DEPTH
public readonly int Depth;
private readonly int[] Depths;
#endif
private readonly Comparator Comparator;
#if IDEAL
public readonly Dictionary<Comparator, int> IdealComparators = new Dictionary<Comparator, int>();
#endif
private readonly long Hash;
private readonly HashSet<int> Inputs = new HashSet<int>();
public readonly Step Parent;
public readonly Dictionary<Comparator, int> PossibleComparators = new Dictionary<Comparator, int>();
private readonly HashSet<int> Solution;
#if SOLVING
public readonly Dictionary<Comparator, int> SolvingComparators = new Dictionary<Comparator, int>();
#endif
public readonly int SwappingsDeviation;
public readonly int SwappingsTotal;
public readonly int TotalComparators;
public readonly int Wires;
public int UnsortedCount { get { return Inputs.Count; } }
public Step(Step parent, Comparator comparator)
{
Parent = parent;
Comparator = comparator;
Wires = parent.Wires;
TotalComparators = parent.TotalComparators + 1;
Solution = parent.Solution;
#if DEPTH
Depths = (int[])parent.Depths.Clone();
var maxDepth = Math.Max(Depths[comparator.LoWire], Depths[comparator.HiWire]) + 1;
Depths[comparator.LoWire] = maxDepth;
Depths[comparator.HiWire] = maxDepth;
Depth = Math.Max(parent.Depth, maxDepth);
#endif
foreach (var input in parent.Inputs)
{
var newValue = input;
if ((comparator.LoShift & newValue) != 0)
{
if ((comparator.HiShift & newValue) == 0)
{
newValue ^= (comparator.LoShift | comparator.HiShift);
}
}
AddNumber(newValue);
}
Hash = ComputeHash(out SwappingsTotal, out SwappingsDeviation);
}
public Step(int wires)
{
Parent = null;
Comparator = default(Comparator);
Wires = wires;
TotalComparators = 0;
Solution = new HashSet<int>();
#if DEPTH
Depths = new int[wires];
Depth = 0;
#endif
var n = 0;
Solution.Add(n);
for (var i = wires - 1; i >= 0; i--)
{
n |= 1 << i;
Solution.Add(n);
}
for (var i = (1 << wires) - 1; i >= 0; i--)
{
AddNumber(i);
}
Hash = ComputeHash(out SwappingsTotal, out SwappingsDeviation);
}
private void AddNumber(int number)
{
if (Solution.Contains(number))
{
return;
}
if (Inputs.Add(number))
{
var ones = Wires;
for (int i = Wires - 1, mask = 1; i >= 0; i--, mask <<= 1)
{
if ((mask & number) != 0)
{
ones--;
}
}
#if COMPARATORS
var wrongZeros = new List<int>(Wires);
var wrongOnes = new List<int>(Wires);
#endif
for (int i = Wires - 1, maskMSB = 1 << i; i >= 0; i--, maskMSB >>= 1)
{
var isOne = (maskMSB & number) != 0;
#if COMPARATORS
var expectOne = i >= ones;
if (isOne != expectOne)
{
(expectOne ? wrongZeros : wrongOnes).Add(i);
}
#endif
if (!isOne)
{
for (int j = 0, maskLSB = 1; j < i; j++, maskLSB <<= 1)
{
if ((maskLSB & number) != 0)
{
IncrementComparator(PossibleComparators, j, i);
}
}
}
}
#if IDEAL
for (var i = wrongOnes.Count - 1; i >= 0; i--)
{
for (var j = wrongZeros.Count - 1; j >= 0; j--)
{
IncrementComparator(IdealComparators, wrongOnes[i], wrongZeros[j]);
}
}
#endif
#if SOLVING
if (wrongOnes.Count == 1 && wrongZeros.Count == 1)
{
IncrementComparator(SolvingComparators, wrongOnes[0], wrongZeros[0]);
}
#endif
}
}
private long ComputeHash(out int total, out int deviation)
{
var classes = new SortedDictionary<int, int>();
var sum = 0;
var sum_2 = 0;
foreach (var value in PossibleComparators.Values)
{
sum += value;
sum_2 += value * value;
int count;
if (classes.TryGetValue(value, out count))
{
classes[value] = count + 1;
}
else
{
classes.Add(value, 1);
}
}
total = sum;
deviation = (sum_2 * PossibleComparators.Count) - (sum * sum);
var hash = 0L;
foreach (var entry in classes)
{
hash ^= (long)entry.Value;
hash ^= (long)entry.Key << 32;
}
return hash;
}
private void IncrementComparator(IDictionary<Comparator, int> dict, int loWire, int hiWire)
{
var comp = new Comparator(loWire, hiWire);
int prevValue;
if (dict.TryGetValue(comp, out prevValue))
{
dict[comp] = prevValue + 1;
}
else
{
dict.Add(comp, 1);
}
}
public override string ToString()
{
var builder = new StringBuilder();
builder.AppendLine("Step");
#if DEPTH
builder.Append(" Depth: ").Append(Depth).AppendLine();
#endif
builder.Append(" Total Comparators: ").Append(TotalComparators).AppendLine();
builder.Append(" Unsorted: ").Append(Inputs.Count).AppendLine();
var step = this;
var i = TotalComparators;
var comps = new Comparator[i];
while (i-- > 0)
{
comps[i] = step.Comparator;
step = step.Parent;
}
builder.Append(" Comparators: [").Append(string.Join(", ", comps)).Append("]").AppendLine();
builder.Append(" Swapping Total: ").Append(SwappingsTotal).AppendLine();
builder.Append(" Swapping Deviation: ").Append((float)SwappingsDeviation / ((float)PossibleComparators.Count * (float)PossibleComparators.Count)).AppendLine();
AppendComparators(builder, "Possible Comparators", PossibleComparators);
#if SOLVING
AppendComparators(builder, "Solving Comparators", SolvingComparators);
#endif
#if IDEAL
AppendComparators(builder, "Incremental Comparators", IdealComparators);
#endif
return builder.ToString();
}
private void AppendComparators(StringBuilder builder, string name, Dictionary<Comparator, int> dict)
{
builder.Append(" ").Append(name).AppendLine(":");
foreach (var entry in dict.OrderByDescending(c => c.Value))
{
builder.Append(" ").Append(entry.Value).Append(": ").Append(entry.Key).AppendLine();
}
}
public int CompareTo(Step other)
{
var result = TotalComparators - other.TotalComparators;
if (result == 0)
{
result = PossibleComparators.Count - other.PossibleComparators.Count;
if (result == 0)
{
result = SwappingsTotal - other.SwappingsTotal;
#if DEPTH
if (result == 0)
{
result = Depth - other.Depth;
#endif
if (result == 0)
{
result = Inputs.Count - other.Inputs.Count;
if (result == 0)
{
result = SwappingsDeviation - other.SwappingsDeviation;
if (result == 0)
{
result = (int)(Hash - other.Hash);
}
}
#if DEPTH
}
#endif
}
}
}
return result;
}
}
private static int BestDepth = int.MaxValue;
private static int LimitComparators = int.MaxValue;
private static void FindBest(Step root, int setSize, int sameEntries)
{
var steps = new List<Step>();
steps.Add(root);
var subSteps = new Step[setSize];
var subStepsCount = 0;
do
{
foreach (var step in steps)
{
var depth = step.Depth;
var comps = step.TotalComparators;
if (comps > LimitComparators || comps == LimitComparators && depth >= BestDepth)
{
continue;
}
var unsorted = step.UnsortedCount;
if (unsorted == 0)
{
if (comps < LimitComparators || comps == LimitComparators && depth < BestDepth)
{
LimitComparators = comps;
BestDepth = depth;
Console.WriteLine(step);
}
continue;
}
foreach (var subStep in step.PossibleComparators.Keys.AsParallel().Select(c => new Step(step, c)))
{
var index = Array.BinarySearch(subSteps, 0, subStepsCount, subStep);
if (index < 0)
{
index = ~index;
}
else
{
var sames = sameEntries;
while (--sames > 0 && ++index < subStepsCount)
{
if (subSteps[index].CompareTo(subStep) > 0)
{
break;
}
}
if (sames == 0)
{
continue;
}
}
if (index < setSize)
{
var limit = subStepsCount < setSize ? subStepsCount++ : setSize - 1;
Array.Copy(subSteps, index, subSteps, index + 1, limit - index);
subSteps[index] = subStep;
}
}
}
steps.Clear();
for (var i = subStepsCount - 1; i >= 0; i--)
{
steps.Add(subSteps[i]);
}
Array.Clear(subSteps, 0, subStepsCount);
subStepsCount = 0;
GC.Collect();
if (steps.Count > 0)
{
Console.WriteLine("{0} / comps {1}-{2} / swaps {3}-{4} / unsorted {5}-{6}", steps.Count, steps.Min(s => s.PossibleComparators.Count), steps.Max(s => s.PossibleComparators.Count), steps.Min(s => s.SwappingsTotal), steps.Max(s => s.SwappingsTotal), steps.Min(s => s.UnsortedCount), steps.Max(s => s.UnsortedCount));
}
}
while (steps.Count > 0);
}
static void Main()
{
try
{
Console.Write("Wires: ");
var wires = int.Parse(Console.ReadLine());
if (wires < 2)
{
throw new ArgumentOutOfRangeException("Wires");
}
var step = new Step(wires);
Console.Write("Comparators: ");
var comparators = Console.ReadLine().Split(new char[] { ' ' }, StringSplitOptions.RemoveEmptyEntries);
if (comparators.Length % 2 != 0)
{
throw new ArgumentOutOfRangeException("Comparators");
}
for (var i = 0; i < comparators.Length; i += 2)
{
var lo = int.Parse(comparators[i]);
var hi = int.Parse(comparators[i + 1]);
if (lo < 1 || lo >= wires || hi < 1 || lo >= hi)
{
throw new ArgumentOutOfRangeException("Comparators");
}
step = new Step(step, new Comparator(lo - 1, hi - 1));
}
Console.WriteLine(step);
Console.Write("Set Size: ");
var setSize = int.Parse(Console.ReadLine());
if (setSize < 1)
{
throw new ArgumentOutOfRangeException("Set Size");
}
Console.Write("Same Entries: ");
var sameEntries = int.Parse(Console.ReadLine());
if (sameEntries < -1 || sameEntries > setSize)
{
throw new ArgumentOutOfRangeException("Same Entries");
}
FindBest(step, setSize, sameEntries);
}
catch (Exception e)
{
Console.WriteLine(e);
}
}
}
Raw
lics-8-colors.hs
dimacs n = "p cnf " ++ show n ++ " " ++ show (2 * length eqs) ++ "\n" ++ show' id eqs ++ show' negate eqs
where
eqs = [[x,y,x+y,0] | x <- [1..n], y <- [x+1..n], x + y <= n]
show' f = unlines . map (unwords . map (show . f))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment