Python Pemecah 3-SAT

Question

Saya telah menulis pemecah 3-SAT berdasarkan prompt ini :

Alice baru-baru ini mulai bekerja untuk perusahaan desain perangkat keras dan sebagai bagian dari pekerjaannya, dia perlu mengidentifikasi cacat pada sirkuit terintegrasi yang dibuat. Suatu pendekatan untuk mengidentifikasi cacat ini bermuara pada pemecahan contoh yang memuaskan. Dia membutuhkan bantuan Anda untuk menulis program untuk melakukan tugas ini.

Masukan
Baris pertama masukan berisi bilangan bulat tunggal, tidak lebih dari 5, yang menunjukkan jumlah kasus uji yang akan diikuti. Baris pertama tiap test case berisi dua bilangan bulat n dan m dimana 1 ≤ n ≤ 20 menunjukkan jumlah variabel dan 1 ≤ m ≤ 100 menunjukkan jumlah klausa. Kemudian, m baris mengikuti sesuai dengan setiap klausa. Setiap klausa adalah disjungsi literal dalam bentuk Xi atau ~ Xi untuk beberapa 1 ≤ i ≤ n, di mana ~ Xi menunjukkan negasi dari Xi literal. Operator “atau” dilambangkan dengan karakter 'v' dan dipisahkan dari literal dengan spasi tunggal.

Output
Untuk setiap kasus uji, tampilkan memuaskan pada satu baris jika ada tugas yang memuaskan; jika tidak, tampilan tidak memuaskan.

Contoh Input

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 

Output Sampel

satisfiable
unsatisfiable

Kode ini pada dasarnya mempertahankan mySetsyang merupakan daftar himpunan, yang semuanya mewakili kemungkinan kombinasi literal yang dapat membuat seluruh pernyataan benar. Setiap kali kami mengurai klausa baru, kami memeriksa apakah negasinya sudah ada dalam satu set, jika demikian, set tersebut tidak disertakan.

Ini berfungsi, tetapi berjalan agak lambat.

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")

Saya pikir masalahnya ada di sini, karena loop-for yang menjorok. 3-SAT seharusnya eksponensial, tetapi saya ingin mempercepatnya (mungkin dengan menghapus loop?)

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

Answer 1

Jika Anda melengkapi kode Anda dengan beberapa pernyataan cetak yang ditempatkan secara strategis, Anda akan melihat bahwa ada beberapa penghitungan berulang yang terjadi. Dalam kasus pengujian kedua saat memproses klausa X2 v ~X3, set {'X1', 'X2'}ditambahkan ke mySetsdua kali. Saat memproses klausa X3 v ~X1, set {'X3', 'X1', 'X2'}akan ditambahkan ke mySetstiga kali.

Untuk kasus besar, ini mungkin mempercepat segalanya untuk berubah mySetsmenjadi set()bukan daftar untuk menghilangkan duplikat. Maka set bagian dalam haruslah frozensets.

mySetsadalah sekumpulan solusi yang memungkinkan yang memenuhi semua klausa, jadi saya menamainya menjadi candidates.

Jika Anda menginisialisasi candidatesberisi satu set kosong, maka klausa pertama tidak perlu ditangani secara terpisah.

Saya pikir Anda bisa berhenti kapan saja candidateskosong.

Juga, bagi kode menjadi beberapa fungsi.

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'}")

Disebut seperti:

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))

atau

import sys

main(sys.stdin)        

Answer 2

Berikut adalah implementasi yang disarankan yang pada dasarnya tidak mengubah apa pun tentang algoritme Anda, tetapi

• memiliki lekukan yang tepat
• menggunakan sedikit petunjuk tipe
• menggunakan himpunan literal dan generator
• digunakan _untuk variabel "tidak terpakai"
• menambahkan a parse_clause()karena kode klausa diulang
• menggunakan a StringIO, untuk tujuan ini, untuk mengejek secara efektif stdindan menggunakan masukan contoh yang Anda tunjukkan
• menggunakan nama yang sesuai dengan PEP8 (dengan garis bawah)

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')