Skip to content

SAT-solver based on resolution method in 2-CNF using PLY

Notifications You must be signed in to change notification settings

vpozdnyakov/sat_solver_resolution

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

14 Commits
 
 
 
 

Repository files navigation

SAT-solver based on resolution method

Homework project in Discrete Mathematics for Algorithm and Software Design course, HSE. Based on PLY (Python Lex-Yacc) parsing tool.

Task description

Given a Boolean formula in 2-CNF, use the resolution method to determine whether it is satisfiable. Clauses of the 2-CNF can be of one of the two forms: α \/ β or α -> β, where α and β are literals (p or ~p, where p is a variable). The CNF is presented in the usual notation, for example: (p -> q) /\ (~r \/ s) /\ (~q -> p)

Example

$ python hw_ply.py
input > (p -> q) /\ (~r \/ s) /\ (~q -> p)

Resolution: (~p\/q)/\(~r\/s)/\(q\/p)/\(None\/q)
Satisfiable: True

input > (p->q) /\ (q->r) /\ (r->s) /\ p /\ ~s

Resolution: (~p\/q)/\(~q\/r)/\(~r\/s)/\(p\/None)/\(~s\/None)/\(~p\/r)/\(q\/None)/\(~q\/s)/\(~r\/None)/\(~p\/s)/\(r\/None)/\(~q\/None)/\(~p\/None)/\(None\/s)/\(None\/None)
Satisfiable: False

About

SAT-solver based on resolution method in 2-CNF using PLY

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages