Một mệnh đề Horn là tuyển của các literal trong đó có tối đa một literal dương. Công thức Horn-SAT thỏa được hay không có thể quyết định trong thời gian đa thức bằng lan truyền đơn vị (unit propagation), khởi đầu gán mọi biến False rồi ép các biến dương thành True khi thân mệnh đề được thỏa. Cho công thức gồm m mệnh đề Horn trên n biến, in SAT hoặc UNSAT.
Dòng đầu: n, m. Mỗi mệnh đề trên một dòng bắt đầu bằng k (số literal), tiếp theo là k số nguyên khác 0 (mỗi mệnh đề có tối đa một số dương).
1≤n≤105, 0≤m≤2⋅105.
Một dòng: SAT nếu thỏa được, ngược lại UNSAT.
Ví dụ:
Đầu vào:
3 3
1 1
2 -1 2
2 -2 3
Đầu ra:
SAT
Giải thích:
Đang tải editor...