#satisfiability — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #satisfiability, aggregated by home.social.
-
“#NeuralNetworks and the #Satisfiability Problem” is the 2019 Stanford PhD dissertation by Salsam. It describes NeuroSAT, a #GNN, that learns to solve propositional satisfiability #SAT, that simple, yet quintessentially NP-complete, problem.
Salsam is an active member of the #Lean theorem prover community, who had worked closely with de Moura.
https://stacks.stanford.edu/file/druid:jt562cf4590/dselsam_dissertation_final-augmented.pdf
-
Weekend project: try to solve some #combinatorics #enumeration problems by reduction to #SharpSAT. (Which, to be clear, I thought was unlikely to succeed!)
I picked c2d http://reasoning.cs.ucla.edu/c2d/ because it scored highly in the 2020 Model Counting Competition https://arxiv.org/abs/2012.01323 but I am not sure this is the same version. The one I got is dated 2005 and was 32-bit only. It ran out of memory on this 364-variable 942-clause instance (corresponding to 6 playing cards chosen from a standard 52-card deck.)
Looking at the 2023 competition instead, I think I should try SharpSAT-TD https://github.com/Laakeri/sharpsat-td but it is not as well documented. For example, I don't know if it supports the "eclauses" (exactly-one clauses) extension of the Dimacs CNF format.