Package: satire 1.0.0.9000

satire: Define and Solve Boolean Satisfiability ('SAT') Problems

Boolean satisifiability ('SAT') tests whether there are sets of variables which satisfy a Boolean formula. This package provides tools for defining 'SAT' problems and includes a 'DPLL'-based 'SAT' solver based upon Davis & Putnam (1960) <doi:10.1145/321033.321034>. Built-in capabilities for Tseytin transformation (Tseytin (1968) <doi:10.1007/978-3-642-81955-1_28>) allows for the input of complex Boolean formula. Cardinalility constraints are implemented using commander variables (Klieber & Kwon (2007) <https://www.cs.cmu.edu/~wklieber/papers/2007_efficient-cnf-encoding-for-selecting-1.pdf>) and sequential counters (Sinz (2005) <doi:10.1007/11564751_73>). Tools for reading and writing 'DIMACS' files are also included.

Authors:Mike Cheng [aut, cre, cph]

satire_1.0.0.9000.tar.gz
satire_1.0.0.9000.zip(r-4.7)satire_1.0.0.9000.zip(r-4.6)satire_1.0.0.9000.zip(r-4.5)
satire_1.0.0.9000.tgz(r-4.6-any)satire_1.0.0.9000.tgz(r-4.5-any)
satire_1.0.0.9000.tar.gz(r-4.7-any)satire_1.0.0.9000.tar.gz(r-4.6-any)
satire_1.0.0.9000.tgz(r-4.6-emscripten)
manual.pdf |manual.html✨
DESCRIPTION |NEWS
card.svg |card.png
satire/json (API)

# Install 'satire' in R:
install.packages('satire', repos = c('https://coolbutuseless.r-universe.dev', 'https://cloud.r-project.org'))

Bug tracker:https://github.com/coolbutuseless/satire/issues

On CRAN:

Conda:

sat

5.10 score 7 stars 2 packages 15 scripts 19 exports 8 dependencies

Last updated from:2bb32cf1a3. Checks:9 OK. Indexed: yes.

TargetResultTimeFilesSyslog
linux-devel-x86_64OK131
source / vignettesOK202
linux-release-x86_64OK125
macos-release-arm64OK127
macos-oldrel-arm64OK87
windows-develOK114
windows-releaseOK76
windows-oldrelOK78
wasm-releaseOK111

Exports:as_cnfis_cnfliterals_to_dimacsread_dimacssat_add_exprssat_add_literalssat_block_solutionsat_card_atleast_ksat_card_atleast_onesat_card_atmost_ksat_card_atmost_onesat_card_exactly_ksat_card_exactly_onesat_copysat_literals_to_lglsat_newsat_solve_dpllsat_solve_naivetseytin_transform

Dependencies:cligluelifecyclemagrittrrlangstringistringrvctrs

introduction
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
Rendered fromintroduction.Rmdusingknitr::rmarkdown

Last update: 2025-04-07
Started: 2025-04-04

Peaceable Queens
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
Rendered frompeaceable-queens.Rmdusingknitr::rmarkdown

Last update: 2025-04-05
Started: 2025-04-04

N queens puzzle
The N-queens puzzle | The 4-queens puzzle | What constraints exist? | Defining the problem | Solve | Plot solution #1 | Plot solution #2
Rendered fromnqueens.Rmdusingknitr::rmarkdown

Last update: 2025-04-04
Started: 2025-04-04

Sudoku
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
Rendered fromsudoku.Rmdusingknitr::rmarkdown

Last update: 2025-04-04
Started: 2025-04-04