Skip to content

Conversation

@k-sidorov
Copy link
Contributor

Consider the following FlatZinc input:

array [1..3] of int: c = [1,0,-1];
var 0..1: x;
var 0..1: y;
var 0..1: z;
array [1..3] of var 0..1: vars = [x,y,z];
constraint int_lin_le(c,vars,0);
solve satisfy;

The current version of the solver crashes with division by zero, because it creates the affine views for all the terms. The bound computation in affine views assumes invertibility (through division by scale), however, affine views of the form <VAR>.scale(0) are not invertible.

This PR fixes this bug by discarding all such terms during FlatZinc compilation. I also add all three models I used for testing; all of them crash on main but successfully terminate in this branch.

The bound computation in affine views assumes invertibility (through division by scale), however, the affine views `<VAR>.scale(0)` are not invertible. This commit fixes it by discarding all such terms during FlatZinc compilation
@maartenflippo maartenflippo changed the title Remove the terms with zero coefficients from lienar constraints fix(pumpkin-solver): Remove the terms with zero coefficients from linear constraints Aug 6, 2025
@k-sidorov k-sidorov merged commit 576887e into main Aug 6, 2025
7 checks passed
@k-sidorov k-sidorov deleted the fix/zero-coefs branch August 6, 2025 14:08
ImkoMarijnissen added a commit that referenced this pull request Nov 10, 2025
🤖 I have created a release *beep* *boop*
---


##
[0.2.2](pumpkin-core-v0.2.1...pumpkin-core-v0.2.2)
(2025-11-10)


### Features

* Adding logging of brancher statistics on completion
([#257](#257))
([9d26842](9d26842))
* Post equality as single predicate instead of splitting in two
([#305](#305))
([8f43208](8f43208))
* Adding edge-finding for the disjunctive constraint
([#275](#275))
([606a7d8](606a7d8))
* Lazy explanation for linear less than or equals
([#290](#290))
([3515c7a](3515c7a))
* Write proofs with gzip encoding
([#264](#264))
([83f76da](83f76da))
* Remove unnecessary variables introduced by bool2int
([#232](#232))
([cf0b2fe](cf0b2fe))
* Use lazy explanations for BinaryEq
([#231](#231))
([4a89a5e](4a89a5e))
* Support warm_start and ignore constraint_name search annotations
([#235](#235))
([d7e8bb0](d7e8bb0))


### Bug Fixes

* Add pumpkin-crates to default-members
([#286](#286))
([bf7ff80](bf7ff80))
* Correctly reporting unknown solution in optimisation and solution
enumeration ([#247](#247))
([8c0f27c](8c0f27c))
* Create correct reason for preprocessing permanent nogood + Removing
unassigned status for PredicateId
([#250](#250))
([98ba136](98ba136))
* Provide `SelectionContext` instead of `Assignments` to
`Brancher::synchronise`
([#312](#312))
([9548114](9548114))
* Remove debug printing
([#254](#254))
([0ca93a2](0ca93a2))
* Remove the terms with zero coefficients from linear constraints
([#269](#269))
([576887e](576887e))
* Take root-propagation into account in the LUS optimiser
([#253](#253))
([d30ed06](d30ed06))
* Reduce cost of predicate notification
([#259](#259))
([d38e990](d38e990))

### Refactors

* Avoid unnecessary traversals of profiles in time-tabling + Improving
Explanations ([#282](#282))
([f7a4fdb](f7a4fdb))
* Don't use binary equals when logging the full proof
([#252](#252))
([4454d93](4454d93))

---
This PR was generated with [Release
Please](https://github.com/googleapis/release-please). See
[documentation](https://github.com/googleapis/release-please#release-please).

---------

Co-authored-by: Imko Marijnissen <imko.marijnissen@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants