3-SAT Çözücü Python
Ben yazdım 3-SAT dayalı çözücüsü bu istemi:
Alice kısa süre önce bir donanım tasarım şirketinde çalışmaya başladı ve işinin bir parçası olarak fabrikasyon entegre devrelerdeki kusurları tespit etmesi gerekiyor. Bu kusurları belirlemeye yönelik bir yaklaşım, bir tatmin edilebilirlik örneğini çözmeye kadar indirgenir. Bu görevi yerine getirecek bir program yazmak için yardımına ihtiyacı var.
Giriş
Girişin ilk satırı, takip edilecek test senaryolarının sayısını gösteren, 5'ten fazla olmayan tek bir tam sayı içerir. Her bir test senaryosunun ilk satırı, n ve m olmak üzere iki tamsayı içerir; burada 1 ≤ n ≤ 20 değişken sayısını gösterir ve 1 ≤ m ≤ 100 cümle sayısını gösterir. Ardından, her bir cümleye karşılık gelen m satırları gelir. Her cümle, bazı 1 ≤ i ≤ n için Xi veya ~ Xi biçimindeki değişmez değerlerin bir ayrımıdır; burada ~ Xi, Xi'nin olumsuzlamasını gösterir. "Veya" operatörü bir "v" karakteriyle gösterilir ve değişmez değerlerden tek boşlukla ayrılır.Çıktı
Her test senaryosu için, tatmin edici bir atama varsa, tek bir satırda tatmin edici göster; aksi takdirde tatmin edilemez görüntüler.Örnek Giriş
2 3 3 X1 v X2 ~X1 ~X2 v X3 3 5 X1 v X2 v X3 X1 v ~X2 X2 v ~X3 X3 v ~X1 ~X1 v ~X2 v ~X3Örnek Çıktı
satisfiable unsatisfiable
Bu kod temelde mySetshangisinin tüm ifadeyi doğru yapabilecek olası değişmez değer kombinasyonlarını temsil eden bir kümeler listesi olduğunu korur . Yeni bir cümleci her ayrıştırdığımızda, olumsuzlamanın bir kümede zaten var olup olmadığını, varsa küme dahil edilmediğini kontrol ederiz.
Bu işe yarıyor, ancak biraz yavaş çalışıyor.
import sys
cases = int(sys.stdin.readline())
def GetReverse(literal):
if literal[0] == '~':
return literal[1:]
else:
return '~' + literal
for i in range(cases):
vars, clauses = map(int, sys.stdin.readline().split())
mySets = []
firstClause = sys.stdin.readline().strip().split(" v ")
for c in firstClause:
this = set()
this.add(c)
mySets.append(this)
for i in range(clauses-1):
tempSets = []
currentClause = sys.stdin.readline().strip().split(" v ")
for s in mySets:
for literal in currentClause:
if not s.__contains__(GetReverse(literal)):
newset = s.copy()
newset.add(literal)
tempSets.append(newset)
mySets = tempSets
if mySets:
print("satisfiable")
else:
print("unsatisfiable")
Sanırım sorun burada, girintili döngülerden dolayı. 3-SAT'ın üstel olması gerekiyor, ancak biraz hızlandırmak istiyorum (belki bir döngüyü kaldırarak?)
for i in range(clauses-1):
tempSets = []
currentClause = sys.stdin.readline().strip().split(" v ")
for s in mySets:
for literal in currentClause:
if not s.__contains__(GetReverse(literal)):
newset = s.copy()
newset.add(literal)
tempSets.append(newset)
mySets = tempSets
Yanıtlar
Kodunuzu stratejik olarak yerleştirilmiş baskı ifadeleriyle uygularsanız, tekrarlanan bazı hesaplamaların olduğunu göreceksiniz. İkinci test durumunda, cümle işlenirken X2 v ~X3, küme iki kez {'X1', 'X2'}eklenir mySets. Maddeyi işlerken, X3 v ~X1küme üç kez {'X3', 'X1', 'X2'}eklenir mySets.
Büyük durumlar için, o değiştirmek için işler daha hızlı olabilir mySetsa set()çiftleri ortadan kaldırmak için bir liste yerine. O halde iç setlerin olması gerekir frozensets.
mySetstüm maddeleri karşılayan olası çözümler kümesidir, bu yüzden adını olarak yeniden adlandırdım candidates.
candidatesTek bir boş küme içerecek şekilde başlatırsanız , ilk cümlenin ayrı ayrı ele alınması gerekmez.
Sanırım candidatesboş olduğunda her zaman durabilirsin .
Ayrıca, kodu işlevlere ayırın.
def is_satisfiable(n_vars, clauses):
candidates = {frozenset()}
for clause in clauses:
temp = set()
for s in candidates:
for literal in clause:
if GetReverse(literal) not in s:
temp.add(s | {literal})
candidates = temp
if len(candidates) == 0:
return False
return True
def load_case(f):
n_vars, n_clauses = f.readline().split()
clauses = [f.readline().strip().split(' v ') for _ in range(int(n_clauses))]
return int(n_vars), clauses
def main(f=sys.stdin):
num_cases = int(f.readline())
for i in range(num_cases):
n_vars, clauses = load_case(f)
result = is_satisfiable(n_vars, clauses)
print(f"{'satisfiable' if result else 'unsatisfiable'}")
Şöyle aradı:
import io
data = """
2
3 3
X1 v X2
~X1
~X2 v X3
3 5
X1 v X2 v X3
X1 v ~X2
X2 v ~X3
X3 v ~X1
~X1 v ~X2 v ~X3
""".strip()
main(io.StringIO(data))
veya
import sys
main(sys.stdin)
İşte algoritmanız hakkında temelde hiçbir şeyi değiştirmeyen önerilen bir uygulama, ancak
- uygun girintiye sahip
- biraz tip ipucu kullanır
- set değişmezlerini ve üreteçlerini kullanır
_"kullanılmayan" değişkenler için kullanırparse_clause()cümle kodu tekrarlandığı için bir ekler- Bir kullanır
StringIO, bu amaçlar için, etkili bir şekilde uzak taklitstdinve gösterdi örnek girişini kullanmak - PEP8 uyumlu adlar kullanır (alt çizgili)
from io import StringIO
from typing import List
stdin = StringIO('''2
3 3
X1 v X2
~X1
~X2 v X3
3 5
X1 v X2 v X3
X1 v ~X2
X2 v ~X3
X3 v ~X1
~X1 v ~X2 v ~X3
'''
)
def get_reverse(literal: str) -> str:
if literal[0] == '~':
return literal[1:]
return '~' + literal
def parse_clause() -> List[str]:
return stdin.readline().strip().split(' v ')
n_cases = int(stdin.readline())
for _ in range(n_cases):
n_vars, n_clauses = (int(s) for s in stdin.readline().split())
my_sets = [{c} for c in parse_clause()]
for _ in range(n_clauses - 1):
temp_sets = []
current_clause = parse_clause()
for s in my_sets:
for literal in current_clause:
if get_reverse(literal) not in s:
new_set = s.copy()
new_set.add(literal)
temp_sets.append(new_set)
my_sets = temp_sets
if my_sets:
print('satisfiable')
else:
print('unsatisfiable')