Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A greatly simplified version of https://github.com/tuzz/supersat
# This is a greatly simplified version of https://github.com/tuzz/supersat
# It reduces the superpermutation problem to boolean satisfiability.
#
# To generate a SAT problem for N=3, LENGTH=9:
# ruby simplesupersat.rb 3 9
#
# And to run a SAT solver on it:
# lingeling 3-9.dimacs
N = Integer(ARGV[0])
LENGTH = Integer(ARGV[1])
filename = "#{N}-#{LENGTH}.dimacs"
@file = File.open(filename, "w")
def next_variable
@variable_count ||= 0
@variable_count += 1
end
def variable(name)
@variables ||= {}
@variables[name] ||= next_variable
end
def clause(string)
@clause_count ||= 0
@clause_count += 1
@file.print string
@file.puts " 0"
end
# The input string has exactly one symbol at each time:
LENGTH.times do |time|
symbols = N.times.map do |symbol|
variable("Symbol_#{time}_#{symbol}")
end
# At most one:
symbols.combination(2) do |(a, b)|
clause "-#{a} -#{b}"
end
# At least one:
clause symbols.join(" ")
end
# The input string starts with ascending numbers:
N.times do |time|
clause variable("Symbol_#{time}_#{time}")
end
bits = Math.log2(LENGTH).ceil
max = 2 ** bits
permutations = 0.upto(N - 1).to_a.permutation.to_a
max.times do |position|
binary = position.to_s(2).rjust(bits, "0")
bools = binary.chars.map { |c| c == "1" }
permutations.each do |perm|
variables = bits.times.map do |bit|
variable("Address_#{perm.join}_bit_#{bit}")
end
literals = variables.zip(bools).map do |v, b|
"#{"-" if b}#{v}"
end
# Ban invalid addresses that go past the end of the input string:
if position + N > LENGTH
clause literals.join(" ")
next
end
# The symbols for the permutation must be at that address in the string:
perm.each.with_index do |symbol, i|
time = position + i
symbol = [variable("Symbol_#{time}_#{symbol}")]
clause (literals + symbol).join(" ")
end
end
end
@file.close
File.open("#{filename}.tmp", "w") do |file|
file.puts "p cnf #{@variable_count} #{@clause_count}"
File.foreach(filename) do |line|
file.puts line
end
end
require "fileutils"
FileUtils.mv("#{filename}.tmp", filename)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.