Dane Sabo
3299181c70
M lazy-lock.json M lua/custom/configs/lspconfig.lua M lua/custom/init.lua A lua/custom/journal.lua A nvim_venv/bin/Activate.ps1 A nvim_venv/bin/activate A nvim_venv/bin/activate.csh A nvim_venv/bin/activate.fish
71 lines
1.6 KiB
Python
71 lines
1.6 KiB
Python
"""For reading in DIMACS file format
|
|
|
|
www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps
|
|
|
|
"""
|
|
|
|
from sympy.core import Symbol
|
|
from sympy.logic.boolalg import And, Or
|
|
import re
|
|
|
|
|
|
def load(s):
|
|
"""Loads a boolean expression from a string.
|
|
|
|
Examples
|
|
========
|
|
|
|
>>> from sympy.logic.utilities.dimacs import load
|
|
>>> load('1')
|
|
cnf_1
|
|
>>> load('1 2')
|
|
cnf_1 | cnf_2
|
|
>>> load('1 \\n 2')
|
|
cnf_1 & cnf_2
|
|
>>> load('1 2 \\n 3')
|
|
cnf_3 & (cnf_1 | cnf_2)
|
|
"""
|
|
clauses = []
|
|
|
|
lines = s.split('\n')
|
|
|
|
pComment = re.compile(r'c.*')
|
|
pStats = re.compile(r'p\s*cnf\s*(\d*)\s*(\d*)')
|
|
|
|
while len(lines) > 0:
|
|
line = lines.pop(0)
|
|
|
|
# Only deal with lines that aren't comments
|
|
if not pComment.match(line):
|
|
m = pStats.match(line)
|
|
|
|
if not m:
|
|
nums = line.rstrip('\n').split(' ')
|
|
list = []
|
|
for lit in nums:
|
|
if lit != '':
|
|
if int(lit) == 0:
|
|
continue
|
|
num = abs(int(lit))
|
|
sign = True
|
|
if int(lit) < 0:
|
|
sign = False
|
|
|
|
if sign:
|
|
list.append(Symbol("cnf_%s" % num))
|
|
else:
|
|
list.append(~Symbol("cnf_%s" % num))
|
|
|
|
if len(list) > 0:
|
|
clauses.append(Or(*list))
|
|
|
|
return And(*clauses)
|
|
|
|
|
|
def load_file(location):
|
|
"""Loads a boolean expression from a file."""
|
|
with open(location) as f:
|
|
s = f.read()
|
|
|
|
return load(s)
|