Initial implementation (#2)

README.md

@@ -1 +1,3 @@
-# fusaso
+# fusaso
+
+I'm a horrible person but Go fuzzing is cool.

Taskfile.yml

@@ -0,0 +1,27 @@
+# https://taskfile.dev
+
+version: '3'
+
+tasks:
+  default:
+    cmds:
+      - task --list-all
+    silent: true
+
+  build:
+    cmds:
+      - go build -o fusaso main.go
+
+  run:
+    cmds:
+      - task: build
+      - ./fusaso
+
+  fuzz:
+    cmds:
+      - go test -v -run=^$ -fuzz=FuzzSolve solve_test.g
+
+  solve:
+    cmds:
+      - task: build
+      - ./fusaso -run

codegen.gotmpl

@@ -0,0 +1,42 @@
+//go:build ignore
+package tofuzz
+
+import (
+	"strings"
+	"testing"
+)
+
+var variables int = {{ .Variables }}
+
+func FuzzSolve(f *testing.F) {
+	f.Add(strings.Repeat("0", variables))
+	f.Add(strings.Repeat("1", variables))
+
+	f.Fuzz(func(t *testing.T, s string) {
+		switch {
+		case len(s) != variables:
+			return
+		case !isValid(s):
+			return
+		case check(s):
+			t.Fatalf("solution: %s", s)
+		}
+	})
+}
+
+func isValid(s string) bool {
+	for _, c := range s {
+		if c != '0' && c != '1' {
+			return false
+		}
+	}
+	return true
+}
+
+func check(x string) bool{
+	switch {
+{{ range .Cases }} {{ "\t" }}case {{ . }}: return false {{ "\n" }}{{ end }}
+	default:
+		return true
+	}
+}

go.mod

@@ -0,0 +1,5 @@
+module github.com/cristaloleg/fusaso
+
+go 1.21
+
+require github.com/cristaloleg/cnf v0.1.0

go.sum

@@ -0,0 +1,2 @@
+github.com/cristaloleg/cnf v0.1.0 h1:9uUb/2bct8vuKLOJanAM0qsJD2ZeILAzRXykBJl/sJI=
+github.com/cristaloleg/cnf v0.1.0/go.mod h1:HIGwS53/irUMNVfUpEs/6j/tRZgfiNr3YUtUWODZGjM=

main.go

@@ -0,0 +1,94 @@
+package main
+
+import (
+	_ "embed"
+	"flag"
+	"fmt"
+	"io"
+	"os"
+	"os/exec"
+	"strings"
+	"text/template"
+
+	"github.com/cristaloleg/cnf"
+)
+
+func main() {
+	fset := flag.NewFlagSet("fusaso", flag.ContinueOnError)
+
+	filename := fset.String("problem", "problem.cnf", "file with the problem (DIMACS format)")
+	output := fset.String("out", "fuzz_solve_test.go", "file with the codegen")
+	run := fset.Bool("run", false, "run the fuzzing")
+
+	if err := fset.Parse(os.Args[1:]); err != nil {
+		panic(err)
+	}
+
+	problemFile, err := os.Open(*filename)
+	if err != nil {
+		panic(err)
+	}
+	defer problemFile.Close()
+
+	outfile, err := os.Create(*output)
+	if err != nil {
+		panic(err)
+	}
+	defer outfile.Close()
+
+	problem, err := cnf.ParseDIMAC(problemFile)
+	if err != nil {
+		panic(err)
+	}
+
+	if err := codegen(outfile, problem); err != nil {
+		panic(err)
+	}
+
+	if *run {
+		cmd := exec.Command("go", "test", "-run=^$", "-fuzz=FuzzSolve", *output)
+		cmd.Stdin = os.Stdin
+		cmd.Stdout = os.Stdout
+		_ = cmd.Run()
+	}
+}
+
+func codegen(w io.Writer, p *cnf.Problem) error {
+	p.Formula.SortBySize()
+
+	data := struct {
+		Variables int
+		Cases     []string
+	}{
+		Variables: p.Variables,
+		Cases:     toCases(p.Formula),
+	}
+
+	return template.Must(template.New("").Parse(codeTmpl)).Execute(w, data)
+}
+
+//go:embed codegen.gotmpl
+var codeTmpl string
+
+func toCases(formula cnf.Formula) []string {
+	res := make([]string, len(formula))
+	for i, c := range formula {
+		res[i] = conv(c)
+	}
+	return res
+}
+
+func conv(clause cnf.Clause) string {
+	var b strings.Builder
+	for i, lit := range clause {
+		if i > 0 {
+			fmt.Fprint(&b, " && ")
+		}
+		if lit.Sign() {
+			fmt.Fprintf(&b, `x[%d] == '0'`, lit.Var()-1)
+		} else {
+			fmt.Fprintf(&b, `x[%d] == '1'`, lit.Var()-1)
+		}
+	}
+	return b.String()
+}

problem.cnf

@@ -0,0 +1,100 @@
+c This Formular is generated by mcnf
+c
+c    horn? no
+c    forced? no
+c    mixed sat? no
+c    clause length = 3
+c
+p cnf 20 91
+ 4 -18 19 0
+3 18 -5 0
+-5 -8 -15 0
+-20 7 -16 0
+10 -13 -7 0
+-12 -9 17 0
+17 19 5 0
+-16 9 15 0
+11 -5 -14 0
+18 -10 13 0
+-3 11 12 0
+-6 -17 -8 0
+-18 14 1 0
+-19 -15 10 0
+12 18 -19 0
+-8 4 7 0
+-8 -9 4 0
+7 17 -15 0
+12 -7 -14 0
+-10 -11 8 0
+2 -15 -11 0
+9 6 1 0
+-11 20 -17 0
+9 -15 13 0
+12 -7 -17 0
+-18 -2 20 0
+20 12 4 0
+19 11 14 0
+-16 18 -4 0
+-1 -17 -19 0
+-13 15 10 0
+-12 -14 -13 0
+12 -14 -7 0
+-7 16 10 0
+6 10 7 0
+20 14 -16 0
+-19 17 11 0
+-7 1 -20 0
+-5 12 15 0
+-4 -9 -13 0
+12 -11 -7 0
+-5 19 -8 0
+1 16 17 0
+20 -14 -15 0
+13 -4 10 0
+14 7 10 0
+-5 9 20 0
+10 1 -19 0
+-16 -15 -1 0
+16 3 -11 0
+-15 -10 4 0
+4 -15 -3 0
+-10 -16 11 0
+-8 12 -5 0
+14 -6 12 0
+1 6 11 0
+-13 -5 -1 0
+-7 -2 12 0
+1 -20 19 0
+-2 -13 -8 0
+15 18 4 0
+-11 14 9 0
+-6 -15 -2 0
+5 -12 -15 0
+-6 17 5 0
+-13 5 -19 0
+20 -1 14 0
+9 -17 15 0
+-5 19 -18 0
+-12 8 -10 0
+-18 14 -4 0
+15 -9 13 0
+9 -5 -1 0
+10 -19 -14 0
+20 9 4 0
+-9 -2 19 0
+-5 13 -17 0
+2 -10 -18 0
+-18 3 11 0
+7 -9 17 0
+-15 -6 -3 0
+-2 3 -13 0
+12 3 -2 0
+-2 -3 17 0
+20 -15 -16 0
+-5 -17 -19 0
+-20 -18 11 0
+-9 1 -5 0
+-19 9 17 0
+12 -2 17 0
+4 -16 -5 0
+c [4, 3, -5, -20, 10, -12, 17, -16, 18, 11, 0]