Spaces:
Running
Running
| <html lang="en"> | |
| <head> | |
| <meta charset="UTF-8"> | |
| <meta name="viewport" content="width=device-width, initial-scale=1.0"> | |
| <title>Elixir DPLL: Interactive Logic Solver</title> | |
| <script src="https://cdn.tailwindcss.com"></script> | |
| <link rel="preconnect" href="https://fonts.googleapis.com"> | |
| <link rel="preconnect" href="https://fonts.gstatic.com" crossorigin> | |
| <link href="https://fonts.googleapis.com/css2?family=Fira+Code:wght@300;400;600&family=Inter:wght@300;400;600;800&family=JetBrains+Mono:wght@400;700&display=swap" rel="stylesheet"> | |
| <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/styles/atom-one-dark.min.css"> | |
| <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/highlight.min.js"></script> | |
| <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/languages/elixir.min.js"></script> | |
| <style> | |
| :root { | |
| --primary: #6366f1; | |
| --accent: #a78bfa; | |
| --success: #34d399; | |
| --danger: #f472b6; | |
| --bg-dark: #0f0f1a; | |
| --bg-panel: #161627; | |
| --bg-code: #1e1e2e; | |
| --border: #2a2a3c; | |
| --text-primary: #e2e8f0; | |
| --text-secondary: #94a3b8; | |
| --neon-glow: 0 0 20px rgba(99, 102, 241, 0.3); | |
| } | |
| body { | |
| font-family: 'Inter', sans-serif; | |
| background: var(--bg-dark); | |
| color: var(--text-primary); | |
| overflow-x: hidden; | |
| } | |
| .font-mono { font-family: 'Fira Code', monospace; } | |
| .font-code { font-family: 'JetBrains Mono', monospace; } | |
| /* Aurora Background */ | |
| .aurora { | |
| position: fixed; | |
| top: 0; left: 0; width: 100%; height: 100%; | |
| z-index: -1; | |
| overflow: hidden; | |
| } | |
| .aurora-blob { | |
| position: absolute; | |
| border-radius: 50%; | |
| filter: blur(80px); | |
| opacity: 0.4; | |
| animation: drift 20s infinite alternate; | |
| } | |
| .blob-1 { width: 600px; height: 600px; background: #6366f1; top: -10%; left: -10%; animation-delay: 0s; } | |
| .blob-2 { width: 500px; height: 500px; background: #ec4899; top: 40%; right: -10%; animation-delay: -5s; } | |
| .blob-3 { width: 400px; height: 400px; background: #06b6d4; bottom: -10%; left: 40%; animation-delay: -10s; } | |
| @keyframes drift { | |
| 0% { transform: translate(0, 0) scale(1); } | |
| 100% { transform: translate(50px, -50px) scale(1.1); } | |
| } | |
| /* Glassmorphism Panel */ | |
| .glass-panel { | |
| background: rgba(22, 22, 39, 0.7); | |
| backdrop-filter: blur(12px); | |
| -webkit-backdrop-filter: blur(12px); | |
| border: 1px solid rgba(255, 255, 255, 0.08); | |
| box-shadow: 0 8px 32px rgba(0, 0, 0, 0.3); | |
| border-radius: 1rem; | |
| } | |
| /* Custom Scrollbar */ | |
| ::-webkit-scrollbar { width: 8px; height: 8px; } | |
| ::-webkit-scrollbar-track { background: var(--bg-dark); } | |
| ::-webkit-scrollbar-thumb { background: var(--border); border-radius: 4px; } | |
| ::-webkit-scrollbar-thumb:hover { background: var(--primary); } | |
| /* Node Animations */ | |
| .node-enter { | |
| animation: popIn 0.4s cubic-bezier(0.175, 0.885, 0.32, 1.275) forwards; | |
| opacity: 0; | |
| transform: scale(0); | |
| } | |
| @keyframes popIn { | |
| to { opacity: 1; transform: scale(1); } | |
| } | |
| .edge-path { | |
| stroke-dasharray: 1000; | |
| stroke-dashoffset: 1000; | |
| animation: drawLine 1s ease-out forwards; | |
| } | |
| @keyframes drawLine { | |
| to { stroke-dashoffset: 0; } | |
| } | |
| /* Syntax Highlighting Overrides */ | |
| .hljs { background: transparent ; padding: 0 ; } | |
| /* Input styling */ | |
| .logic-input { | |
| background: var(--bg-code); | |
| border: 1px solid var(--border); | |
| transition: all 0.3s ease; | |
| } | |
| .logic-input:focus { | |
| border-color: var(--primary); | |
| box-shadow: 0 0 0 3px rgba(99, 102, 241, 0.2); | |
| outline: none; | |
| } | |
| /* Button effects */ | |
| .btn-glow { | |
| position: relative; | |
| overflow: hidden; | |
| transition: all 0.3s; | |
| } | |
| .btn-glow:hover { | |
| box-shadow: var(--neon-glow); | |
| transform: translateY(-1px); | |
| } | |
| .btn-glow::after { | |
| content: ''; | |
| position: absolute; | |
| top: -50%; left: -50%; width: 200%; height: 200%; | |
| background: linear-gradient(45deg, transparent, rgba(255,255,255,0.1), transparent); | |
| transform: rotate(45deg) translateY(-100%); | |
| transition: transform 0.6s; | |
| } | |
| .btn-glow:hover::after { | |
| transform: rotate(45deg) translateY(100%); | |
| } | |
| /* Tree Canvas Container */ | |
| #tree-container { | |
| cursor: grab; | |
| } | |
| #tree-container:active { | |
| cursor: grabbing; | |
| } | |
| /* Tooltip */ | |
| .tooltip { | |
| visibility: hidden; | |
| opacity: 0; | |
| transition: opacity 0.2s; | |
| } | |
| .has-tooltip:hover .tooltip { | |
| visibility: visible; | |
| opacity: 1; | |
| } | |
| </style> | |
| </head> | |
| <body class="min-h-screen flex flex-col"> | |
| <!-- Background Effects --> | |
| <div class="aurora"> | |
| <div class="aurora-blob blob-1"></div> | |
| <div class="aurora-blob blob-2"></div> | |
| <div class="aurora-blob blob-3"></div> | |
| </div> | |
| <!-- Header --> | |
| <header class="w-full border-b border-white/5 bg-[#0f0f1a]/80 backdrop-blur-md sticky top-0 z-50"> | |
| <div class="max-w-7xl mx-auto px-4 h-16 flex items-center justify-between"> | |
| <div class="flex items-center gap-3"> | |
| <div class="w-8 h-8 rounded-lg bg-gradient-to-br from-indigo-500 to-purple-600 flex items-center justify-center font-bold text-white">E</div> | |
| <h1 class="text-lg font-semibold tracking-tight text-white">DPLL <span class="text-indigo-400 font-light">Visualizer</span></h1> | |
| </div> | |
| <div class="flex items-center gap-4 text-sm text-slate-400"> | |
| <a href="https://huggingface.co/spaces/akhaliq/anycoder" target="_blank" class="hover:text-indigo-400 transition-colors flex items-center gap-2"> | |
| <span class="bg-indigo-500/10 text-indigo-400 px-2 py-1 rounded text-xs font-mono">Built with anycoder</span> | |
| </a> | |
| </div> | |
| </div> | |
| </header> | |
| <!-- Main Content --> | |
| <main class="flex-1 w-full max-w-7xl mx-auto p-4 md:p-6 grid grid-cols-1 lg:grid-cols-12 gap-6"> | |
| <!-- Left Panel: Input & Controls --> | |
| <div class="lg:col-span-4 space-y-6 flex flex-col"> | |
| <!-- Input Section --> | |
| <div class="glass-panel p-5 space-y-4"> | |
| <div class="flex items-center justify-between"> | |
| <h2 class="text-sm font-semibold text-indigo-300 uppercase tracking-wider flex items-center gap-2"> | |
| <svg class="w-4 h-4" fill="none" stroke="currentColor" viewBox="0 0 24 24"><path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M9 12h6m-6 4h6m2 5H7a2 2 0 01-2-2V5a2 2 0 012-2h5.586a1 1 0 01.707.293l5.414 5.414a1 1 0 01.293.707V19a2 2 0 01-2 2z"></path></svg> | |
| Logic Formula (CNF) | |
| </h2> | |
| <div class="has-tooltip relative"> | |
| <span class="tooltip absolute bottom-full left-1/2 -translate-x-1/2 mb-2 px-2 py-1 bg-black text-xs text-white rounded whitespace-nowrap">Format: (a || !b) && (!a || c)</span> | |
| <button id="info-btn" class="text-slate-500 hover:text-white transition-colors"> | |
| <svg class="w-4 h-4" fill="none" stroke="currentColor" viewBox="0 0 24 24"><path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M13 16h-1v-4h-1m1-4h.01M21 12a9 9 0 11-18 0 9 9 0 0118 0z"></path></svg> | |
| </button> | |
| </div> | |
| </div> | |
| <textarea id="formula-input" class="logic-input w-full h-32 p-4 rounded-lg font-code text-sm text-emerald-300 resize-none" spellcheck="false" placeholder="Enter CNF formula...">(a || !b) && (!a || c) && (b || !c) && (!a || !c)</textarea> | |
| <div class="flex gap-2"> | |
| <button onclick="app.reset()" class="flex-1 btn-glow px-4 py-2 rounded-lg bg-white/5 hover:bg-white/10 text-sm font-medium text-slate-300 border border-white/10">Reset</button> | |
| <button onclick="app.solve()" class="flex-1 btn-glow px-4 py-2 rounded-lg bg-gradient-to-r from-indigo-600 to-purple-600 text-sm font-bold text-white shadow-lg shadow-indigo-900/20"> | |
| Run DPLL | |
| </button> | |
| </div> | |
| <div class="grid grid-cols-2 gap-2"> | |
| <button onclick="app.loadExample(1)" class="px-3 py-2 rounded bg-white/5 hover:bg-white/10 text-xs text-slate-400 transition border border-white/5">Simple SAT</button> | |
| <button onclick="app.loadExample(2)" class="px-3 py-2 rounded bg-white/5 hover:bg-white/10 text-xs text-slate-400 transition border border-white/5">UNSAT</button> | |
| <button onclick="app.loadExample(3)" class="px-3 py-2 rounded bg-white/5 hover:bg-white/10 text-xs text-slate-400 transition border border-white/5">Complex</button> | |
| <button onclick="app.loadExample(4)" class="px-3 py-2 rounded bg-white/5 hover:bg-white/10 text-xs text-slate-400 transition border border-white/5">4 Queens</button> | |
| </div> | |
| </div> | |
| <!-- Speed Control --> | |
| <div class="glass-panel p-5"> | |
| <div class="flex justify-between items-center mb-2"> | |
| <span class="text-xs font-medium text-slate-400">Animation Speed</span> | |
| <span id="speed-val" class="text-xs font-mono text-indigo-400">1x</span> | |
| </div> | |
| <input type="range" id="speed-slider" min="1" max="5" step="1" value="2" class="w-full h-1 bg-slate-700 rounded-lg appearance-none cursor-pointer accent-indigo-500"> | |
| </div> | |
| <!-- Elixir Code Preview --> | |
| <div class="glass-panel p-5 flex-1 flex flex-col min-h-[300px]"> | |
| <h2 class="text-sm font-semibold text-purple-300 uppercase tracking-wider mb-3 flex items-center gap-2"> | |
| <svg class="w-4 h-4" fill="none" stroke="currentColor" viewBox="0 0 24 24"><path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M10 20l4-16m4 4l4 4-4 4M6 16l-4-4 4-4"></path></svg> | |
| Elixir Implementation | |
| </h2> | |
| <div class="relative flex-1 bg-[#1e1e2e] rounded-lg border border-white/5 overflow-hidden group"> | |
| <button onclick="app.copyCode()" class="absolute top-2 right-2 p-1.5 rounded bg-white/5 hover:bg-white/10 opacity-0 group-hover:opacity-100 transition z-10 text-xs text-slate-400"> | |
| Copy | |
| </button> | |
| <pre class="h-full overflow-auto p-4 text-xs"><code class="language-elixir" id="elixir-code"> | |
| defmodule DpllSolver do | |
| @moduledoc """ | |
| A pure functional implementation of the DPLL algorithm. | |
| """ | |
| @spec solve([[integer]]) :: {:sat, map} | :unsat | |
| def solve(clauses) do | |
| case dpll(clauses, %{}) do | |
| {:sat, model} -> {:sat, model} | |
| :unsat -> :unsat | |
| end | |
| end | |
| defp dpll(clauses, model) do | |
| cond do | |
| # Check for empty clauses (conflict) | |
| Enum.any?(clauses, &(&1 == [])) -> :unsat | |
| # Check if all clauses are satisfied | |
| clauses == [] -> {:sat, model} | |
| true -> | |
| # 1. Unit Propagation | |
| case find_unit_clause(clauses) do | |
| nil -> | |
| # 2. Pure Literal Elimination | |
| case find_pure_literal(clauses) do | |
| nil -> | |
| # 3. Branching (Splitting) | |
| var = choose_variable(clauses) | |
| case dpll(assign(clauses, var, true), Map.put(model, var, true)) do | |
| {:sat, m} -> {:sat, m} | |
| :unsat -> dpll(assign(clauses, var, false), Map.put(model, var, false)) | |
| end | |
| lit -> | |
| dpll(assign(clauses, lit, true), Map.put(model, lit, true)) | |
| end | |
| lit -> | |
| dpll(assign(clauses, lit, true), Map.put(model, lit, true)) | |
| end | |
| end | |
| end | |
| defp assign(clauses, lit, val) do | |
| # Returns new clauses with lit satisfied and !lit removed | |
| Enum.map(clauses, fn clause -> | |
| cond do | |
| lit in clause -> :removed | |
| -lit in clause -> List.delete(clause, -lit) | |
| true -> clause | |
| end | |
| end) | |
| |> Enum.reject(&(&1 == :removed)) | |
| end | |
| defp find_unit_clause(clauses) do | |
| Enum.find_value(clauses, fn | |
| [lit] -> lit | |
| _ -> nil | |
| end) | |
| end | |
| defp find_pure_literal(clauses) do | |
| all_lits = List.flatten(clauses) | |
| Enum.find_value(all_lits, fn lit -> | |
| if (-lit) not in all_lits, do: lit, else: nil | |
| end) | |
| end | |
| defp choose_variable(clauses) do | |
| List.flatten(clauses) |> hd |> abs | |
| end | |
| end | |
| </code></pre> | |
| </div> | |
| </div> | |
| </div> | |
| <!-- Middle: Visualization --> | |
| <div class="lg:col-span-5 flex flex-col h-[600px] lg:h-auto glass-panel relative overflow-hidden"> | |
| <div class="absolute top-4 left-4 z-10 flex gap-2"> | |
| <div class="bg-black/40 backdrop-blur px-3 py-1 rounded-full border border-white/10 text-xs text-slate-300 flex items-center gap-2"> | |
| <span class="w-2 h-2 rounded-full bg-emerald-400"></span> SAT Path | |
| </div> | |
| <div class="bg-black/40 backdrop-blur px-3 py-1 rounded-full border border-white/10 text-xs text-slate-300 flex items-center gap-2"> | |
| <span class="w-2 h-2 rounded-full bg-rose-500"></span> UNSAT Branch | |
| </div> | |
| </div> | |
| <div id="tree-container" class="w-full h-full relative overflow-hidden bg-gradient-to-b from-[#0f0f1a] to-[#131325]"> | |
| <!-- SVG Tree will be rendered here --> | |
| <svg id="tree-svg" class="w-full h-full absolute top-0 left-0 origin-top"></svg> | |
| <div id="node-layer" class="absolute top-0 left-0 w-full h-full pointer-events-none"></div> | |
| <div id="start-msg" class="absolute inset-0 flex items-center justify-center text-slate-600"> | |
| <div class="text-center"> | |
| <svg class="w-12 h-12 mx-auto mb-3 opacity-50" fill="none" stroke="currentColor" viewBox="0 0 24 24"><path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M14.752 11.168l-3.197-2.132A1 1 0 0010 9.87v4.263a1 1 0 001.555.832l3.197-2.132a1 1 0 000-1.664z"></path><path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M21 12a9 9 0 11-18 0 9 9 0 0118 0z"></path></svg> | |
| <p class="font-mono text-sm">Click "Run DPLL" to start visualization</p> | |
| </div> | |
| </div> | |
| </div> | |
| </div> | |
| <!-- Right Panel: Logs & Status --> | |
| <div class="lg:col-span-3 space-y-6 flex flex-col"> | |
| <!-- Status Panel --> | |
| <div class="glass-panel p-5"> | |
| <h2 class="text-sm font-semibold text-emerald-300 uppercase tracking-wider mb-4">System Status</h2> | |
| <div class="space-y-3"> | |
| <div class="flex justify-between items-center"> | |
| <span class="text-xs text-slate-400">Result</span> | |
| <span id="result-badge" class="px-2 py-0.5 rounded text-xs font-bold bg-slate-700 text-slate-300">--</span> | |
| </div> | |
| <div class="flex justify-between items-center"> | |
| <span class="text-xs text-slate-400">Variables</span> | |
| <span id="var-count" class="font-mono text-sm text-white">0</span> | |
| </div> | |
| <div class="flex justify-between items-center"> | |
| <span class="text-xs text-slate-400">Clauses</span> | |
| <span id="clause-count" class="font-mono text-sm text-white">0</span> | |
| </div> | |
| <div class="flex justify-between items-center"> | |
| <span class="text-xs text-slate-400">Decisions</span> | |
| <span id="decision-count" class="font-mono text-sm text-white">0</span> | |
| </div> | |
| </div> | |
| </div> | |
| <!-- Unit Propagation Log --> | |
| <div class="glass-panel p-5 flex-1 flex flex-col min-h-[250px]"> | |
| <h2 class="text-sm font-semibold text-amber-300 uppercase tracking-wider mb-3 flex items-center gap-2"> | |
| <svg class="w-4 h-4" fill="none" stroke="currentColor" viewBox="0 0 24 24"><path stroke-linecap="round" stroke-linejoin="round" stroke-width="2" d="M13 10V3L4 14h7v7l9-11h-7z"></path></svg> | |
| Inference Log | |
| </h2> | |
| <div id="inference-log" class="flex-1 overflow-y-auto font-mono text-xs space-y-2 pr-2"> | |
| <div class="text-slate-600 italic">Waiting for execution...</div> | |
| </div> | |
| </div> | |
| <!-- Assignment Table --> | |
| <div class="glass-panel p-5"> | |
| <h2 class="text-sm font-semibold text-blue-300 uppercase tracking-wider mb-3">Final Assignment</h2> | |
| <div id="assignment-grid" class="grid grid-cols-4 gap-2"> | |
| <!-- Dynamic assignments --> | |
| <div class="col-span-4 text-center text-xs text-slate-600 py-2">No solution yet</div> | |
| </div> | |
| </div> | |
| </div> | |
| </main> | |
| <script> | |
| /** | |
| * DPLL Logic Solver & Visualizer | |
| * Implements the DPLL algorithm with step-by-step visualization. | |
| */ | |
| class DPLLVisualizer { | |
| constructor() { | |
| this.svg = document.getElementById('tree-svg'); | |
| this.nodeLayer = document.getElementById('node-layer'); | |
| this.logContainer = document.getElementById('inference-log'); | |
| this.assignmentGrid = document.getElementById('assignment-grid'); | |
| this.speedSlider = document.getElementById('speed-slider'); | |
| this.speedVal = document.getElementById('speed-val'); | |
| this.speed = 2; | |
| this.isRunning = false; | |
| this.treeData = null; | |
| this.currentNodes = []; | |
| this.idCounter = 0; | |
| this.scale = 1; | |
| this.translateX = 0; | |
| this.translateY = 0; | |
| // Bind UI events | |
| this.speedSlider.addEventListener('input', (e) => { | |
| this.speed = parseInt(e.target.value); | |
| this.speedVal.textContent = this.speed + 'x'; | |
| }); | |
| // Pan/Zoom listeners for SVG | |
| this.setupPanZoom(); | |
| // HighlightJS | |
| hljs.highlightAll(); | |
| } | |
| setupPanZoom() { | |
| const container = document.getElementById('tree-container'); | |
| let isDragging = false; | |
| let startX, startY; | |
| container.addEventListener('mousedown', (e) => { | |
| isDragging = true; | |
| startX = e.clientX - this.translateX; | |
| startY = e.clientY - this.translateY; | |
| }); | |
| window.addEventListener('mousemove', (e) => { | |
| if (!isDragging) return; | |
| this.translateX = e.clientX - startX; | |
| this.translateY = e.clientY - startY; | |
| this.updateTransform(); | |
| }); | |
| window.addEventListener('mouseup', () => isDragging = false); | |
| container.addEventListener('wheel', (e) => { | |
| e.preventDefault(); | |
| const delta = e.deltaY > 0 ? 0.9 : 1.1; | |
| this.scale *= delta; | |
| this.updateTransform(); | |
| }); | |
| } | |
| updateTransform() { | |
| const transform = `translate(${this.translateX}px, ${this.translateY}px) scale(${this.scale})`; | |
| this.svg.style.transform = transform; | |
| this.nodeLayer.style.transform = transform; | |
| } | |
| resetView() { | |
| this.scale = 1; | |
| this.translateX = 0; | |
| this.translateY = 0; | |
| this.updateTransform(); | |
| } | |
| // --- Logic Parsing --- | |
| parseFormula(input) { | |
| // Remove whitespace | |
| let clean = input.replace(/\s+/g, ''); | |
| // Replace operators | |
| clean = clean.replace(/\|\|/g, ' OR '); | |
| clean = clean.replace(/&&/g, ' AND '); | |
| clean = clean.replace(/!/g, ' NOT '); | |
| // Extract clauses between () | |
| const clauses = []; | |
| const regex = /\(([^)]+)\)/g; | |
| let match; | |
| while ((match = regex.exec(clean)) !== null) { | |
| clauses.push(match[1]); | |
| } | |
| if (clauses.length === 0) throw new Error("Invalid format. Use (a || !b) && (c)"); | |
| // Map variables to integers | |
| const varMap = {}; | |
| let nextVar = 1; | |
| const getVar = (name) => { | |
| if (!varMap[name]) varMap[name] = nextVar++; | |
| return varMap[name]; | |
| }; | |
| const cnf = clauses.map(clause => { | |
| const lits = clause.split('OR').map(l => l.trim()); | |
| return lits.map(l => { | |
| const isNeg = l.includes('NOT'); | |
| const name = l.replace('NOT', '').trim(); | |
| const id = getVar(name); | |
| return isNeg ? -id : id; | |
| }); | |
| }); | |
| return { cnf, varMap, varCount: nextVar - 1 }; | |
| } | |
| // --- DPLL Algorithm (Async for visualization) --- | |
| async solve() { | |
| if (this.isRunning) return; | |
| this.isRunning = true; | |
| this.resetUI(); | |
| const input = document.getElementById('formula-input').value; | |
| let cnf, varMap, varCount; | |
| try { | |
| const parsed = this.parseFormula(input); | |
| cnf = parsed.cnf; | |
| varMap = parsed.varMap; | |
| varCount = parsed.varCount; | |
| } catch (e) { | |
| alert("Parsing Error: " + e.message); | |
| this.isRunning = false; | |
| return; | |
| } | |
| // Update Stats | |
| document.getElementById('var-count').textContent = varCount; | |
| document.getElementById('clause-count').textContent = cnf.length; | |
| document.getElementById('start-msg').style.display = 'none'; | |
| // Create Inverse Map for display | |
| const invMap = {}; | |
| Object.entries(varMap).forEach(([k, v]) => invMap[v] = k); | |
| // Tree root | |
| const rootId = this.idCounter++; | |
| const rootNode = { id: rootId, x: 300, y: 40, label: 'Start', parent: null, status: 'active' }; | |
| this.treeData = rootNode; | |
| this.drawNode(rootNode); | |
| // Run DPLL | |
| const startTime = performance.now(); | |
| const result = await this.dpll(cnf, {}, rootNode, invMap, 0); | |
| const endTime = performance.now(); | |
| // Finalize | |
| const resultBadge = document.getElementById('result-badge'); | |
| if (result.sat) { | |
| resultBadge.textContent = 'SATISFIABLE'; | |
| resultBadge.className = 'px-2 py-0.5 rounded text-xs font-bold bg-emerald-500/20 text-emerald-400 border border-emerald-500/30'; | |
| this.renderAssignment(result.model, invMap); | |
| this.flashSuccess(rootNode); | |
| } else { | |
| resultBadge.textContent = 'UNSATISFIABLE'; | |
| resultBadge.className = 'px-2 py-0.5 rounded text-xs font-bold bg-rose-500/20 text-rose-400 border border-rose-500/30'; | |
| } | |
| this.log(`Finished in ${(endTime - startTime).toFixed(1)}ms`, 'info'); | |
| this.isRunning = false; | |
| } | |
| async dpll(clauses, model, parentNode, invMap, depth) { | |
| await this.sleep(); | |
| // Check Empty Clause (Conflict) | |
| if (clauses.some(c => c.length === 0)) { | |
| parentNode.status = 'conflict'; | |
| this.updateNodeVisual(parentNode); | |
| this.log(`Conflict detected at depth ${depth}`, 'error'); | |
| return { sat: false }; | |
| } | |
| // Check All Satisfied | |
| if (clauses.length === 0) { | |
| parentNode.status = 'sat'; | |
| this.updateNodeVisual(parentNode); | |
| this.log(`Model found: ${JSON.stringify(model)}`, 'success'); | |
| return { sat: true, model: { ...model } }; | |
| } | |
| // Unit Propagation | |
| const unit = this.findUnit(clauses); | |
| if (unit) { | |
| const litName = unit > 0 ? invMap[unit] : `!${invMap[-unit]}`; | |
| this.log(`Unit Prop: ${litName} = true`, 'warning'); | |
| const newClauses = this.simplify(clauses, unit); | |
| const newModel = { ...model, [Math.abs(unit)]: unit > 0 }; | |
| // Visuals for unit prop don't branch, just extend the line | |
| const nextNode = this.createChildNode(parentNode, litName, depth + 1, 'unit'); | |
| this.drawEdge(parentNode, nextNode); | |
| return this.dpll(newClauses, newModel, nextNode, invMap, depth + 1); | |
| } | |
| // Pure Literal | |
| const pure = this.findPure(clauses); | |
| if (pure) { | |
| const litName = pure > 0 ? invMap[pure] : `!${invMap[-pure]}`; | |
| this.log(`Pure Lit: ${litName} = true`, 'warning'); | |
| const newClauses = this.simplify(clauses, pure); | |
| const newModel = { ...model, [Math.abs(pure)]: pure > 0 }; | |
| const nextNode = this.createChildNode(parentNode, litName, depth + 1, 'unit'); | |
| this.drawEdge(parentNode, nextNode); | |
| return this.dpll(newClauses, newModel, nextNode, invMap, depth + 1); | |
| } | |
| // Branching (Splitting) | |
| const variable = this.chooseVar(clauses); | |
| const varName = invMap[variable]; | |
| this.log(`Branch on ${varName}`, 'info'); | |
| document.getElementById('decision-count').textContent = parseInt(document.getElementById('decision-count').textContent) + 1; | |
| // Try True | |
| const trueNode = this.createChildNode(parentNode, `${varName}=T`, depth + 1, 'branch'); | |
| this.drawEdge(parentNode, trueNode); | |
| const trueResult = await this.dpll( | |
| this.simplify(clauses, variable), | |
| { ...model, [variable]: true }, | |
| trueNode, | |
| invMap, | |
| depth + 1 | |
| ); | |
| if (trueResult.sat) return trueResult; | |
| // Try False | |
| const falseNode = this.createChildNode(parentNode, `${varName}=F`, depth + 1, 'branch'); | |
| this.drawEdge(parentNode, falseNode); | |
| return this.dpll( | |
| this.simplify(clauses, -variable), | |
| { ...model, [variable]: false }, | |
| falseNode, | |
| invMap, | |
| depth + 1 | |
| ); | |
| } | |
| // --- Logic Helpers --- | |
| findUnit(clauses) { | |
| for (let c of clauses) { | |
| if (c.length === 1) return c[0]; | |
| } | |
| return null; | |
| } | |
| findPure(clauses) { | |
| const all = clauses.flat(); | |
| const counts = {}; | |
| all.forEach(l => { | |
| const v = Math.abs(l); | |
| if (!counts[v]) counts[v] = { pos: 0, neg: 0 }; | |
| if (l > 0) counts[v].pos++; else counts[v].neg++; | |
| }); | |
| for (let v in counts) { | |
| if (counts[v].pos > 0 && counts[v].neg === 0) return parseInt(v); | |
| if (counts[v].neg > 0 && counts[v].pos === 0) return -parseInt(v); | |
| } | |
| return null; | |
| } | |
| chooseVar(clauses) { | |
| return Math.abs(clauses[0][0]); | |
| } | |
| simplify(clauses, lit) { | |
| return clauses | |
| .filter(c => !c.includes(lit)) // Remove clauses containing lit | |
| .map(c => c.filter(x => x !== -lit)); // Remove -lit from clauses | |
| } | |
| // --- Visualization Helpers --- | |
| createChildNode(parent, label, depth, type) { | |
| const id = this.idCounter++; | |
| // Calculate position based on tree layout | |
| // Simple vertical layout with spacing based on depth | |
| const y = parent.y + 80; | |
| const xOffset = (type === 'branch' ? 120 : 0) / (depth + 1); | |
| // Random jitter to prevent perfect overlap in unit chains | |
| const jitter = (Math.random() - 0.5) * 40; | |
| const node = { | |
| id: id, | |
| x: parent.x + (type === 'branch' ? (parent.childrenLeft ? -80 : 80) : jitter), | |
| y: y, | |
| label: label, | |
| parent: parent, | |
| status: 'active', | |
| type: type | |
| }; | |
| if (type === 'branch') parent.childrenLeft = !parent.childrenLeft; // Toggle side | |
| this.drawNode(node); | |
| return node; | |
| } | |
| drawNode(node) { | |
| const el = document.createElement('div'); | |
| el.id = `node-${node.id}`; | |
| el.className = `absolute transform -translate-x-1/2 -translate-y-1/2 node-enter flex items-center justify-center w-12 h-12 rounded-full border-2 bg-[#1e1e2e] z-20 font-mono text-xs font-bold text-white shadow-lg transition-colors duration-500`; | |
| el.style.left = node.x + 'px'; | |
| el.style.top = node.y + 'px'; | |
| el.style.borderColor = '#6366f1'; | |
| el.style.boxShadow = '0 0 15px rgba(99, 102, 241, 0.4)'; | |
| el.innerHTML = `<span class="truncate px-1">${node.label}</span>`; | |
| this.nodeLayer.appendChild(el); | |
| // Pan view to follow node if it goes off screen | |
| const container = document.getElementById('tree-container'); | |
| if (node.y > 500 + Math.abs(this.translateY)) { | |
| this.translateY -= 100; | |
| this.updateTransform(); | |
| } | |
| } | |
| drawEdge(parent, child) { | |
| const path = document.createElementNS('http://www.w3.org/2000/svg', 'path'); | |
| const d = `M ${parent.x} ${parent.y + 24} L ${child.x} ${child.y - 24}`; | |
| path.setAttribute('d', d); | |
| path.setAttribute('stroke', '#4b5563'); | |
| path.setAttribute('stroke-width', '2'); | |
| path.setAttribute('fill', 'none'); | |
| path.classList.add('edge-path'); | |
| this.svg.appendChild(path); | |
| } | |
| updateNodeVisual(node) { | |
| const el = document.getElementById(`node-${node.id}`); | |
| if (!el) return; | |
| if (node.status === 'conflict') { | |
| el.style.borderColor = '#f43f5e'; | |
| el.style.boxShadow = '0 0 15px rgba(244, 63, 94, 0.4)'; | |
| el.style.color = '#fda4af'; | |
| } else if (node.status === 'sat') { | |
| el.style.borderColor = '#34d399'; | |
| el.style.boxShadow = '0 0 20px rgba(52, 211, 153, 0.6)'; | |
| el.style.backgroundColor = '#064e3b'; | |
| } | |
| } | |
| flashSuccess(node) { | |
| // Trace back path | |
| let curr = node; | |
| while (curr) { | |
| const el = document.getElementById(`node-${curr.id}`); | |
| if (el) { | |
| el.style.borderColor = '#34d399'; | |
| el.style.color = '#fff'; | |
| el.style.zIndex = 30; | |
| } | |
| // Highlight edge to parent | |
| // (Simplified for this demo, just highlighting nodes) | |
| curr = curr.parent; | |
| } | |
| } | |
| // --- UI Helpers --- | |
| log(msg, type) { | |
| const div = document.createElement('div'); | |
| div.className = 'py-1 border-l-2 pl-2 text-xs font-mono animate-pulse'; | |
| if (type === 'error') { | |
| div.classList.add('border-rose-500', 'text-rose-400'); | |
| div.innerHTML = `<span class="font-bold">✗</span> ${msg}`; | |
| } else if (type === 'success') { | |
| div.classList.add('border-emerald-500', 'text-emerald-400'); | |
| div.innerHTML = `<span class="font-bold">✓</span> ${msg}`; | |
| } else if (type === 'warning') { | |
| div.classList.add('border-amber-500', 'text-amber-400'); | |
| div.innerHTML = `<span class="font-bold">⚡</span> ${msg}`; | |
| } else { | |
| div.classList.add('border-indigo-500', 'text-indigo-300'); | |
| div.innerHTML = `<span class="font-bold">ℹ</span> ${msg}`; | |
| } | |
| this.logContainer.prepend(div); // Add to top | |
| // Remove pulse after a while | |
| setTimeout(() => div.classList.remove('animate-pulse'), 1000); | |
| } | |
| renderAssignment(model, invMap) { | |
| this.assignmentGrid.innerHTML = ''; | |
| Object.entries(model).forEach(([k, v]) => { | |
| const name = invMap[k]; | |
| const val = v ? 'T' : 'F'; | |
| const color = v ? 'text-emerald-400 border-emerald-500/30 bg-emerald-500/10' : 'text-rose-400 border-rose-500/30 bg-rose-500/10'; | |
| const div = document.createElement('div'); | |
| div.className = `flex flex-col items-center justify-center p-2 rounded border ${color}`; | |
| div.innerHTML = ` | |
| <span class="text-xs font-bold opacity-70">${name}</span> | |
| <span class="text-lg font-bold font-mono">${val}</span> | |
| `; | |
| this.assignmentGrid.appendChild(div); | |
| }); | |
| } | |
| resetUI() { | |
| this.svg.innerHTML = ''; | |
| this.nodeLayer.innerHTML = ''; | |
| this.logContainer.innerHTML = '<div class="text-slate-600 italic">Starting process...</div>'; | |
| this.assignmentGrid.innerHTML = '<div class="col-span-4 text-center text-xs text-slate-600 py-2">No solution yet</div>'; | |
| document.getElementById('result-badge').textContent = '--'; | |
| document.getElementById('result-badge').className = 'px-2 py-0.5 rounded text-xs font-bold bg-slate-700 text-slate-300'; | |
| document.getElementById('decision-count').textContent = '0'; | |
| this.idCounter = 0; | |
| this.resetView(); | |
| } | |
| sleep() { | |
| // Base delay 1000ms, divided by speed multiplier | |
| const delay = 800 / this.speed; | |
| return new Promise(resolve => setTimeout(resolve, delay)); | |
| } | |
| reset() { | |
| if (this.isRunning) return; | |
| this.resetUI(); | |
| document.getElementById('start-msg').style.display = 'flex'; | |
| } | |
| loadExample(id) { | |
| if (this.isRunning) return; | |
| const examples = { | |
| 1: "(a || !b) && (!a || c) && (b || !c)", // SAT | |
| 2: "(a) && (!a || b) && (!b)", // UNSAT | |
| 3: "(x || y) && (!x || y || z) && (!y || !z) && (x || !y || z)", // SAT | |
| 4: "(!Q1_1) && (!Q2_1) && (!Q2_2) && (Q2_1 || Q2_2) && (!Q2_1 || !Q2_2) && (!Q3_1) && (!Q3_2) && (!Q3_3) && (Q3_1 || Q3_2 || Q3_3) && (!Q3_1 || !Q3_2) && (!Q3_1 || !Q3_3) && (!Q3_2 || !Q3_3)" | |
| }; | |
| document.getElementById('formula-input').value = examples[id]; | |
| } | |
| copyCode() { | |
| const code = document.getElementById('elixir-code').textContent; | |
| navigator.clipboard.writeText(code).then(() => { | |
| const btn = document.querySelector('button[onclick="app.copyCode()"]'); | |
| const original = btn.textContent; | |
| btn.textContent = "Copied!"; | |
| setTimeout(() => btn.textContent = original, 2000); | |
| }); | |
| } | |
| } | |
| // Initialize | |
| const app = new DPLLVisualizer(); | |
| // Initial setup | |
| app.resetView(); | |
| </script> | |
| </body> | |
| </html> |