HN Academy

The best online courses of Hacker News.

Hacker News Comments on
Automated Reasoning: satisfiability

Coursera · EIT Digital · 3 HN comments

HN Academy has aggregated all Hacker News stories and comments that mention Coursera's "Automated Reasoning: satisfiability" from EIT Digital .
Course Description

In this course you will learn how to apply satisfiability (SAT/SMT) tools to solve a wide range of problems.

Several basic examples are given to get the flavor of the applications: fitting rectangles to be applied for printing posters, scheduling problems, solving puzzles, and program correctness. Also underlying theory is presented: resolution as a basic approach for propositional satisfiability, the CDCL framework to scale up for big formulas, and the simplex method to deal with linear inequallities.

The light weight approach to following this course is just watching the lectures and do the corresponding quizzes. To get a flavor of the topic this may work out fine. However, the much more interesting approach is to use this as a basis to apply SAT/SMT yourself on several problems, for instance on the problems presented in the honor's assignment.

HN Academy Rankings
  • Ranked #2 this month (jul/aug) · view
Provider Info
This course is offered by EIT Digital on the Coursera platform.
HN Academy may receive a referral commission when you make purchases on sites after clicking through links on this page. Most courses are available for free with the option to purchase a completion certificate.
See also: all Reddit discussions that mention this course at

Hacker News Stories and Comments

All the comments and stories posted to Hacker News that reference this url.
Jul 31, 2020 · psandersen on Kissat SAT Solver
I've been looking to get my feet wet with SAT and/or SMT solvers; can anyone recommend any short courses that I could start with to get a practical feel where where & how to use them? Python would be preferred.

Maybe this would be a good start?

Ideally I would like to be able to take predicted outputs from ML plus business requirements to solve allocation problems; and more pie in the sky I would like to know enough to get inspiration for how to link a neural network with a sat solver, such as perhaps replacing or augmenting beam search in sequence decoding tasks.

Well done! I'm taking a course on SAT solvers [1], but it uses some lisp format and lets you input from a richer language (e.g. distinct, if-then-else, plus integers rather than just booleans), so I had to look up the conjunctive normal format in your app. The readme for this repo [2] sent me here [3]. Pretty simple format.

I love how fast your app is!




Which course have you got in mind, [1] given by Hans Zantema?

[1] Automated Reasoning: satisfiability,

HN Academy is an independent project and is not operated by Y Combinator, Coursera, edX, or any of the universities and other institutions providing courses.
~ [email protected]
;laksdfhjdhksalkfj more things ~ Privacy Policy ~
Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.