fnordomat 4ad8db04d3 Tiny, pedagogical DPLL SAT solver in C.		před 5 roky
..
Makefile	4ad8db04d3 Tiny, pedagogical DPLL SAT solver in C.	před 5 roky
README.md	4ad8db04d3 Tiny, pedagogical DPLL SAT solver in C.	před 5 roky
sat.c	4ad8db04d3 Tiny, pedagogical DPLL SAT solver in C.	před 5 roky

satsolver

A very simple, easy to understand DPLL SAT solver in 7533 bytes of C

Input format: command line arguments are clauses. literals are a-z positive, A-Z negative. Output format: sat (with a satisfying assignment), or unsat.

For example:

./sat abcdefghijklmnopqrstuvwxyz ABCDEFGHIJKLMNOPQRSTUVWXYZ ABCDEFz GHIJKLy MNOPQRx STUVwX PQRSTUvW KLUvwXY FGHIJOPQRu ABCDEFStZ KLOPQRsTU KOPQst KLrUVWX FGIJrxY KLQrUvW ABCDHIru GHOQrTUw KLPqSTU KLOqSuV BCDEPq GILMpQ LpqRSTU GOpqRSTuv ABDEpqRs KLOpqrSTUv GHIJKLMpqrsTU IJpqrst KLNoQ EHLopqR KLNopqr ABEGHn ABFHImO EFlOPQRS ABFIl AEFIkLT EFstUV JkLOstUv JkoQRstU NostuVWX stux ostu korst jOTUVWX jOPQRv juVWXZ jOPQRSuw ABCDEFNOsu jlrUVWx jklm ABcdefghj jopqtUvWx jrx jpqrs jkrst kost iTUvwx ghituV iJ ijK ijkL ijklM hOPQR hIJKL hOrst mnuVWX Opst ABcDeFgh hijopr hjOPr jKLMNOp joRSTu nOpqr noSTUVW hI gORSTU gu gry Ag fRUX fuZ fuz fOx fOrt pqrsT lOr

README.md

satsolver