Repository navigation

Add binary decision ILP to SAT and fix solution validators - #1218

Merged

GiggleLiu merged 22 commits into

issue-1213-direct-qubo-phase4from

feat/binary-ilp-to-sat

Oct 29, 2026

Merged

Add binary decision ILP to SAT and fix solution validators#1218
GiggleLiu merged 22 commits into
issue-1213-direct-qubo-phase4from
feat/binary-ilp-to-sat

Commits on Oct 23, 2026
- Add binary decision ILP to SAT reduction
  isPANN
  committed
  c6bfae6
- Fix solution length validation and remove redundant test scaffolding
  isPANN
  committed
  0daa9a8
Commits on Oct 27, 2026
- Count ILP nonzeros per constraint family instead of rows times columns
  
  isPANN
  and
  claude
  committed
  4da646d
- Check ILP nonzero bounds on dense sources
  
  isPANN
  and
  claude
  committed
  f95447a
- Bound scheduling QUBO sizes by worker bits and start windows
  
  isPANN
  and
  claude
  committed
  4ce1d38
- Restate StaffScheduling and SWRTD QUBO sizes in the paper and tests
  
  isPANN
  and
  claude
  committed
  0801132
- Reject negative ConsecutiveOnesSubmatrix bounds at construction
  
  isPANN
  and
  claude
  committed
  8523caa
- Declare exact parameter counts the constructions always produce
  
  isPANN
  and
  claude
  committed
  3de4a67
- Keep 3-SAT literal-dependent counts as upper bounds
  
  isPANN
  and
  claude
  committed
  b8867cf
Commits on Oct 28, 2026
- Test exact construction counts on degenerate graphs
  
  isPANN
  and
  claude
  committed
  0318bfd
- Reduce negative-weight MaxCut to MinimumMatrixCover with an edge gadget
  
  isPANN
  and
  claude
  committed
  f7be538
- Simplify the MaxCut gadget, retype the COS bound, and clean up docs
  
  isPANN
  and
  claude
  committed
  ef18c76
- Remove the KSatisfiability KN variant and short-clause constructors
  
  isPANN
  and
  claude
  committed
  5e512c7
- Declare MonochromaticTriangle counts exact and drop stale short-clause text
  
  isPANN
  and
  claude
  committed
  86d6808
- Bound KSatisfiability by FixedK and tidy the K-SAT reductions
  
  isPANN
  and
  claude
  committed
  eafd02a
- Drop the FixedK trait
  
  isPANN
  and
  claude
  committed
  3c2f9bd
Commits on Oct 29, 2026

Navigation Menu

Repository navigation

Add binary decision ILP to SAT and fix solution validators - #1218

Add binary decision ILP to SAT and fix solution validators#1218
GiggleLiu merged 22 commits into
issue-1213-direct-qubo-phase4from
feat/binary-ilp-to-sat

Commits on Oct 23, 2026

Add binary decision ILP to SAT reduction

Fix solution length validation and remove redundant test scaffolding

Commits on Oct 27, 2026

Count ILP nonzeros per constraint family instead of rows times columns

Check ILP nonzero bounds on dense sources

Bound scheduling QUBO sizes by worker bits and start windows

Restate StaffScheduling and SWRTD QUBO sizes in the paper and tests

Reject negative ConsecutiveOnesSubmatrix bounds at construction

Declare exact parameter counts the constructions always produce

Keep 3-SAT literal-dependent counts as upper bounds

Commits on Oct 28, 2026

Test exact construction counts on degenerate graphs

Reduce negative-weight MaxCut to MinimumMatrixCover with an edge gadget

Simplify the MaxCut gadget, retype the COS bound, and clean up docs

Remove the KSatisfiability KN variant and short-clause constructors

Declare MonochromaticTriangle counts exact and drop stale short-clause text

Bound KSatisfiability by FixedK and tidy the K-SAT reductions

Drop the FixedK trait

Commits on Oct 29, 2026

Align K3 reduction proofs with exact-width clauses

Check matrix-cover objective range before reduction

Merge pull request #1225 from CodingThrust/refactor/remove-ksat-kn

Merge pull request #1224 from CodingThrust/feat/exact-tight-bounds

Merge pull request #1222 from CodingThrust/fix/ilp-nonzeros-bounds

Merge pull request #1223 from CodingThrust/fix/qubo-scheduling-bounds