結果

問題 No.5005 3-SAT
ユーザー ID 21712
提出日時 2025-02-09 12:45:21
言語 Go
(1.23.4)
結果
AC  
実行時間 1,858 ms / 2,000 ms
コード長 2,178 bytes
コンパイル時間 10,436 ms
コンパイル使用メモリ 236,144 KB
実行使用メモリ 6,824 KB
スコア 756
最終ジャッジ日時 2025-02-09 12:48:45
合計ジャッジ時間 200,659 ms
ジャッジサーバーID
（参考情報） 		judge3 / judge4
純コード判定しない問題か言語
このコードへのチャレンジ
（要ログイン）
ファイルパターン 結果
other AC * 100
権限があれば一括ダウンロードができます

ソースコード

diff # 

package main

import . "fmt"
import "iter"
import "time"

const N = 2048
const M = 256

func main() {
	conds := make([]*Cond, 0, N)
	for i := 0; i < N; i++ {
		z := newCond(i)
		Scan(z)
		if z.IsNoEffect() {
			continue
		}
		conds = append(conds, z)
	}
	
	go dfs(conds)
	
	<-time.After(time.Millisecond * 1800)
	
	println(score)
	for _, v := range ans[:] {
		Print(v)
	}
	Println()
}

var fixed [M]bool
var ans = make([]int, M)
var tmp [M]int
var score int

func dfs(conds []*Cond) {
	if len(conds) == 0 {
		return
	}
	z := conds[0]
	for a, p := range z.Iter() {
		if fixed[a] {
			if tmp[a] != p {
				continue
			}
			if z.Id > score {
				score = z.Id
				ans = make([]int, M)
				copy(ans[:], tmp[:])
			}
			dfs(conds[1:])
			return
		}
	}
	for a, p := range z.Iter() {
		if fixed[a] {
			continue
		}
		fixed[a] = true
		tmp[a] = p
		if z.Id > score {
			score = z.Id
			ans = make([]int, M)
			copy(ans[:], tmp[:])
		}
		dfs(conds[1:])
		fixed[a] = false
	}
}

type Cond struct {
	Id int
	factors [][]int
}

func newCond(id int) *Cond {
	return &Cond{id, make([][]int, 2)}
}

func (z *Cond) Ones() []int {
	return z.factors[1]
}

func (z *Cond) Zeros() []int {
	return z.factors[0]
}

func (z *Cond) Iter() iter.Seq2[int, int] {
	return func(yield func(k, v int) bool) {
		for p, fs := range z.factors {
			for _, a := range fs {
				if !yield(a, p) {
					return
				}
			}
		}
	}
}

func (z *Cond) IsNoEffect() bool {
	return len(z.Ones()) == 0 && len(z.Zeros()) == 0
}

func (z *Cond) IsOk(solution []int) bool {
	for i, fs := range z.factors {
		for _, a := range fs {
			if solution[a] == i {
				return true
			}
		}
	}
	return false
}

func (z *Cond) add(a, p int) {
	z.factors[p] = append(z.factors[p], a)
}

func (z *Cond) Scan(s ScanState, v rune) error {
	var a,b,c,p,q,r int
	Fscan(s,&a,&b,&c,&p,&q,&r)
	switch {
		case a == b && b == c:
			if p == q && q == r {
				z.add(a, p)
			}
		case a == b:
			if p == q {
				z.add(a, p)
				z.add(c, r)
			}
		case a == c:
			if p == r {
				z.add(a, p)
				z.add(b, q)
			}
		case b == c:
			if q == r {
				z.add(a, p)
				z.add(b, q)
			}
		default:
			z.add(a, p)
			z.add(b, q)
			z.add(c, r)
	}
	return nil
}
0