Skip to content

Instantly share code, notes, and snippets.

@antimon2

antimon2/Project.toml

Created March 8, 2024 10:48
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save antimon2/9c0ee88952fe85bc2b0b9ed95e0e8b9c to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save antimon2/9c0ee88952fe85bc2b0b9ed95e0e8b9c to your computer and use it in GitHub Desktop.
Download ZIP
solve_3sat_by_regex.jl.ipynb
Raw
Project.toml
[compat]
julia = "1.6"
Display the source blob
Display the rendered blob
Raw
solve_3sat_by_regex.jl.ipynb
{
"cells": [
{
"metadata": {
"ExecuteTime": {
"end_time": "2024-03-08T19:45:52.263000+09:00",
"start_time": "2024-03-08T10:45:50.621Z"
},
"trusted": false
},
"id": "53fb30b0",
"cell_type": "code",
"source": "versioninfo()",
"execution_count": 1,
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": "Julia Version 1.10.2\nCommit bd47eca2c8a (2024-03-01 10:14 UTC)\nBuild Info:\n Official https://julialang.org/ release\nPlatform Info:\n OS: Linux (x86_64-linux-gnu)\n CPU: 12 × Intel(R) Core(TM) i7-9750H CPU @ 2.60GHz\n WORD_SIZE: 64\n LIBM: libopenlibm\n LLVM: libLLVM-15.0.7 (ORCJIT, skylake)\nThreads: 1 default, 0 interactive, 1 GC (on 12 virtual cores)\n"
}
]
},
{
"metadata": {},
"cell_type": "markdown",
"source": "ref(original): [https://perl.plover.com/NPC/NPC-3SAT.html](https://perl.plover.com/NPC/NPC-3SAT.html) \n(ref: [https://twitter.com/abap34/status/1766004781393547633](https://twitter.com/abap34/status/1766004781393547633))"
},
{
"metadata": {
"ExecuteTime": {
"end_time": "2024-03-08T19:45:52.613000+09:00",
"start_time": "2024-03-08T10:45:50.624Z"
},
"trusted": false
},
"id": "c89de6b9",
"cell_type": "code",
"source": "mk_string(n, m) = 'x'^n * ';' * \"x,\"^m",
"execution_count": 2,
"outputs": [
{
"data": {
"text/plain": "mk_string (generic function with 1 method)"
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
]
},
{
"metadata": {
"ExecuteTime": {
"end_time": "2024-03-08T19:45:52.951000+09:00",
"start_time": "2024-03-08T10:45:50.627Z"
},
"trusted": false
},
"id": "13ba1a6b",
"cell_type": "code",
"source": "mk_string(3, 4)",
"execution_count": 3,
"outputs": [
{
"data": {
"text/plain": "\"xxx;x,x,x,x,\""
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
]
},
{
"metadata": {
"ExecuteTime": {
"end_time": "2024-03-08T19:45:52.961000+09:00",
"start_time": "2024-03-08T10:45:50.629Z"
},
"trusted": false
},
"id": "6a36f52f",
"cell_type": "code",
"source": "function mk_pattern(n, clauses)\n iobuf = IOBuffer()\n print(iobuf, '^')\n for _=1:n\n print(iobuf, \"(x?)\")\n end\n print(iobuf, \".*;\")\n for idxs in clauses\n print(iobuf, \"(?:\")\n print(iobuf, join(map(idxs) do n\n n < 0 ? \"\\\\$(-n)x\" : \"\\\\$n\"\n end, '|'))\n print(iobuf, \"),\")\n end\n return String(take!(iobuf))\nend",
"execution_count": 4,
"outputs": [
{
"data": {
"text/plain": "mk_pattern (generic function with 1 method)"
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
]
},
{
"metadata": {
"ExecuteTime": {
"end_time": "2024-03-08T19:45:52.996000+09:00",
"start_time": "2024-03-08T10:45:50.630Z"
},
"trusted": false
},
"id": "cacd9ef3",
"cell_type": "code",
"source": "mk_pattern(3, [(1,2,-3), (1,-2,3), (-1,-2,3), (-1,-2,-3)])",
"execution_count": 5,
"outputs": [
{
"data": {
"text/plain": "\"^(x?)(x?)(x?).*;(?:\\\\1|\\\\2|\\\\3x),(?:\\\\1|\\\\2x|\\\\3),(?:\\\\1x|\\\\2x|\\\\3),(?:\\\\1x|\\\\2x|\\\\3x),\""
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
]
},
{
"metadata": {
"ExecuteTime": {
"end_time": "2024-03-08T19:45:53.004000+09:00",
"start_time": "2024-03-08T10:45:50.632Z"
},
"trusted": false
},
"id": "e8124405",
"cell_type": "code",
"source": "function solve_3sat(N, clauses)\n _string = mk_string(N, length(clauses))\n _rex = Regex(mk_pattern(N, clauses))\n occursin(_rex, _string)\nend",
"execution_count": 6,
"outputs": [
{
"data": {
"text/plain": "solve_3sat (generic function with 1 method)"
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
]
},
{
"metadata": {
"ExecuteTime": {
"end_time": "2024-03-08T19:45:53.117000+09:00",
"start_time": "2024-03-08T10:45:50.636Z"
},
"trusted": false
},
"id": "fa308210",
"cell_type": "code",
"source": "solve_3sat(3, [(1,2,-3), (1,-2,3), (-1,-2,3), (-1,-2,-3)])",
"execution_count": 7,
"outputs": [
{
"data": {
"text/plain": "true"
},
"execution_count": 7,
"metadata": {},
"output_type": "execute_result"
}
]
},
{
"metadata": {
"ExecuteTime": {
"end_time": "2024-03-08T19:45:53.118000+09:00",
"start_time": "2024-03-08T10:45:50.640Z"
},
"trusted": false
},
"id": "880bff6e",
"cell_type": "code",
"source": "solve_3sat(4, [\n (1, 2, 3),\n (4, 2, -3),\n (-1, 4, 3),\n (-1, -4, 2),\n (-4, -2, 3),\n (-1, -2, -3),\n (1, -4, -3),\n# (1, 4, -2),\n])",
"execution_count": 8,
"outputs": [
{
"data": {
"text/plain": "true"
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
]
},
{
"metadata": {
"ExecuteTime": {
"end_time": "2024-03-08T19:45:53.119000+09:00",
"start_time": "2024-03-08T10:45:50.642Z"
},
"trusted": false
},
"id": "e9311aeb",
"cell_type": "code",
"source": "solve_3sat(4, [\n (1, 2, 3),\n (4, 2, -3),\n (-1, 4, 3),\n (-1, -4, 2),\n (-4, -2, 3),\n (-1, -2, -3),\n (1, -4, -3),\n (1, 4, -2),\n])",
"execution_count": 9,
"outputs": [
{
"data": {
"text/plain": "false"
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
]
},
{
"metadata": {
"trusted": false
},
"id": "eca199b2",
"cell_type": "code",
"source": "",
"execution_count": null,
"outputs": []
}
],
"metadata": {
"kernelspec": {
"name": "julia-1.10",
"display_name": "Julia 1.10.2",
"language": "julia"
},
"language_info": {
"file_extension": ".jl",
"name": "julia",
"mimetype": "application/julia",
"version": "1.10.2"
},
"gist": {
"id": "",
"data": {
"description": "solve_3sat_by_regex.jl.ipynb",
"public": true
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment