{ "_id": "6a200782b401979e73446b54", "Package": "satire", "Type": "Package", "Title": "Define and Solve Boolean Satisfiability ('SAT') Problems", "Version": "1.0.0.9000", "Authors@R": "c(\nperson(\"Mike\", \"Cheng\", role = c(\"aut\", \"cre\", 'cph'), email = \"mikefc@coolbutuseless.com\"))", "Maintainer": "Mike Cheng ", "URL": "https://github.com/coolbutuseless/satire", "BugReports": "https://github.com/coolbutuseless/satire/issues", "Description": "Boolean satisifiability ('SAT') tests whether there are\nsets of variables which satisfy a Boolean formula. This package\nprovides tools for defining 'SAT' problems and includes a\n'DPLL'-based 'SAT' solver based upon Davis & Putnam (1960)\n. Built-in capabilities for Tseytin\ntransformation (Tseytin (1968)\n) allows for the input of\ncomplex Boolean formula. Cardinalility constraints are\nimplemented using commander variables (Klieber & Kwon (2007)\n)\nand sequential counters (Sinz (2005)\n). Tools for reading and writing\n'DIMACS' files are also included.", "License": "MIT + file LICENSE", "Encoding": "UTF-8", "RoxygenNote": "7.3.2", "Config/testthat/edition": "3", "VignetteBuilder": "knitr", "Config/pak/sysreqs": "libicu-dev", "Repository": "https://coolbutuseless.r-universe.dev", "Date/Publication": "2025-04-07 00:17:36 UTC", "RemoteUrl": "https://github.com/coolbutuseless/satire", "RemoteRef": "HEAD", "RemoteSha": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "NeedsCompilation": "no", "Packaged": { "Date": "2026-06-03 10:50:05 UTC", "User": "root" }, "Author": "Mike Cheng [aut, cre, cph]", "MD5sum": "506ed8d428f6beb4e8755172babbe049", "_user": "coolbutuseless", "_type": "src", "_file": "satire_1.0.0.9000.tar.gz", "_fileid": "3456022e70e5f07ca780fa350b9b4843bd78babaec95ad0cddd9acbb951661d8", "_filesize": 666261, "_sha256": "3456022e70e5f07ca780fa350b9b4843bd78babaec95ad0cddd9acbb951661d8", "_created": "2026-06-03T10:50:05.000Z", "_published": "2026-06-03T10:52:50.668Z", "_distro": "noble", "_jobs": [ { "job": 79277186798, "time": 131, "config": "linux-devel-x86_64", "r": "4.7.0", "check": "OK", "artifact": "7382550529" }, { "job": 79277186906, "time": 125, "config": "linux-release-x86_64", "r": "4.6.0", "check": "OK", "artifact": "7382549121" }, { "job": 79277186881, "time": 87, "config": "macos-oldrel-arm64", "r": "4.5.3", "check": "OK", "artifact": "7382534419" }, { "job": 79277186814, "time": 127, "config": "macos-release-arm64", "r": "4.6.0", "check": "OK", "artifact": "7382549441" }, { "job": 79276617174, "time": 202, "config": "source", "r": "4.6.0", "check": "OK", "artifact": "7382503706" }, { "job": 79277186815, "time": 111, "config": "wasm-release", "r": "4.6.0", "check": "OK", "artifact": "7382543186" }, { "job": 79277186841, "time": 114, "config": "windows-devel", "r": "4.7.0", "check": "OK", "artifact": "7382544340" }, { "job": 79277186919, "time": 78, "config": "windows-oldrel", "r": "4.5.3", "check": "OK", "artifact": "7382531363" }, { "job": 79277186865, "time": 76, "config": "windows-release", "r": "4.6.0", "check": "OK", "artifact": "7382530666" } ], "_buildurl": "https://github.com/r-universe/coolbutuseless/actions/runs/26879791394", "_status": "success", "_host": "GitHub-Actions", "_upstream": "https://github.com/coolbutuseless/satire", "_commit": { "id": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "author": "mike ", "committer": "mike ", "message": "update docs [no ci]\n", "time": 1743985056 }, "_maintainer": { "name": "Mike Cheng", "email": "mikefc@coolbutuseless.com", "login": "coolbutuseless", "description": "Cool, but useless.", "uuid": 181818 }, "_registered": true, "_dependencies": [ { "package": "R", "version": ">= 4.1.0", "role": "Depends" }, { "package": "stringr", "role": "Imports" }, { "package": "knitr", "role": "Suggests" }, { "package": "rmarkdown", "role": "Suggests" }, { "package": "testthat", "version": ">= 3.0.0", "role": "Suggests" }, { "package": "ggplot2", "role": "Suggests" }, { "package": "purrr", "role": "Suggests" }, { "package": "glue", "role": "Suggests" } ], "_owner": "coolbutuseless", "_selfowned": true, "_usedby": 2, "_updates": [], "_tags": [], "_topics": [ "sat" ], "_stars": 7, "_contributors": [ { "user": "coolbutuseless", "count": 8, "uuid": 181818 } ], "_userbio": { "uuid": 181818, "type": "user", "name": "mikefc", "description": "Cool, but useless." }, "_downloads": { "count": 0, "source": "https://cranlogs.r-pkg.org/downloads/total/last-month/satire" }, "_devurl": "https://github.com/coolbutuseless/satire", "_searchresults": 15, "_rbuild": "4.6.0", "_assets": [ "extra/citation.cff", "extra/citation.html", "extra/citation.json", "extra/citation.txt", "extra/contents.json", "extra/NEWS.html", "extra/NEWS.txt", "extra/readme.html", "extra/readme.md", "extra/satire.html", "manual.pdf" ], "_cranurl": false, "_exports": [ "as_cnf", "is_cnf", "literals_to_dimacs", "read_dimacs", "sat_add_exprs", "sat_add_literals", "sat_block_solution", "sat_card_atleast_k", "sat_card_atleast_one", "sat_card_atmost_k", "sat_card_atmost_one", "sat_card_exactly_k", "sat_card_exactly_one", "sat_copy", "sat_literals_to_lgl", "sat_new", "sat_solve_dpll", "sat_solve_naive", "tseytin_transform" ], "_help": [ { "page": "as_cnf", "title": "Convert an arbitrary Boolean expression to conjunctive normal form (CNF)", "topics": [ "as_cnf" ] }, { "page": "is_cnf", "title": "Determine if the expression (in a string) is in conjunctive normal form", "topics": [ "is_cnf" ] }, { "page": "literals_to_dimacs", "title": "Convert literals to a DIMACS-formatted string", "concept": [ "export functions" ], "topics": [ "literals_to_dimacs" ] }, { "page": "print.sat_dimacs", "title": "Print a DIMACs representation returned from 'literals_to_dimacs()'", "topics": [ "print.sat_dimacs" ] }, { "page": "print.sat_prob", "title": "Print 'sat' object", "topics": [ "print.sat_prob" ] }, { "page": "read_dimacs", "title": "Read a DIMACS file as a 'sat' object.", "topics": [ "read_dimacs" ] }, { "page": "sat_add_exprs", "title": "Add Boolean expressions to a SAT problem", "concept": [ "ways of adding clauses" ], "topics": [ "sat_add_exprs" ] }, { "page": "sat_add_literals", "title": "Add integer literals to a SAT problem", "concept": [ "ways of adding clauses" ], "topics": [ "sat_add_literals" ] }, { "page": "sat_block_solution", "title": "Block a given result - use this for manually finding multiple solutions to a given problem.", "topics": [ "sat_block_solution" ] }, { "page": "sat_card_exactly_k", "title": "Add to SAT problem the cardinality constraint that \"exactly k\", \"at most k\" or \"at least k\" of the given variables are true", "concept": [ "SAT cardinality constraints" ], "topics": [ "sat_card_atleast_k", "sat_card_atmost_k", "sat_card_exactly_k" ] }, { "page": "sat_card_exactly_one", "title": "Add to SAT problem the cardinality constraint for \"exactly one\", \"at most one\" or \"at least one\" of the given variables is true", "concept": [ "SAT cardinality constraints" ], "topics": [ "sat_card_atleast_one", "sat_card_atmost_one", "sat_card_exactly_one" ] }, { "page": "sat_copy", "title": "Copy a SAT problem", "topics": [ "sat_copy" ] }, { "page": "sat_literals_to_lgl", "title": "Convert a sequence of integer literals to named logical vector", "topics": [ "sat_literals_to_lgl" ] }, { "page": "sat_new", "title": "Initialise a new SAT problem", "topics": [ "sat_new" ] }, { "page": "sat_solve_dpll", "title": "SAT solver using DPLL technique", "concept": [ "SAT solvers" ], "topics": [ "sat_solve_dpll" ] }, { "page": "sat_solve_naive", "title": "Naive, brute-force SAT solver with up-front memory allocation", "concept": [ "SAT solvers" ], "topics": [ "sat_solve_naive" ] }, { "page": "tseytin_transform", "title": "Convert a boolean formula to CNF using Tseytin's transformation", "topics": [ "tseytin_transform" ] } ], "_readme": "https://github.com/coolbutuseless/satire/raw/HEAD/README.md", "_rundeps": [ "cli", "glue", "lifecycle", "magrittr", "rlang", "stringi", "stringr", "vctrs" ], "_vignettes": [ { "source": "introduction.Rmd", "filename": "introduction.html", "title": "introduction", "engine": "knitr::rmarkdown", "headings": [ "satire", "What's in the box", "SAT Solvers", "SAT Example: Finding all possible work teams", "Problem statement", "Tools for defining a problem", "Cardinality helpers", "Unsatisfiable problem example", "Solving a problem from a DIMACs file" ], "created": "2025-04-04 11:34:43", "modified": "2025-04-07 00:17:36", "commits": 2 }, { "source": "nqueens.Rmd", "filename": "nqueens.html", "title": "N queens puzzle", "engine": "knitr::rmarkdown", "headings": [ "The N-queens puzzle", "The 4-queens puzzle", "What constraints exist?", "Defining the problem", "Solve", "Plot solution #1", "Plot solution #2" ], "created": "2025-04-04 11:34:43", "modified": "2025-04-04 11:34:43", "commits": 1 }, { "source": "peaceable-queens.Rmd", "filename": "peaceable-queens.html", "title": "Peaceable Queens", "engine": "knitr::rmarkdown", "headings": [ "The Peaceable Queens Puzzle", "Nomenclature", "Individual squares", "Row variables", "Basic pieces in R", "Boolean Expressions", "Expressions constraining the row/column indicator variables (for white)", "Expressions constraining the row/column indicator variables (for black)", "Exclusivity of white/black indicator variables", "Expressions constraining the diagonals", "Creating the SAT problem in", "Solving", "Solving with an external solver", "DIMACS export" ], "created": "2025-04-04 11:34:43", "modified": "2025-04-05 09:30:25", "commits": 4 }, { "source": "sudoku.Rmd", "filename": "sudoku.html", "title": "Sudoku", "engine": "knitr::rmarkdown", "headings": [ "Solving a 4x4 sudoku with SAT", "Nomenclature", "Constraints", "Defining a SAT problem - building blocks", "Building block: at least one of a set of variables must be true.", "Building block: at most one of a set of variables must be true", "Building block: exactly one of a set of variables must be true", "Defining the SAT problem with", "Solving" ], "created": "2025-04-04 11:34:43", "modified": "2025-04-04 11:34:43", "commits": 1 } ], "_score": 5.100370545117563, "_indexed": true, "_nocasepkg": "satire", "_universes": [ "coolbutuseless" ], "_binaries": [ { "r": "4.7.0", "os": "linux", "version": "1.0.0.9000", "date": "2026-06-03T10:52:19.000Z", "distro": "noble", "commit": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "fileid": "252b612a8232252818cd666cf94fae916bca13575e5d36c444639a222bc33d72", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/coolbutuseless/actions/runs/26879791394" }, { "r": "4.6.0", "os": "linux", "version": "1.0.0.9000", "date": "2026-06-03T10:52:15.000Z", "distro": "noble", "commit": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "fileid": "6b9325824a426a28dfd965ce43da21874325b00ea240f28c6dadd16a354d4926", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/coolbutuseless/actions/runs/26879791394" }, { "r": "4.5.3", "os": "mac", "version": "1.0.0.9000", "date": "2026-06-03T10:51:39.000Z", "commit": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "fileid": "56c1deaf453131822c281a8a3d7909050e0df12301cc156eb729f016a76a31bf", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/coolbutuseless/actions/runs/26879791394" }, { "r": "4.6.0", "os": "mac", "version": "1.0.0.9000", "date": "2026-06-03T10:52:17.000Z", "commit": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "fileid": "367cd612a785eda49ca65b953469514eaad3144e4d8ea60cec9960d0f6f92a51", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/coolbutuseless/actions/runs/26879791394" }, { "r": "4.6.0", "os": "wasm", "version": "1.0.0.9000", "date": "2026-06-03T10:52:14.000Z", "commit": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "fileid": "b54e36d2f2538fd8401ba422209b48bac1b1b0886672581ca2ad9198a232a9b0", "status": "success", "buildurl": "https://github.com/r-universe/coolbutuseless/actions/runs/26879791394" }, { "r": "4.7.0", "os": "win", "version": "1.0.0.9000", "date": "2026-06-03T10:51:54.000Z", "commit": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "fileid": "ae92ba9d41db50e6f7a40e1e5cc7099592971a9059f8b4a50ad329406f2f0bb4", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/coolbutuseless/actions/runs/26879791394" }, { "r": "4.5.3", "os": "win", "version": "1.0.0.9000", "date": "2026-06-03T10:51:21.000Z", "commit": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "fileid": "9c2f72460718c334f1c5df68308e7ec476fb015072f5b771afac8fd35603810c", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/coolbutuseless/actions/runs/26879791394" }, { "r": "4.6.0", "os": "win", "version": "1.0.0.9000", "date": "2026-06-03T10:51:18.000Z", "commit": "2bb32cf1a319d6f95a7a67330ebccaaff741de8d", "fileid": "1959827c540e61d349b567b22f8b820b0f945733bf645eefe8b0fc56dd7ffe05", "status": "success", "check": "OK", "buildurl": "https://github.com/r-universe/coolbutuseless/actions/runs/26879791394" } ] }