Inconsistent results with/without weight of 0 about gophersat HOT 6 CLOSED

This seems like a bug to me too.

from gophersat.

This is definitely a bug, and I'll have a look at it right now. Sorry for the delay, I haven't been notified of this issue by e-mail.

from gophersat.

Hi there, thanks for the reply and fix.
I found another failure case after this fix. So the issue should probably be rephrased to “Equal PB Problems can lead to different num of results”.

Here is the failure case

package main

import (
	"fmt"
	"github.com/crillab/gophersat/solver"
)

func main() {
	pb1 := solver.AtMost([]int{1, 2, 3, 4}, 3)
	pb2 := solver.AtLeast([]int{1, 2, 3, 4}, 2)

	case1 := func(){
		pb3 := solver.GtEq([]int{2, 3, 4}, []int{1, 1, 2}, 3)
		pb := solver.ParsePBConstrs([]solver.PBConstr{pb1, pb2, pb3})
		s := solver.New(pb)
		fmt.Println("Case1", s.CountModels())
	}

	case2 := func(){
		pb3 := solver.GtEq([]int{1, 2, 4}, []int{1, 2, 1}, 3)
		pb := solver.ParsePBConstrs([]solver.PBConstr{pb1, pb2, pb3})
		s := solver.New(pb)
		fmt.Println("Case2", s.CountModels())
	}

	case1()
	case2()
}

// output:
// 4
// 5

You can test it out here:
https://play.golang.org/p/lKZ9IlfehRw

@fdelorme can we reopen this issue?

from gophersat.

Yes ! I'll have a look at that.

from gophersat.

The bug is fixed now in the version 1.2.0. It wasn't an issue with PB constraints, but a bug in the solver.CountModels functions, caused by an optimization in the core solver.

For instance, as soon as the solver finds the instance is satisfied by binding the variable x1 to false, and the variables x2 and x4 to false, the solver returns as it doesn't have to try to bind the variable x3 (both x3 and not(x3) satisfy the problem). The problem is, CountModels counted this as a single model (not(x1) and x2 and x4) instead of 2 (not(x1) and x2 and x3 and x4, or not (x1) and x2 and not(x3) and x4).

As of now the fix doesn't appear in the go playground (probably a caching issue), but I tested it locally and it does now display 5 and 5.

Please let me know if you want me to close the issue.

from gophersat.

@fdelorme Thanks for the explanation and it really makes sense. This new release works for me now! I am closing this ticket now.

from gophersat.