{"action":"created","issue":{"url":"https://api.github.com/repos/niklasso/minisat/issues/20","labels_url":"https://api.github.com/repos/niklasso/minisat/issues/20/labels{/name}","comments_url":"https://api.github.com/repos/niklasso/minisat/issues/20/comments","events_url":"https://api.github.com/repos/niklasso/minisat/issues/20/events","html_url":"https://github.com/niklasso/minisat/issues/20","id":54262104,"number":20,"title":"Minor logic errors in simplification","user":{"login":"chanseokoh","id":10523105,"avatar_url":"https://avatars.githubusercontent.com/u/10523105?v=3","gravatar_id":"","url":"https://api.github.com/users/chanseokoh","html_url":"https://github.com/chanseokoh","followers_url":"https://api.github.com/users/chanseokoh/followers","following_url":"https://api.github.com/users/chanseokoh/following{/other_user}","gists_url":"https://api.github.com/users/chanseokoh/gists{/gist_id}","starred_url":"https://api.github.com/users/chanseokoh/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/chanseokoh/subscriptions","organizations_url":"https://api.github.com/users/chanseokoh/orgs","repos_url":"https://api.github.com/users/chanseokoh/repos","events_url":"https://api.github.com/users/chanseokoh/events{/privacy}","received_events_url":"https://api.github.com/users/chanseokoh/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":10,"created_at":"2015-01-13T23:09:57Z","updated_at":"2016-01-26T17:22:36Z","closed_at":null,"body":"This was reported a long time ago, but no action has been taken since then. To make it conspicuous, and as a record, I am opening an issue.\r\n\r\nDetails can be found here:\r\nhttps://groups.google.com/forum/#!searchin/minisat/chanseok/minisat/ldiQ82kdLzA/2NzpebK7qEkJ"},"comment":{"url":"https://api.github.com/repos/niklasso/minisat/issues/comments/175127334","html_url":"https://github.com/niklasso/minisat/issues/20#issuecomment-175127334","issue_url":"https://api.github.com/repos/niklasso/minisat/issues/20","id":175127334,"user":{"login":"TomMD","id":137806,"avatar_url":"https://avatars.githubusercontent.com/u/137806?v=3","gravatar_id":"","url":"https://api.github.com/users/TomMD","html_url":"https://github.com/TomMD","followers_url":"https://api.github.com/users/TomMD/followers","following_url":"https://api.github.com/users/TomMD/following{/other_user}","gists_url":"https://api.github.com/users/TomMD/gists{/gist_id}","starred_url":"https://api.github.com/users/TomMD/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/TomMD/subscriptions","organizations_url":"https://api.github.com/users/TomMD/orgs","repos_url":"https://api.github.com/users/TomMD/repos","events_url":"https://api.github.com/users/TomMD/events{/privacy}","received_events_url":"https://api.github.com/users/TomMD/received_events","type":"User","site_admin":false},"created_at":"2016-01-26T17:22:36Z","updated_at":"2016-01-26T17:22:36Z","body":"@johntyree You could run a SAT solver that gives you a set of assignments plus an unsat core.  Then to construct the equivalent problem you re-produce the unsat core and add the assignments in as new CNF clauses with a single, possibly negated, literal."}}