0 0 0 0 0 0
0 a b c 0 0
0 d e f 0 0
0 g h i 0 0
0 0 0 0 0 0
0 0 0 0 0 0
0 0 0 0 0 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 0 0 0 0 0
0 0 0 0 0 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 0 0 0 0 0
0 0 0 0 0 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 * * * * 0
0 0 0 0 0 0
0 0 0 0 0 0
0 0 0 0 0 0
0 0 a b c 0
0 0 d e f 0
0 0 g h i 0
0 0 0 0 0 0
0, 0, 0, 0, 0, 0
0, x0, x4, x5, x6, 0
0, x1, x7, x8, x9, 0
0, x2,x10,x11,x12, 0
0, x3,x13,x14, 1, 0
0, 0, 0, 0, 0, 1'
0, 0, 0, 0, 0, 0
0, x0, x4, x5, x6, 0
0, x1, x7, x8, x9, 0
0, x2,x10,x11,x12, 0
0, x3,x13,x14, 1, 0
0, 0, 0, 0, 0, 1'
solver = "glucose-syrup" # Default solver
Macbi wrote:Here's a program I've been working on for a while. It's a search program along the same lines as lifesrc, WLS and JLS, but it works via a SAT solver (hence "Logic").
$ make
cd syrup/parallel; make r; cp glucose-syrup_release ../../bin/glucose-syrup
make[1]: Entering directory '/Python/logic-life-search-master/solvers/syrup/syrup/parallel'
Compiling: core/Solver.or
In file included from /Python/logic-life-search-master/solvers/syrup/syrup/utils/Options.h:30:0,
from /Python/logic-life-search-master/solvers/syrup/syrup/core/Solver.h:55,
from /Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc:54:
/Python/logic-life-search-master/solvers/syrup/syrup/utils/ParseUtils.h: In function ‘double Glucose::parseDouble(B&)’:
/Python/logic-life-search-master/solvers/syrup/syrup/utils/ParseUtils.h:99:5: warning: this ‘while’ clause does not guard... [-Wmisleading-indentation]
while (*in >= '0' && *in <= '9')
^~~~~
/Python/logic-life-search-master/solvers/syrup/syrup/utils/ParseUtils.h:103:2: note: ...this statement, but the latter is misleadingly indented as if it is guarded by the ‘while’
if (*in != 'e') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3);
^~
/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc In member function ‘void Glucose::Solver::write_char(unsigned char)’:
/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc:326:47: error: ‘putc_unlocked’ was not declared in this scope
if(putc_unlocked((int) ch, certifiedOutput) == EOF)
^
/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc In member function ‘void Glucose::Solver::analyze(Glucose::CRef, Glucose::vec<Glucose::Lit>&, Glucose::vec<Glucose::Lit>&, int&, unsigned int&, unsigned int&)’:
/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc:774:49: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]
if(chanseokStrategy && nblevels <= coLBDBound) {
~~~~~~~~~^~~~~~~~~~~~~
/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc In member function ‘void Glucose::Solver::adaptSolver()’:
/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc:1416:24: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]
if(c.lbd() <= coLBDBound) {
~~~~~~~~^~~~~~~~~~~~~
/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc In member function ‘Glucose::lbool Glucose::Solver::search(int)’:
/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.cc:1562:49: warning: comparison between signed and unsigned integer expressions [-Wsign-compare]
if(chanseokStrategy && nblevels <= coLBDBound) {
~~~~~~~~~^~~~~~~~~~~~~
make[1]: *** [/Python/logic-life-search-master/solvers/syrup/syrup/parallel/../mtl/template.mk:71: /Python/logic-life-search-master/solvers/syrup/syrup/parallel/../core/Solver.or] Error 1
make[1]: Leaving directory '/Python/logic-life-search-master/solvers/syrup/syrup/parallel'
cp: cannot stat 'glucose-syrup_release': No such file or directory
make: *** [makefile:2: all] Error 1
./lls -b 8 8 -p 3 -x 2 -y 1 -i --force_at_most 5 -r pB2ac/S -v 3
A for awesome wrote:Do you know why this search input is returning unsatisfiable? I'm attempting to rediscover the 2c/3 you posted on the 5S thread:Code: Select all./lls -b 8 8 -p 3 -x 2 -y 1 -i --force_at_most 5 -r pB2ac/S -v 3
Pardon me if I'm overlooking something obvious.
77topaz wrote:A for awesome wrote:Do you know why this search input is returning unsatisfiable? I'm attempting to rediscover the 2c/3 you posted on the 5S thread:Code: Select all./lls -b 8 8 -p 3 -x 2 -y 1 -i --force_at_most 5 -r pB2ac/S -v 3
Pardon me if I'm overlooking something obvious.
It might be that the force_at_most parameter is clashing with the phases of the (2,1)c/3 ship that have more than 5 cells? I'm not completely sure if the force_at_most parameter is supposed to apply to all phases or just the first one, though.
A for awesome wrote:Do you know why this search input is returning unsatisfiable? I'm attempting to rediscover the 2c/3 you posted on the 5S thread:Code: Select all./lls -b 8 8 -p 3 -x 2 -y 1 -i --force_at_most 5 -r pB2ac/S -v 3
Pardon me if I'm overlooking something obvious.
Rhombic wrote:After seeing you have submitted absolutely amazing results in the OCA spaceship thread, I'm guessing that LLS now handles non-totalistic rules too.
A for awesome wrote:Do you know why this search input is returning unsatisfiable? I'm attempting to rediscover the 2c/3 you posted on the 5S thread:Code: Select all./lls -b 8 8 -p 3 -x 2 -y 1 -i --force_at_most 5 -r pB2ac/S -v 3
77topaz wrote:It might be that the force_at_most parameter is clashing with the phases of the (2,1)c/3 ship that have more than 5 cells? I'm not completely sure if the force_at_most parameter is supposed to apply to all phases or just the first one, though.
BlinkerSpawn wrote:Fairly certain "-r pB2ac/S" disallows everything that isn't B2, from looking at the descriptions.
-r B2e3aceij5-ijr/S23-a4
-r pB1-c2345678/S012345678
--force_at_least 30 0 1 2
--force_at_most 0 -1
AforAmpere wrote:Has anyone compiled this for Cygwin or Windows? If so, can you upload the compiled glucose-sugar file?
Making dependencies
Depends on: simp
Compiling: /LLS/solvers/syrup/parallel/Main.or
/LLS/solvers/syrup/parallel/Main.cc:53:18: fatal error: zlib.h: No such file or directory
/LLS/solvers/syrup/parallel/../core/Solver.cc:326:47: error: ‘putc_unlocked’ was not declared in this scope
if(putc_unlocked((int) ch, certifiedOutput) == EOF)
Rhombic wrote:Can't seem to compile syrup (from syrup.zip)
Traceback (most recent call last):
File "./lls", line 199, in <module>
indent = indent, verbosity = verbosity
File "/Python/logic-life-search-master/LLS.py", line 61, in preprocess_solve_and_postprocess
indent = indent, verbosity = verbosity
File "/Python/logic-life-search-master/LLS.py", line 175, in preprocess_and_solve
indent = indent, verbosity = verbosity)
File "/Python/logic-life-search-master/LLS.py", line 246, in solve
DIMACS_string, solver=solver, parameters=parameters, timeout=timeout, save_dimacs = save_dimacs, dry_run = dry_run, indent = indent + 1, verbosity = verbosity)
File "/Python/logic-life-search-master/LLS_SAT_solvers.py", line 48, in SAT_solve
solution, time_taken = use_solver(solver, dimacs_file, parameters = parameters, timeout = timeout, indent = indent, verbosity = verbosity)
File "/Python/logic-life-search-master/LLS_SAT_solvers.py", line 84, in use_solver
stdout=subprocess.PIPE, stdin=subprocess.PIPE, stderr=subprocess.PIPE)
File "/usr/lib/python2.7/subprocess.py", line 390, in __init__
errread, errwrite)
File "/usr/lib/python2.7/subprocess.py", line 1025, in _execute_child
raise child_exception
OSError: [Errno 8] Exec format error
./lls -m -b 16 6 -p 3 -x 0 -y 1
rokicki wrote:Here's a just slightly more complex command line that returns a c/3 spaceship in under 10 seconds.Code: Select all./lls -m -b 16 6 -p 3 -x 0 -y 1
calcyman wrote:You'll need to run git checkout cad98 since the latest version of the repo is missing all of the code which should be in src.
Macbi wrote:calcyman wrote:You'll need to run git checkout cad98 since the latest version of the repo is missing all of the code which should be in src.
I fixed it. I think.
local g = golly()
local FALSE = 1000000000
local TRUE = -FALSE
local a = {}
g.show("Getting pattern from Golly . . .")
g.update()
local r = g.getrect()
local w = r[3] + 2
local h = r[4] + 2
local cells = g.getcells(r)
local oncells = {}
for ci=1,#cells,2 do
oncells[(cells[ci]-r[1]+1) .. " " .. (cells[ci+1]-r[2]+1)] = 1
end
g.show("Writing DIMACS-format CNF file . . .")
g.update()
local F = assert(io.open("t.cnf", "w"), "Can't write to t.cnf")
F:write("p cnf 1 1\n")
local inputbase = 1
local outputbase = 1 + w * h
local nextvar = 1 + 2 * w * h
function input(x, y)
if x < 0 or y < 0 or x >= w or y >= h then
return FALSE
else
return x + y * w + inputbase
end
end
function output(x, y)
if x < 0 or y < 0 or x >= w or y >= h then
return FALSE
else
return x + y * w + outputbase
end
end
function inputassum(x, y)
local t = input(x, y)
if t == FALSE then
return {FALSE, 0, 0}
else
return {t, 1, 1}
end
end
function getoff(a, v)
if v == 0 or v < a[2] then
return TRUE
elseif v > a[3] then
return FALSE
else
return a[1] + v - a[2]
end
end
function n(v)
return - v
end
function truity(v)
return v == TRUE
end
function notfalsity(v)
return v ~= FALSE and v ~= 0
end
function emit(a, b, c)
if not truity(a) and not truity(b) and not truity(c) then
if notfalsity(a) then F:write(" ", a) end
if notfalsity(b) then F:write(" ", b) end
if notfalsity(c) then F:write(" ", c) end
F:write(" 0\n")
end
end
function sum4(a, b, min, max)
if b[1] == FALSE then return a end
if a[1] == FALSE then return b end
if min == 0 then min = 1 end
if max == 0 then max = a[3] + b[3] end
local base = nextvar
nextvar = nextvar + max - min + 1
local r = {base, min, max}
for av=0, a[3] do
for bv=0, b[3] do
local s = av + bv
if s >= min and s <= max then
emit(n(getoff(a, av)), n(getoff(b, bv)), getoff(r, s))
end
end
end
for av=1, 1+a[3] do
for bv=1, 1+b[3] do
local s = av + bv - 1
if s >= min and s <= max then
emit(getoff(a, av), getoff(b, bv), n(getoff(r, s)))
end
end
end
return r
end
function sum(a, b)
return sum4(a, b, 0, 0)
end
local cache = {}
function getv2(x, y)
local key = "v2 " .. x .. " " .. y
if cache[key] == nil then
cache[key] = sum(inputassum(x, y), inputassum(x, y+1))
end
return cache[key]
end
function geth2(x, y)
local key = "h2 " .. x .. " " .. y
if cache[key] == nil then
cache[key] = sum(inputassum(x, y), inputassum(x+1, y))
end
return cache[key]
end
function geth4(x, y)
local key = "h4 " .. x .. " " .. y
if cache[key] == nil then
cache[key] = sum(geth2(x, y), geth2(x, y+2))
end
return cache[key]
end
function calc(x, y)
local z0 = input(x, y)
local z1 = output(x, y)
local xd = x - x % 2
local yd = y - y % 2
local xo = 3 * x - 2 * xd - 1
local yo = 3 * y - 2 * yd - 1
local xm = 2 * x - xo
local h4 = geth4(xd, y-1)
local v2 = getv2(xo, yd)
local s = sum4(h4, sum(v2, sum(inputassum(xm, y), inputassum(xo, yo))), 2, 4)
emit(n(getoff(s, 4)), 0, n(z1))
emit(getoff(s, 2), 0, n(z1))
emit(getoff(s, 3), z0, n(z1))
emit(n(getoff(s, 3)), getoff(s, 4), z1)
local xx = nextvar
nextvar = nextvar + 1
emit(n(getoff(s, 2)), getoff(s, 4), xx)
emit(n(xx), n(z0), z1)
end
for y=0, h-1 do
for x=0, w-1 do
calc(x, y)
end
end
for x=0, w-3 do
emit(n(input(x, 0)), n(input(x+1, 0)), n(input(x+2, 0)))
emit(n(input(x, h-1)), n(input(x+1, h-1)), n(input(x+2, h-1)))
end
for y=0, h-3 do
emit(n(input(0, y)), n(input(0, y+1)), n(input(0, y+2)))
emit(n(input(w-1, y)), n(input(w-1, y+1)), n(input(w-1, y+2)))
end
for y=0, h-1 do
for x=0, w-1 do
if oncells[x .. " " .. y] then
F:write(" ", output(x, y), " 0\n")
else
F:write(" ", n(output(x, y)), " 0\n")
end
end
end
F:close()
g.show("Running glucose . . .")
g.update()
os.execute("./glucose t.cnf t.res")
F = assert(io.open("t.res", "r"), "Can't read t.res")
local sawresult = false
for line in F:lines() do
if string.sub(line, 1, 3) ~= "UNS" then
g.show("Sending result back to Golly . . .")
g.update()
local toks = {}
for tok in line:gmatch("[^%s]+") do
table.insert(toks, tok)
end
for y=0, h-1 do
for x=0, w-1 do
if (tonumber(toks[input(x, y)]) < 0) then
g.setcell(x+r[1]-1, y+r[2]-1, 0)
else
g.setcell(x+r[1]-1, y+r[2]-1, 1)
end
end
end
sawresult = true
end
end
if not sawresult then
g.show("No predecessor.")
g.update()
else
g.setgen(-1+tonumber(g.getgen()))
g.show("Finished.")
g.update()
end
Users browsing this forum: No registered users and 1 guest