"=" support in cnf+

[farteryhr]

i see in the code that "=" is supported in opb format (by adding both <= and >=), but not in cnf+? is this intended or, just forgotten?

ps i wonder what's the status of #3, does duplicate in input still affect correctness across different variant of minicard now?

pps is jsminisolvers demo, seems only cnf is handled but not any of cardinality extension... is it unfinished?

ppps i'm playing with a classic problem no-three-in-line (latest results are quite old) and comparing across sat/logic solvers, while i find it perfect fit for minicard.
but i see #3 and this problem uses duplicates, and also i'm on windows, not sure how and which variant of minicard should i compile.
also since dear @liffiton showed interest in any usage of minicard, i'll feel free to present it here (and possibly eventually completely offload it to him (just kidding)).
this py3 script generates the problem definition and feed into some solvers or just saves the cnf[+] files. hopefully it will feed into minicard with no problem.
EDIT: oops just find pysat works on windows, gotta try it!
EDIT: works like a charm!

from collections import defaultdict
from sys import argv
# assume rot4 symetry
NH=8 # 27 for N=54 (no solution found yet)
if len(argv)>=2 and argv[1].isnumeric():
	NH=int(argv[1])
N=NH*2

dictuni={}
ps=[]

def all4(yx):
	y,x=yx
	return ((y,x),(N-y-1,N-x-1),(N-x-1,y),(x,N-y-1))

def gcd(a,b):
	if a==0:
		return b
	if b==0:
		return a
	return gcd(a%b,b) if a>b else gcd(b%a,a)


for y in range(NH):
	for x in range(NH):
		yx=(y,x)
		ps.append(yx)
		for nyx in all4(yx):
			dictuni[nyx]=yx

print("start")

most2=[]
for dx in range(NH):
	for dy in range(-NH+1,NH):
		if gcd(abs(dx),abs(dy))!=1:
			continue
		gbcp=defaultdict(lambda:[])
		for y in range(N):
			for x in range(N):
				cprod=x*dy-y*dx;
				gbcp[cprod].append(dictuni[(y,x)]) # has duplicate term, "x+x+y<=2"
		for k,v in gbcp.items():
			if len(v)>=3:
				most2.append(tuple(sorted(v)))
print(len(most2))
most2=sorted(list(set(most2)))

sum2=[]
for i in range(NH):
	sum2.append(tuple(sorted([dictuni[(i,j)] for j in range(N)])))
	# sum2.append(tuple(sorted([dictuni[(j,i)] for j in range(N)])))
	# each sum2 slice contains exactly 1 duplicate point
	# each row of N correspond to a "+" column in NH*NH crossing at main diagonal, same as column
sum2=sorted(list(set(sum2)))

print("gen ok",len(most2),len(sum2))

# remove some of obvious redundancy (~1%)
setmost2=set(most2)
for m2 in most2:
	for i in range(len(m2)):
		m2m1=tuple(m2[:i]+m2[i+1:])
		if m2m1 in setmost2:
			setmost2.remove(m2m1)
print("most2 removed:",len(most2)-len(setmost2),"of",len(most2))
most2=sorted(list(setmost2))

if 0:
	from pyscipopt import Model, quicksum
	scip=Model()
	dvars={}
	for y in range(NH):
		for x in range(NH):
			dvars[(y,x)]=scip.addVar(f"x_{y}_{x}","B")
	for m2 in most2:
		scip.addCons(quicksum([dvars[yx] for yx in m2])<=2)
	for s2 in sum2:
		scip.addCons(quicksum([dvars[yx] for yx in s2])==2)
	if 0:
		scip.setEmphasis(3) # https://scipopt.org/doc/html/type__paramset_8h_source.php#l00070
		scip.optimize()
		sol=scip.getBestSol()
		mtx=[[0 for x in range(N)] for y in range(N)]
		for p,var in dvars.items():
			if sol[var]>0.5:
				yxs=all4(p)
				for yx in yxs:
					mtx[yx[0]][yx[1]]=1
		print("\n".join(map(lambda line:"".join(map(lambda b:("□","■")[b],line)),mtx)))
	else:
		scip.setParamsCountsols()
		scip.count()
		print(scip.getNCountedSols()) # should match https://oeis.org/A037189 * 2
	quit()
	
