1. Alexandru Moșoi
  2. gasca

Source

gasca / lib / bcp_test.go

package gasca

import (
	"testing"
)

// Returns true fi cnf contains all dimacs
func hasAll(cnf []Literal, dimacs... int) bool {
	set := make(map[Literal]bool)
	for _, lit := range cnf {
		set[lit] = true
	}
	for _, lit := range dimacs {
		if !set[FromDIMACS(lit)] {
			return false
		}
	}
	return true
}

// Tests a very simple formula.
func TestBCPSimple1(t *testing.T) {
	f := NewFormula(10)
	f.AddDIMACSClause([]int { 1 })
	f.AddDIMACSClause([]int { -1, 2 })
	f.AddDIMACSClause([]int { -2, 3 })
	f.AddDIMACSClause([]int { -2, 4 })
	f.AddDIMACSClause([]int { -2, 5 })
	f.AddDIMACSClause([]int { -3, -4, -5, 6 })

	bcp := NewBCP(f)
	if bcp == nil {
		t.Error("Formula is not a contradiction:", f)
	}
	if !hasAll(bcp.Trail, 1, 2, 3, 4, 5, 6) {
		t.Error("Not all literals were discovered:", bcp.Trail)
	}
}

// Tests a very simple formula.
func TESTBCPSimple2(t *testing.T) {
	f := NewFormula(10)
	f.AddDIMACSClause([]int { 1 })
	f.AddDIMACSClause([]int { -1, 2 })
	f.AddDIMACSClause([]int { -1, -2, 3 })
	f.AddDIMACSClause([]int { -1. -2, -3, 4 })
	f.AddDIMACSClause([]int { -1, -2, -3, -4, 5 })
	f.AddDIMACSClause([]int { -1, -2, -3, -4, -5, 6 })
	f.AddDIMACSClause([]int { -1, -2, -3, -4, -5, -6, 7 })

	bcp := NewBCP(f)
	if bcp == nil {
		t.Error("Formula is not a contradiction")
	}
	if !hasAll(bcp.Trail, 1, 2, 3, 4, 5, 6, 7) {
		t.Error("Not all literals were discovered", bcp.Trail)
	}
}

// Builds a very long chain.
func TestBCPLongChain(t *testing.T) {
	u := make([]int, 0, 100)
	f := NewFormula(100)
	for i := 1; i < 100; i++ {
		f.AddDIMACSClause([]int { -i, i + 1 })
		u = append(u, i)
	}
	f.AddDIMACSClause([]int { 1 })
	u = append(u, 100)

	bcp := NewBCP(f)
	if bcp == nil {
		t.Error("Formula is not a contradiction")
	}
	if !hasAll(bcp.Trail, u...) {
		t.Error("Incomplete chain:", bcp.Trail)
	}
}

// Checks that BCP detects a contradiction.
func TestBCPContradiction1(t *testing.T) {
	f := NewFormula(10)
	f.AddDIMACSClause([]int { 1 })
	f.AddDIMACSClause([]int { -1, 2 })
	f.AddDIMACSClause([]int { -2, 3 })
	f.AddDIMACSClause([]int { -2, 4 })
	f.AddDIMACSClause([]int { -2, 5 })
	f.AddDIMACSClause([]int { -1, 6 })
	f.AddDIMACSClause([]int { -6, 7 })
	f.AddDIMACSClause([]int { -6, 8 })
	f.AddDIMACSClause([]int { -6, 9 })
	f.AddDIMACSClause([]int { -3, -4, -5, 10 })
	f.AddDIMACSClause([]int { -7, -8, -9, -10 })

	bcp := NewBCP(f)
	if bcp != nil {
		t.Error("Formula is a contradiction")
	}
}

// Checks that BCP detects a contradiction.
func TestBCPContradiction2(t *testing.T) {
	f := NewFormula(10)
	f.AddDIMACSClause([]int { 1 })
	f.AddDIMACSClause([]int { -1 })

	bcp := NewBCP(f)
	if bcp != nil {
		t.Error("Formula is a contradiction")
	}
}

// Propagates a solution of small.cnf.gz.
func TestBCPSmall(t *testing.T) {
	f, _ := ReadFile("small.cnf.gz")

	sol := []int{-1, -2, 3, -4, -5, -6, -7, 8, -9, -10, -11, 12, -13, -14,
	-15, -16, -17, -18, 19, -20, -21, -22, -23, 24, -25, -26, -27, -28, 29,
	-30, -31, -32, 33, -34, -35, -36, -37, -38, 39, -40, 41, -42, -43, -44,
	-45, -46, -47, 48, -49, -50, -51, 52, -53, -54, -55, -56, -57, -58, 59,
	-60, 61, -62, -63, -64, -65, 66, -67, -68, -69, -70, -71, 72, -73, -74,
	-75, -76, -77, -78, 79, -80, -81, 82, -83, -84, -85, -86, -87, -88, 89,
	-90, -91, 92, -93, -94, -95, -96, -97, 98, -99, -100}

	bcp := NewBCP(f)

	for num := 1; num <= len(sol); num++ {
		count := 0
		for _, lit := range sol[:num] {
			if bcp.IsAssigned(FromDIMACS(lit)) {
				continue
			}

			count++
			if bcp.PropagateLiteral(FromDIMACS(lit), false) {
				t.Error("Formula is not a contradiction:", f)
			}
		}
		for i := 0; i < count; i++ {
			bcp.Undo()
		}
	}
}

// Performs a failed literal probing.
func BenchmarkFLP(b *testing.B) {
	b.StopTimer()
	f, _ := ReadFile("big.cnf.gz")
	bcp := NewBCP(f)
	b.StartTimer()

	for i := 0; i < b.N; i++ {
		for var_ := 1; var_ <= f.NumVariables; var_++ {
			lit := Variable(var_).Pos()

			for j := 0; j < 2; j++ {
				lit = lit.Neg()
				if !bcp.IsAssigned(lit) {
					bcp.PropagateLiteral(lit, false)
					bcp.Undo()
				}
			}
		}
	}
}