-
49441ba4e2
docs: add example instances and changelog
HEAD
main
dualfroz
2026-08-28 22:40:00 +02:00
-
14cd727d4a
test: add cardinality, xor, proof, and incremental tests
dualfroz
2026-08-28 19:15:00 +02:00
-
cca8377dfb
test: add cdcl, encoder, and difference logic tests
dualfroz
2026-08-28 15:50:00 +02:00
-
ccaa52b887
test: add solver, formula, and dimacs tests
dualfroz
2026-08-28 12:25:00 +02:00
-
4ed3491f50
feat(cli): add command-line entry point
dualfroz
2026-08-28 09:00:00 +02:00
-
cf47589cf6
feat(proof): add drat/rup proof logging and checking
dualfroz
2026-08-27 22:40:00 +02:00
-
8fea34a107
feat(cdcl): add incremental sat solving under assumptions
dualfroz
2026-08-27 19:15:00 +02:00
-
40b43a927f
feat(allsat): add model enumeration over all solutions
dualfroz
2026-08-27 15:50:00 +02:00
-
95cd91cedc
feat(theory): add difference logic solver
dualfroz
2026-08-27 12:25:00 +02:00
-
ec9edca5fa
feat(encode): add pigeonhole principle generator
dualfroz
2026-08-27 09:00:00 +02:00
-
8af1fa439a
feat(encode): add hamiltonian cycle encoding
dualfroz
2026-08-26 22:40:00 +02:00
-
a3b16797a2
feat(encode): add vertex cover encoding
dualfroz
2026-08-26 19:15:00 +02:00
-
59b3ebd355
feat(encode): add sudoku encoding and grid parser
dualfroz
2026-08-26 15:50:00 +02:00
-
6f96d10593
feat(encode): add graph coloring encoding
dualfroz
2026-08-26 12:25:00 +02:00
-
61c0449d7f
feat(encode): add n-queens encoding
dualfroz
2026-08-26 09:00:00 +02:00
-
3854d42178
feat(encode): add cardinality constraint encodings
dualfroz
2026-08-25 22:40:00 +02:00
-
64876af98f
feat(xor): add xor reasoning with gaussian elimination
dualfroz
2026-08-25 19:15:00 +02:00
-
4c9f61e79c
feat(preproc): add bounded variable elimination
dualfroz
2026-08-25 15:50:00 +02:00
-
fa34e71864
feat(preproc): add clause simplification pipeline
dualfroz
2026-08-25 12:25:00 +02:00
-
89a0105839
feat(cdcl): add top-level cdcl solve api
dualfroz
2026-08-25 09:00:00 +02:00
-
b5d1f4e2f3
feat(cdcl): add cdcl search with 1-uip analysis and restarts
dualfroz
2026-08-24 22:40:00 +02:00
-
95b52dec31
feat(cdcl): add solver state with two-watched-literal scheme
dualfroz
2026-08-24 19:15:00 +02:00
-
9795316136
feat(cdcl): add activity-ordered variable heap
dualfroz
2026-08-24 15:50:00 +02:00
-
81664ccad0
feat(cdcl): add solver statistics
dualfroz
2026-08-24 12:25:00 +02:00
-
0818ca05ff
feat(formula): add tseitin cnf transformation
dualfroz
2026-08-24 09:00:00 +02:00
-
a0cdd0c32b
feat(formula): add propositional formula parser and evaluator
dualfroz
2026-08-23 22:40:00 +02:00
-
09cf81b3e0
feat(dpll): add recursive dpll solver with model verification
dualfroz
2026-08-23 19:15:00 +02:00
-
34d591cbc3
feat(dimacs): add dimacs cnf parser and renderer
dualfroz
2026-08-23 15:50:00 +02:00
-
3104e31a5f
feat(core): add literal, clause, and cnf types
dualfroz
2026-08-23 12:25:00 +02:00
-
f37331f214
chore: add gitignore and build configuration
dualfroz
2026-08-23 09:00:00 +02:00