if 0:
	from z3 import *
	dvars={}
	for yx in ps:
		varyx=Bool("D_%d_%d"%yx)
		dvars[yx]=varyx
	#s=Tactic('smt').solver()
	s=Solver()
	
	most2=[Sum(tuple(map(lambda p:dvars[p],t)))<=2 for t in most2]
	sum2=[Sum(tuple(map(lambda p:dvars[p],t)))==2 for t in sum2]
	print("expr ok")
	s.add(most2+sum2)
	print("add ok")
	print(s.check())
	m = s.model()
	
	mtx=[[0 for x in range(N)] for y in range(N)]
	for p,v in dvars.items():
		v=dvars[p]
		if m.evaluate(v):
			yxs=all4(p)
			for yx in yxs:
				mtx[yx[0]][yx[1]]=1
				
	print("\n".join(map(lambda line:"".join(map(lambda b:("□","■")[b],line)),mtx)))
	quit()
	
if 0: # cnf, AND of ORs
	dvars={}
	for yx in ps:
		dvars[yx]=yx[0]*NH+yx[1]+1
		
	cnfnotalls=[] # convert from most2, mustn't choose sum(coef)>=3
	terms=[] # (coef,var)
	stack=[] # var
	def dg(cur,cursum):
		if cursum>=3:
			cnfnotalls.append(tuple(stack))
			return
		for i in range(cur,len(terms)):
			term=terms[i]
			coef,nvar=term
			stack.append(nvar)
			dg(i+1,cursum+coef)
			stack.pop()
		
	for m2 in most2:
		dcoef=defaultdict(lambda:0)
		for summand in m2:
			dcoef[dvars[summand]]+=1
		terms=[]
		for k,v in sorted(dcoef.items()):
			terms.append((v,k))
		dg(0,0) #add to cnfnotalls
	print("notalls",len(cnfnotalls))
	cnfnotalls=sorted(list(set(cnfnotalls)))
	cnfnotalls=list(map(lambda clause:tuple(map(lambda e:-e,clause)),cnfnotalls))
	print("cnf notalls",len(cnfnotalls))
	
	cnfsum2=[]
	# in fact converted to sum>=2
	for summands in sum2:
		varsummands=[dvars[p] for p in summands]
		# by specifying must choose at least one in "all except each one"
		for i in range(len(varsummands)):
			least1=varsummands[0:i]+varsummands[i+1:]
			# almost always contain a pair of duplicate, only 2 of N that selects one of the pair don't
			# since this is in an OR caluse, duplicate doesn't make sense
			cnfsum2.append(tuple(sorted(set(least1))))
	cnfsum2=sorted(list(set(cnfsum2)))
	print("cnf sum2",len(cnfsum2))
	
	allcnf=cnfnotalls+cnfsum2
	allcnf=list(map(lambda clause:list(clause)+[0],allcnf))
	
	txtclauses="\n".join(map(lambda clause:" ".join(map(str,clause)),allcnf))
	txthead="p cnf %d %d"%(NH*NH,len(allcnf))
	
	with open("no3l2_%d.cnf"%N, mode="w", encoding="utf-8") as cnffile:
		cnffile.write(txthead+"\n")
		cnffile.write(txtclauses+"\n")
		
if 0: #minicard cnf+
	dvars={}
	for yx in ps:
		dvars[yx]=yx[0]*NH+yx[1]+1
	cnfpmost2=list(map(lambda clause:(list(map(lambda e:str(dvars[e]),clause))+["<=","2"]),most2))
	#cnfpsum2=list(map(lambda clause:(list(map(lambda e:str(dvars[e]),clause))+["==","2"]),sum2))
	cnfpsum2le=list(map(lambda clause:(list(map(lambda e:str(dvars[e]),clause))+["<=","2"]),sum2))
	cnfpsum2ge=list(map(lambda clause:(list(map(lambda e:str(-dvars[e]),clause))+["<=",str(len(clause)-2)]),sum2))
	cnfpsum2=cnfpsum2le+cnfpsum2ge
	allcnf=cnfpmost2+cnfpsum2
	txtclauses="\n".join(map(lambda clause:" ".join(clause),allcnf))
	txthead="p cnf+ %d %d"%(NH*NH,len(allcnf))
	
	with open("no3l_%d.cnfp"%N, mode="w", encoding="utf-8") as cnffile:
		cnffile.write(txthead+"\n")
		cnffile.write(txtclauses+"\n")

if 1: #pysat minicard
	from pysat.solvers import Minicard
	s=Minicard()
	dvars={}
	for yx in ps:
		dvars[yx]=yx[0]*NH+yx[1]+1
	cnfpmost2=list(map(lambda clause:(list(map(lambda e:dvars[e],clause))),most2))
	#cnfpsum2=list(map(lambda clause:(list(map(lambda e:str(dvars[e]),clause))+["==","2"]),sum2))
	cnfpsum2le=list(map(lambda clause:(list(map(lambda e:dvars[e],clause))),sum2))
	cnfpsum2ge=list(map(lambda clause:(list(map(lambda e:-dvars[e],clause))),sum2))
	for m2 in cnfpmost2:
		s.add_atmost(m2,2)
	for s2le in cnfpsum2le:
		s.add_atmost(s2le,2)
	for s2ge in cnfpsum2ge:
		s.add_atmost(s2ge,len(s2ge)-2)
	if 0:# extra constraint: no orthogonal touch
		notouch=[]
		for y in range(NH-1):
			for x in range(NH-1):
				notouch.append(((y,x),(y,x+1)))
				notouch.append(((y,x),(y+1,x)))
		for x in range(NH-1):
			notouch.append(((NH-1,x),(x,NH-1)))
			notouch.append(((NH-1,x),(NH-1,x+1)))
			notouch.append(((x,NH-1),(x+1,NH-1)))
		notouch.append(((NH-1,NH-1),))
		cnfnotouch=list(map(lambda clause:(list(map(lambda e:-dvars[e],clause))),notouch))
		s.append_formula(cnfnotouch)
	nofsols=0
	for model in s.enum_models():
		nofsols+=1
		print(nofsols,model)
		mtx=[[0 for x in range(N)] for y in range(N)]
		for p,v in dvars.items():
			v=dvars[p]
			if v in model:
				yxs=all4(p)
				for yx in yxs:
					mtx[yx[0]][yx[1]]=1
		print("\n".join(map(lambda line:"".join(map(lambda b:("□","■")[b],line)),mtx)))
	print("total solutions:",nofsols)

[liffiton]

Thanks for the questions! That's an interesting application. I'd love to hear if you get some new results there.

i see in the code that "=" is supported in opb format (by adding both <= and >=), but not in cnf+? is this intended or, just forgotten?

I didn't think to add it because I wasn't using equality constraints myself at the time, and it would just be syntactic sugar over adding the <= and >= constraints individually. You can still achieve the same result with two constraints instead of one, and the internal implementation would just generate those two constraints from the one = constraint anyway.

ps i wonder what's the status of #3, does duplicate in input still affect correctness across different variant of minicard now?

[...] but i see #3 and this problem uses duplicates, and also i'm on windows, not sure how and which variant of minicard should i compile.

In the CNF encodings, yes, duplicate literals will still give incorrect results. Those encodings weren't really intended to be part of the solver, per se, but rather just demonstrations of alternative approaches to make comparisons (as seen in the poster).

You should compile "the core MiniCard solver with native AtMost constraints" in minicard/.

I don't have the needed combination of time+motivation to work out duplicate literals in the encodings, so that is unlikely to be implemented.

pps is jsminisolvers demo, seems only cnf is handled but not any of cardinality extension... is it unfinished?

Oh, that demo only instantiates a MinisatSolver object, so it's just demoing Minisat, not Minicard. The library includes both; I just didn't put both in the demonstration page. I "cheated" and just used a simple array format for entering clauses there, and parsing out CNF or CNF+ would have taken a lot longer. But again, the library supports Minicard just fine. For your purposes, though, I'd strongly suggest compiling the C++ code natively, as it should have much better performance and fewer limitations than the JS library.

EDIT: oops just find pysat works on windows, gotta try it! EDIT: works like a charm!

And yes, pysat is another way to go. They've since developed the Python library idea much further than I had in PyMiniSolvers.